[TYPES] paper on gradual typing with inference

[David Hopwood]

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.

Parametricity is one way to achieve this security property, but it can also
be achieved in other ways that do not involve parametricity (and are simpler
than the approach you suggest using monads or effects-typing, I think).

For example, class-based object-oriented programming languages typically
support private instance variables. So an instance of a "box" class with a 
private field holding some value (possibly of a parameterized type) can be
passed to a pure function with the same practical effect as passing a
parameter of universally quantified type in a language with parametricity:
the function can only return the box. (If the function is impure, it can
also place a reference to the box elsewhere, but still cannot obtain the
encapulated value.) Obtaining the value from the box can either require use
of a token/capability value, or can be restricted to a certain lexical
region of the program.

Class-based object-orientation can be simulated easily just using lexically
scoped closures, so this technique can be used in a wide range of languages,
including languages that are both total and gradually typed.

-- 
David Hopwood