On typed, untyped, and “uni-typed” languages
Recently, the question of how to refer to languages like Racket, Python, or JavaScript came up on the TYPES mailing list (a list that includes most of the academic researchers in programming languages). I wrote a reply there, but I thought it deserved a nicer form.
Benjamin Pierce, in the introduction to Types and Programming Languages, which is probably the standard text on type systems in English at this point, defines types systems as follows:
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.
According to this, Python (and Ruby, JavaScript, Scheme, etc) doesn't do this, and thus does not have a type system, and is therefore usefully classified as "untyped". John Reynolds, in my advisor’s favorite definition of a type system, writes:
Type structure is a syntactic discipline for enforcing levels of abstraction.
Python has a variety of methods for enforcing abstraction levels, but they are not syntactic, with the possible exception of scope. It might be possible to view scopes in Python or other languages as type systems, but that would probably not prove very enlightening.
The slogan the “untyped is uni-typed”, often propounded by Bob Harper is somewhat different. In the general case, the implementation of a language like Python must be implemented so that there's exactly one “type” internally, and all Python values fit into that type. You can see this if you look at the Python C API -- there's the `PyObject` type, and it represents anything in Python. Other languages have similar internal implementation types. In contrast, the C API for OCaml doesn't have a such a type. In this sense, the "uni-typed" claim is clearly true.
However, if you want to understand why people find untyped languages useful, and how they use them, I think that the uni-typed perspective doesn't let us answer the questions we want. This is similar to the perspective that human thinking operates at the level of neurons—it's clearly true, but it doesn't help us figure out what other people will do in practice. Instead, I find it useful to think about how programmers in languages like Python reason about their programs—often it turns out to be via unformalized reasoning that bears a close resemblance to Pierce and Reynolds' definitions, usually often not to particular type systems in existing languages. Much of our work on Typed Racket has involved exploring exactly this question.
