Does “untyped” also mean “dynamically typed” in the academic CS world?

Yes, this is standard practice in academic literature. To understand it, it helps to know that the notion of “type” was invented in the 1930s, in the context of lambda calculus (in fact, even earlier, in the context of set theory). Since then, a whole branch of computational logic has emerged that is known as “type theory”. Programming language theory is based on these foundations. And in all these mathematical contexts, “type” has a particular, well-established meaning.

The terminology “dynamic typing” was invented much later — and it is a contradiction in terms in the face of the common mathematical use of the word “type”.

For example, here is the definition of “type system” that Benjamin Pierce uses in his standard text book Types and Programming Languages:

A type system is a tractable syntactic method for proving the absence
of certain program behaviors by classifying phrases according to the
kinds of values they compute.

He also remarks:

The word “static” is sometimes added explicitly–we speak of a
“statically typed programming language,” for example–to distinguish the
sorts of compile-time analyses we are considering here from the
dynamic or latent typing found in languages such as Scheme (Sussman
and Steele, 1975; Kelsey, Clinger, and Rees, 1998; Dybvig, 1996),
where run-time type tags are used to distinguish different kinds of
structures in the heap. Terms like “dynamically typed” are arguably
misnomers and should probably be replaced by “dynamically checked,”
but the usage is standard.

Most people working in the field seem to be sharing this point of view.

Note that this does not mean that “untyped” and “dynamically typed” are synonyms. Rather, that the latter is a (technically misleading) name for a particular case of the former.

PS: And FWIW, I happen to be both an academic researcher in type systems, and a non-academic implementer of JavaScript, so I have to live with the schisma. 🙂

Leave a Comment