On the Type Structure of Standard ML

Abstract

Standard ML is a useful programming language with a polymorphic type system and a flexible module facility.One notable feature of the core expression language of ML is that it is implicdy typed: no explicit type information need be supplied by the programmer.In contrast, the module language of ML is explicitly typed; in particular, the types of parameters in parametric modules must be supplied by the programmer.We study the type structure of Standard ML by giving an explicitly-typed, polymorphic function calculus that captures many of the essential aspects of both the core and module language.In this setting, implicitly-typed core language expressions are regarded as a convenient short-hand for an explicitly-typed counterpart in our function calculus.In contrast to the Girard-Reynolds polymorphic calculus, our function calculus is