[TYPES] paper on gradual typing with inference

[Matthias Felleisen]

Parametricity has indeed been a stumbling block for our work on Typed  
Scheme -- a full-fledged practical and sound implementation of  
gradual static typing for a production programming language (see POPL  
2008 for the paper, with Sam Tobin-Hochstadt). We are working with  
the rest of PLT though, and Jacob Matthews @ UChicago (with Amal)  
plus others have made good progress on this:

    ESOP 2008: Parametric polymorphism through run-time sealing,
    or Theorems for low, low prices! (Jacob Matthews and Amal Ahmed)
    is probably the best citation for your purposes.

We intend to build on this for the integration of parametric  
polymorphism at module boundaries. -- Matthias


On Jan 17, 2008, at 5:40 PM, 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
>
>
>
>