An Extension of ML with First-Class Abstract Types

           In Proceedings of the ACM SIGPLAN Workshop on ML
            and its Applications, San Francisco, June 1992

      Konstantin Laufer, New York University, laufer@cs.nyu.edu

         Martin Odersky, Yale University, odersky@cs.yale.edu


This paper presents a semantic extension of ML, where the component
types of a datatype may be existentially quantified. We show how
datatypes over existential types add significant flexibility to the
language without even changing ML syntax; in particular, we give
examples demonstrating how we express

o first-class abstract types,

o multiple implementations of a given abstract type,

o heterogeneous aggregates of different implementations of the same
  abstract type, and

o dynamic dispatching of operations with respect to the implementation
  type.

We have a deterministic Damas-Milner inference system for our
language, which leads to a syntactically sound and complete type
reconstruction algorithm. Furthermore, the type system is semantically
sound with respect to a standard denotational semantics.  Most
previous work on existential types does not consider type
reconstruction. Other work appears to be semantically unsound or does
not permit polymorphic instantiation of variables of existential
type. By contrast, in our system such variables are let-bound and may
be instantiated polymorphically.

We have implemented a Standard ML prototype of an interpreter with
type reconstruction for our core language, Mini-ML extended with
recursive datatypes over existentially quantified component types. All
examples from this paper have been developed and tested using our
interpreter.