[TYPES] Types of expressions in dynamic languages: "un-typed" or "uni-typed"?
samth at cs.indiana.edu
Wed Jan 8 10:37:12 EST 2014
Pierce, in the introduction to TaPL, writes:
"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."
do this, and thus does not have a type system, and is therefore
usefully classified as "untyped".
Reynolds , 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 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.
 Reynolds, _Types, Abstraction, and Parametric Polymorphism_,
Information Processing, 1983
 If you look at the OCaml C API, this will appear to be wrong, but
the `value` type is really a pointer type, and the pointed-to value in
the heap is not tagged in the way a `PyObject` is.
On Tue, Jan 7, 2014 at 10:11 PM, Siraaj Khandkar <siraaj at khandkar.net> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> We're having a discussion with a friend regarding the most accurate way
> to describe the typing situation in Python.
> His view is that Python data are typed and variables un-typed, moreover,
> he proposes that the terms "un-typed" and "uni-typed" are practically
> At first it seemed somewhat reasonable to me, but the more I thought
> about it, the more my mind rejected both, the equivalence and the
> The idea of uni-typing is that there's a set of types that the runtime
> supports and expressions can be composed of any members of that set,
> thus forming a single type, which is that set. This idea seems to
> describe the situation in a useful (for analysis) and an enlightening
> way, while the term "un-typed" does not seem to say anything useful.
> I'm also feeling uneasy about the phrasing: un-typed _variables_. That
> is, data and _expressions_ have types, but individual variables are just
> not something you can make a claim about outside of a context of an
> We'd appreciate very much if the enlightened folks of this list would
> provide some input on this.
> Siraaj Khandkar
> .o. o.o ..o o.. .o.
> ..o .oo o.o .oo ..o
> ooo .o. .oo oo. ooo
More information about the Types-list