Records, variants and qualified types

Benedict R. Gaster

PhD Thesis.

University of Nottingham
Technical report NOTTCS-TR-98-3


Records and variants provide flexible ways to construct datatypes, but the restrictions imposed by type systems can prevent them from being used in flexible ways. For example, typed languages often prohibit basic operations such as adding fields to a record, and may not allow access to individual components unless the type, and hence the run-time representation of the record, is fixed at compile-time. These limitations are often the result of concerns about efficiency, or of the inability to express accurately the types of key operations.

This dissertation studies type systems that remedy these problems, supporting extensible records and variants, with a full complement of polymorphic operations on each. The systems are based on the theory of qualified types, from which they inherit a simple compilation method and effective type inference for the implicitly typed versions.

Qualified types is a general theory for constrained polymorphism, whose semantics (implicit) has previously been defined in terms of a translation into the second order polymorphic lambda-calculus, supported by a statement of coherence. This dissertation describes two alternative (explicit) semantics for qualified types. The first
describes the meaning of an overloaded expression via specialization, while the second interprets expressions in polynomial categories.