News for hackers. Stuff that matters.
Re:Idris: A Language for Type-Driven Development by still_grokking on Tuesday January 24, 2023 @02:51AM (#34500733)
> According to this, there are no such things as "dynamically typed” langugages, only “unityped” ones.

Bingo.

That's exactly what Harper said.

Did you actually read that thing?

Re:Idris: A Language for Type-Driven Development by teddyh on Tuesday January 24, 2023 @02:43PM (#34509084)
It doesn’t actually matter what that thing said. Most everybody uses the term “dynamically typed” when referring to languages like Python, Lisp, etc. and this is the first time I’ve heard the term “unityped” – is not a term in common use.

And (bringing this back to its origin), using terms which actually are in common use, Python does allow storing types as values in variables.

Re:Idris: A Language for Type-Driven Development by still_grokking on Wednesday January 25, 2023 @02:21AM (#34515394)
> is not a term in common use

That's the fun thing about it. But in some circles everybody knows this term. ;-) (You can see it as an "in joke", if you like).

> Python does allow storing types as values in variables.

Python does not have "types" in the CS sense (besides the one all mighty uni-type, of course).

All you can store in variables in Python are values. (Before arguing further please look up type theory first, so we can avoid going in circles).