Accession Number : ADA267839


Title :   Standard ML Weak Polymorphism Can Be Sound


Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE


Personal Author(s) : Greiner, John


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a267839.pdf


Report Date : May 1993


Pagination or Media Count : 22


Abstract : 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 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.


Descriptors :   *POLYMORPHISM , DATA PROCESSING , MANAGEMENT , VARIABLES , SOUND , COUNTERS , STORAGE , STATICS , COMPILERS


Subject Categories : Crystallography


Distribution Statement : APPROVED FOR PUBLIC RELEASE