[TYPES] Types of expressions in dynamic languages: "un-typed" or "uni-typed"?

[Prof. Robert Harper]

Please see my Practical Foundations book for a thorough discussion of this needlessly vexed issue.

The word "type" should be reserved for structural purposes, they codify the "comprehension principles" that constitute the language.  Things like "duck types" are "refinements" or "predicates" that are descriptive of the (typed) programs that have a pre-determined operational meaning.  So, of course, Python and its relatives are and always have been unityped.  Some also have refinements to express verification conditions.  

One side benefit of calling a type a type is that one immediately sees that the whole idea of having only one type is, um, questionable.  First off, why confine yourself a priori to such a severe limitation?  Second off, you will see that the language really has half-hearted stabs at having types by having, for example, "multiple arguments", which exposes in an ad hoc way the type "thing * thing * ... * thing" or "thing sequence" without really admitting it (and using pattern matching syntax to cover it up).

Bob Harper

Sent from tablet

> On Jan 7, 2014, at 22:11, 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 was
> 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
> equivalent.
> 
> 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
> phrasing.
> 
> 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
> expression.
> 
> 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
> 
>