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

[Sean McDirmid]

Pragmatically, the programmer is still able to talk about "ducks" in Python even if the check to see if a value can be used as a duck occurs dynamically. Explaining to the programmer that Python only has one type would be very unfriendly and confusing when clearly one can talk about ducks that quack in the language without much problems.

I guess it depends on your definition of type system and types. For a narrower definition oriented purely around static type checking, it might make sense to say Python has one type.

On Jan 8, 2014, at 21:59, "Gavin Mendel-Gleason" <gavin.mendel.gleason at gmail.com<mailto:gavin.mendel.gleason at gmail.com>> wrote:


Sure what's wrong with uni-typing as a description?  If you want to mimic dynamic typing in a typed programming language, it's trivial to do with a single type embedding all the types available with a wrapping constructor.  Unboxing is simply a compiler optimisation removing the constructor through some sort of partial computation.  Type errors are really just exceptions that give assertions on the typing constructors allowed in a given code path.


On 8 January 2014 10:09, Sean McDirmid <smcdirm at microsoft.com<mailto:smcdirm at microsoft.com>> wrote:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

It is difficult to sort any type system into a simple easily named bucket.

I see Python (and Ruby, Javascript) as dynamically and structurally typed. Static structural typing and dynamic nominal typing are completely sensical for other languages (especially the former, the latter is possible even if it lacks examples).

I reserve "untyped" for languages where you don't even get a decent message-not-understood run-time error (e.g. a memory corruption in C on doing something bad to a void*). Untyped is much weaker than a safe dynamic language that crashes more elegantly (and more easily debugged) when a type error occurs.

I agree that the concept of uni-typing isn't very useful; it doesn't tell us very much about the real typing properties of the language.

-----Original Message-----
From: Types-list [mailto:types-list-bounces at lists.seas.upenn.edu<mailto:types-list-bounces at lists.seas.upenn.edu>] On Behalf Of Siraaj Khandkar
Sent: Wednesday, January 8, 2014 11:12 AM
To: types-list at lists.seas.upenn.edu<mailto:types-list at lists.seas.upenn.edu>
Subject: [TYPES] Types of expressions in dynamic languages: "un-typed" or "uni-typed"?

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