[wk_end]

typedfalse wrote "unityped", not "untyped" (note the "i").

When type system people talk about types they're implicitly talking about static types, rather than what Python might call a type. Robert Harper lays out the argument [0] that Python is basically a statically typed language with many "classes" but a single type - that's where I was first exposed to this idea.

> The characteristics of a dynamic language are [that] values are classified [...] into a variety of forms that can be distinguished at run-time. A collection of values can be of a variety of classes, and we can sort out at run-time which is which and how to handle each form of value. Since every value in a dynamic language is classified in this manner, what we are doing is agglomerating all of the values of the language into a single, gigantic (perhaps even extensible) type. To borrow an apt description from Dana Scott, the so-called untyped (that is “dynamically typed”) languages are, in fact, unityped. Rather than have a variety of types from which to choose, there is but one!

> And this is precisely what is wrong with dynamically typed languages: rather than affording the freedom to ignore types, they instead impose the bondage of restricting attention to a single type! Every single value has to be a value of that type, you have no choice! Even if in a particular situation we are absolutely certain that a particular value is, say, an integer, we have no choice but to regard it as a value of the “one true type” that is classified, not typed, as an integer. Conceptually, this is just rubbish, but it has serious, tangible penalties. For one, you are depriving yourself of the ability to state and enforce the invariant that the value at a particular program point must be an integer. For another, you are imposing a serious bit of run-time overhead to represent the class itself (a tag of some sort) and to check and remove and apply the class tag on the value each time it is used.

[0] https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...

[teddyh]

That’s not the normal nomenclature. If that language was used to describe, for instance, Java, we could say that Java only has a very small number of types: the unboxed types, and “object”. But this is not how we usually describe Java, and also not how we normally describe dynamically typed languages.

[wk_end]

No, that's not the case. The term "class" here isn't being used to describe OOP classes. You can read the article for more details, but "class" here is being used to describe something like a dynamically distinguished subset of a type: a branch of a sum type in a language like Haskell or SML or Idris.

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.

[teddyh]

> When type system people talk about types they're implicitly talking about static types, rather than what Python might call a type. Robert Harper lays out the argument [0] that Python is basically a statically typed language with many "classes" but a single type - that's where I was first exposed to this idea.

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.

[still_grokking]

> 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?

[teddyh]

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.

[still_grokking]

> 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).