Standard ML Weak Polymorphism Can Be Sound

Adding ML-style references to a Hindley-Milner polymorphic type system is troublesome because such a system is unsound with naive polymorphic generalization of reference types. Tofte [12] introduced a distinction between imperative and applicative type variables, such that applicative type variables are never in reference types, that provides a simple static analysis of which type variables may be polymorphically generalized. MacQueen's [7] weak type variables generalize imperative type variables with a counter called a strength. The finer distinction allows a more accurate analysis of when a reference may be created, and thus which type variables may be generalized. Unfortunately, weak polymorphism has been presented only as part of the implementation of the SML/NJ compiler, not as a formal type system. As a result, it is not well understood, as its more subtle points are not well known. Furthermore, while versions of the implementation have repeatedly been shown unsound, the concept ..