If I write a well-typed function in one of these languages that consumes a value of type Foo, it's statically guaranteed that it can operate on any value of type Foo, regardless of its class, but it needs to dynamically ascertain - using a pattern match - which class of Foo-typed values it is to do anything meaningful with it.
Java operates under the same principle, in its way. In Java, barring escape hatches from the type system (casts), if I write a method that consumes an object of type Foo, likewise, it's statically enforced that it can operate on any object of type Foo, and notably it can't operate on any object of type Object. But in order to invoke a method on my Foo-typed object, it needs to do a dynamic dispatch to ascertain which class' methods to invoke. So what Java calls classes do type-theoretic double-duty - in a static dispatch context, Foo is a type; but in a dynamic dispatch context, Foo's subclasses constitute its open set of (type-theoretic) classes.
This is totally normal nomenclature in PLT circles (Harper, after all, is one of the biggest names in PLT circles, and he's borrowed this idea from Dana Scott who's another big name). The comments section of an article on a programming language, especially one deeply rooted in PLT, is probably a reasonable place to be open to it.
According to this, there are no such things as dynamically typed langugages, only “unityped” ones. I stand by my claim that the former is a normal accepted term, while the latter is niche at best.
Bingo.
That's exactly what Harper said.
Did you actually read that thing?
And (bringing this back to its origin), using terms which actually are in common use, Python does allow storing types as values in variables.
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).