ON THE TYPE-STRUCTURE OF STANDARD ML

Standard ML is a useful programming language with a polymorphic type s ystem and a flexible module facility. One notable feature of the core expression language of ML is that it is implicitly 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-typ ed, polymorphic function calculus that captures many of the essential aspects of both the core and module language. In this setting, implici tly-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 ca lculus is predicative: the type system may be built up by induction on type levels. We show that, in a precise sense, the language becomes i nconsistent if restrictions imposed by type levels are relaxed. More s pecifically, we prove that the important programming features of ML ca nnot be added to any impredicative language, such as the Girard-Reynol ds calculus, without implicitly assuming a type of all types.