[TYPES] paper on gradual typing with inference

[Geoffrey Alan Washburn]

Philip Wadler wrote:
> If you set it up carefully, it is possible to mix polymorphic functions 
> with gradual typing and maintain parametricity.  
    It is also worth noting that it is possible to develop a 
generalization of the parametricity theorem that holds in languages with 
runtime type analysis, and should be applicable to languages with adhoc 
polymorphism and other sorts of dynamic type tests. 

In the polymorphic lambda-calculus, no expression is allowed to depend 
upon how an abstract type may be instantiated.  The first key insight is 
that this property is merely one end of a spectrum.  At the other end of 
the spectrum, any expression in a term may depend on the instantiation 
of any possible abstract type.  In between, some expressions may be 
depend on the instantiation of some abstract types.  I expect most 
programs using runtime type analysis, etc. fall somewhere in this part 
of the spectrum.

The second key insight is that in the polymorphic lambda-calculus this 
dependency relationship (or rather the lack of dependency) is implicit.  
Therefore, if we augment the type system to make it possible to express 
the dependencies between abstract types and expressions explicitly, it 
is possible to reason about these other points in the spectrum.  
Information-flow type systems are an example of a class of type systems 
that makes dependencies between expressions explicit by labeling types.  
Therefore, one way that the dependencies could be made explicit is to 
augment the type system of the polymorphic lambda-calculus with 
information-flow labels on both types and kinds. 

For example, assuming that the labels are drawn from a lattice with both 
top (Top) and bottom (Bot) elements.  The type of the identity function 
in the polymorphic lambda-calculus,

    forall a:*. a -> a,

where * is the base kind, could then be expressed in this augmented 
language as

    forall a:(* @ Top). a @ Bot -> a @ Bot.

Here "* @ Top" is used to denote "a type with the information content 
Top", and "a @ Bot" is used to denote "a value of type 'a' with an 
information content of Bot".  Therefore, for any given instantiation of 
the universal, the function takes values of that type, with no 
information content, to values of that type, again with no information 
content.  Assuming that there is no general recursion, we know that this 
function must be the identity function because the information content 
of the of the value produced is less than the information content of the 
abstract type (Bot <: Top).  This fact means that it is not possible for 
the value returned by the function to depend upon the type used to 
instantiate the universal.  Therefore, the function must return its 
argument, because there is no other means of producing a value of the 
correct type. 

Alternately, if we have a function with the type

    forall a:(* @ Top). a @ Bot -> a @ Top

it is possible that this function is not the identity because the value 
returned has  a maximal information content.   Therefore, the value 
returned might depend upon the chosen instantiation of the universal.  
For example, it could be the function that returns its argument, unless 
the argument is an integer, in which case, the function returns 0.

For more information on this idea, you can read my LICS 2005 paper, 
written with Stephanie Weirich, "Generalizing Parametricity Using 
Information Flow".   Even more information on this idea can be found in 
my dissertation.