Nested Types

Martin Odersky Swiss Federal Institute of Technology Lausanne

Modern object-oriented programming languages such as Beta or Java have introduced the idea of nested classes. Modern module systems such as the ones of SML or CAML also support nesting, namely nesting of signatures and structures. Details differ, but there are many parallels in the motivation and applications of both approaches. In particular, there are strong analogies between abstract type components in module signatures, formalizations of virtual types in Beta, and formalizations of self-types and matching.

Trying to bring out the commonalities in these approaches, we discuss a type system which focuses on nested types. A type declaration in that system defines a record type signature which may itself contain nested type declarations. These nested type declarations may be either abstract or concrete. Abstract nested types may be redefined in subtypes of their containing types. A type declaration which redefines an abstract type component of a supertype may strengthen the abstract type’s bound, or it may give a concrete implementation type.

Abstract types do not have explicit open and pack constructs associated with them. Instead, dot notation (i.e. record access) is used for opening an abstract type and record formation is used for packing abstract components.

This idea leads to a simple and general scheme for expressing many typing problems addressed by advanced object and module systems. In particular, one can model

• abstract type-like encapsulation such as class-private or package-private members in Java,

• self types and matching,

• sound uses of virtual types, such as covariant specialization of families of classes,

• functors with sharing constraints.

All these concepts can be obtained by encodings into a kernel language over function types, nested record types, and type parameterization. The encodings are generally quite straightforward, so that it’s conceivable that programmers programmers could apply them directly, rather than going through pre-packaged language extensions.

In agreement with mainstream programming language practice, our type system is nominal: type declarations introduce fresh types and subtyping is governed by explicit subtype clauses. This is in contrast to most classical type systems which only consider structural typing. The nominal approach makes it easy to express many patterns of recursive type references and sidesteps decidability problems which would arise in a structural version of the type system.