Standard ML–NJ Weak Polymorphism and Imperative Constructs

AbstractStandard ML of New Jersey (SML–NJ) uses “weak type variables” to restrict the polymorphic use of functions that may allocate reference cells, manipulate continuations, or use exceptions. However, the type system used in the SML–NJ compiler has not previously been presented in a form other than source code nor proved correct. We present a set of typing rules, based on analysis of the concepts underlying “weak polymorphism”, that appears to subsume the implemented algorithm and uses type variables of only a slightly more general nature than the compiler. One insight in the analysis is that allowing a variable to occur both “ordinarily” and “weakly” in a type permits a simpler and more flexible formulation of the typing rules. In particular, we are able to treat applications of polymorphic functions to imperative arguments with greater flexibility than SML–NJ. The soundness of the type system is proved for imperative code using operational semantics, by showing that evaluation preserves typability. By incorporating assumptions about memory addresses in the type system, we avoid proofs by co-induction