[TYPES] paper on gradual typing with inference

[Philip Wadler]

Tim,

If you set it up carefully, it is possible to mix polymorphic functions 
with gradual typing and maintain parametricity.  Here is a paper that 
discusses the key idea in the context of contracts:

Relationally-parametric polymorphic contracts
A Guha, J Matthews, RB Findler, S Krishnamurthi - Proceedings of the 
2007 symposium on Dynamic languages, 2007 - portal.acm.org

Also look out for forthcoming papers on this topic by Jacob Matthews, 
Amal Ahmed, Robby Finder, and Philip Wadler (all together and in various 
combinations).

Cheers,  -- P


Tim Sweeney wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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
> 
> 
> 
> 

-- 
  \ Philip Wadler, Professor of Theoretical Computer Science
  /\ School of Informatics, University of Edinburgh
/  \ http://homepages.inf.ed.ac.uk/wadler/