Polymorphic Type Inference and Abstract Data Types

                          Konstantin Laufer
                         laufer@math.luc.edu

                            Martin Odersky
                          odersky@ira.uka.de

                             June 5, 1994

                       Technical Report LUC-001

      An abridged version appeared in ACM Trans. on Programming
      Languages and Systems, Vol 16(6), Sept 1994, pp 1411-1430.


Many statically-typed programming languages provide an abstract data
type construct, such as the module in Modula-2. However, in most of
these languages, implementations of abstract data types are not
first-class values. Thus they cannot be assigned to variables, passed
as function parameters, or returned as function results.

Several higher-order functional languages feature strong and static
type systems, parametric polymorphism, algebraic data types, and
explicit type variables. Most of them rely on Hindley-Milner type
inference instead of requiring explicit type declarations for
identifiers.  Although some of these languages support abstract data
types, it appears that none of them directly provides light-weight
abstract data types whose implementations are first-class values.

We show how to add significant expressive power to statically-typed
functional languages with explicit type variables by incorporating
first-class abstract types as an extension of algebraic data
types. Furthermore, we extend record types to allow abstract
components. The components of such abstract records are selected using
the dot notation.

Following Mitchell and Plotkin, we formalize abstract types in terms
of existentially quantified types. We give a syntactically sound and
complete type inference algorithm and prove that our type system is
semantically sound with respect to a standard denotational semantics.

Categories and Subject Descriptors: D.3.2 [Programming Languages]:
Language Classifications -- applicative languages; D.3.3 [Programming
Languages]: Language Constructs and Features -- abstract data types,
modules, packages; F.3.2 [Logics and Meanings of Programs]: Semantics
of Programming Languages -- denotational semantics; F.3.3 [Logics and
Meanings of Programs]: Studies of Program Constructs -- type structure

General Terms: Languages, Theory

Additional Key Words and Phrases: Dynamic dispatching, existentially
quantified types, first-class abstract types, polymorphism, type
inference, universally quantified types