Standard ML Type Generativity as Existential Quantification

Claudio Russo

Abstract: One of the distinguishing features of Standard ML is the use of type generativity. Each declaration of a datatype binds a globally fresh type name to the type identifier introduced. Type generativity has been regarded as an extra-logical device which, though desirable in a programming language to ensure data abstraction, bears no close resemblance to type theoretic constructs. We show that it corresponds precisely to existential quantification over types, and use the observation to suggest proper extensions to the current static semantics of Standard ML.

Keywords: language design, type theory, modules, Standard ML.

LFCS report ECS-LFCS-96-344, June 1996.

This report is available in the following forms.