[TYPES] paper on gradual typing with inference

[Jeremy Siek]

Hi Tim, Matthias, Phil,

On Jan 18, 2008, at 7:54 AM, Matthias Felleisen wrote:

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

Yes, I'd recommend both the above paper and the DSL 2007 paper Phil  
mentioned in the following
email.

Also, I'd like to point out a closely related issue (perhaps a  
different view on the same issue).
Casts could allow programmers to introspect on a type, thereby  
breaking parametricity.
For example, if one were allowed to write (using the notation of  
System F)

f = /\ a. fun x:a. ((fun y:?. y + 1) a)

then f is not really parametric because the program is checking  
whether 'a' is 'int'.

In the design of our inference algorithm, there is a little bit of  
foreshadowing of this
problem and one way to solve it. During inference, if a type variable  
is constrained by
a ? and nothing more specific, then the type variable resolves to ?  
(so it does not
stay a type variable). Extending this to a Hindley-Milner setting,  
this means we would
not generalize that type variable. For example, in

let f = fun x. ((fun y:?. y +1) a)
in ...

we have

f : ? -> int

and not

f : forall a. a -> int

Thus, with this approach we consider casts as yet another kind of  
operation
that rules out polymorphism.

Cheers,
Jeremy


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