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.

Robert Recorde Room

Department of Computer Science