[Prev][Next][Index][Thread]
SML weak types paper available
The following paper on the soundness of SML "weak" types is now
available via anonymous ftp from
reports.adm.cs.cmu.edu
1993/CMU-CS-93-160.ps
This is a reworking of an incorrect version previously announced on
the SML mailing list. It has also been submitted to the Journal of
Functional Programming.
------------------------------------------------------------------------
Standard ML Weak Polymorphism Can Be Sound
John Greiner
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 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 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 has not
been proven sound or unsound. We present several formal systems of
weak polymorphism, show their connection to the SML/NJ implementation,
and show the soundness of most of these systems.