Parametric polymorphism with references

Paolo Torrini

(Swansea University)

Hindley-Milner polymorphism is a tractable form of parametric polymorphism that is widely used in functional languages (e.g. SML, OCaml, Haskell). Also known as 'let' polymorphism, it allows for generalisation, in the body of 'let' expressions, of type variables that do not occur free in the environment. Proof-theoretic soundness relies on the logic of propositional quantification as part of system F --- although proof systems for 'let' polymorphism can be syntactically defined on top of a distinction between types and type schemes, that makes it possible to dispense with explicit quantifier introduction.

In languages with references, things are more complicated. If evaluating the definiens of a 'let' expression requires allocation of new references, which depend on type variables that occur in the definiens type, the naive approach turns out to be semantically unsound. Different solutions have been proposed and adopted in practice, based on different ways to approximate the set of type variables that are unsafe with respect to generalisation.

The general argument boils down to the fact that type variables can be generalised only when they do not occur free in the environment --- this time in an extended sense though, that should take the store into account. This suggests there may be natural ways to constrain generalisation, relying on more expressive forms of typing judgement, and in particular on substructural logic.
Thursday 2nd May 2013, 14:00
Robert Recorde Room
Department of Computer Science