[TYPES] paper on gradual typing with inference

[Tim Sweeney]

Hello,

This is a welcome work on gradual typing.

Now, please pardon me for using this thread to note something relevant to dynamic and gradual typing, which I haven't seen said elsewhere:

Any language with a dynamic or gradual type system is necessarily either partial (potentially non-terminating), or aparametric (admitting programs that violate the parametricity property, described in http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html).

This is the case because a dynamically typed fragment of a program may coerce a value of unknown type to a specific type required in a context, such as coercing x to a numeric type in x+1.

A coercion which fails may provide a means such as exception-handling or returning an appropriately typed indicator value (such as the integer value 0) which the program can observe and act upon.  In this case, the language is aparametric, as it allows extracting information from a value of universal type.  But parametricity is a valuable security property in languages: a pure function with a parameter of universally quantified type guarantees that it cannot inspect that parameter, but can only place it somewhere in its result value.

If failed coercions always cause an unrecoverable program abort, then it's observably equivalent to any other divergent outcome.  Hence the language doesn't necessarily violate parametricity, but it is certainly partial.

Because gradual typing, total programming, and parametricity are all desirable features in a language, I wanted to note that a type system can soundly support all three in the following way:

Start with a total language, and extend it using e.g. Haskell style monads, or effects-typing, to support aparametricity and partiality as effects.  At the top level of a program, both would be allowed.  Once a function is invoked with requires parametricity or totality, the type system guarantees that it cannot perform operations which are either partial or aparametricity.

This approach could be extended further, to the extent of treating every axiom underlying a type system as an independent effect, enabling portions of code to be verified within restrictive fragments of the type system guaranteeing other properties such as linearity, non-commutativity, etc.

This provides an interesting means for soundly layering future proofs-of-programs features requiring parametricity and totality on top of existing languages and runtime frameworks which are more lax.

Tim Sweeney

-----Original Message-----
From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of Jeremy Siek
Sent: Wednesday, January 16, 2008 7:14 PM
To: type-list
Subject: [TYPES] paper on gradual typing with inference

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Colleagues,

We are pleased to share with you a new paper about integrating
gradual typing and unification-based type inference (which
underlies the Hindley-Milner type system). This was one of
those systems where the algorithm was easy to come up
with, but the type system was somewhat tricky.

http://ece.colorado.edu/~siek/pldi08gradual.pdf

Any comments or suggests are most welcome.

The paper is under review for PLDI 2008**.

Best regards,
Jeremy Siek & Manish Vachharajani

**The review was double blind, but the reviews have already been
submitted and the identities of the authors revealed.

____________________________________
Jeremy Siek <jeremy.siek at colorado.edu>
http://ece.colorado.edu/~siek/
Assistant Professor
Dept. of Electrical and Computer Engineering
University of Colorado at Boulder