ISBN 0-521-47253-9
This book describes the use of qualified types to provide a general framework for the combination of polymorphism and overloading. For example, qualified types can be viewed as a generalization of type classes in the functional language Haskell and the theorem prover Isabelle. These in turn are extensions of equality types in Standard ML. Other applications of qualified types include extensible records and subtyping.
Using a general formulation of qualified types, the author extends the Damas/Milner type inference algorithm to support qualified types, which in turn specifies the set of all possible types for any term. In addition, he describes a new technique for establishing suitable coherence conditions that guarantee the same semantics for all possible translations of a given term.
Practical issues that arise in concrete implementations are also discussed, concentrating in particular on the implementation of overloading in Haskell and Gofer, a small functional programming system developed by the author.
This thesis describes a type system that combines ML-style polymorphism with a general approach to overloading. The central idea is to use qualified types that include predicates and restrict the set of types at which an object can be used to particular instances of a polymorphic type. Different applications of qualified types can be obtained by changing the underlying system of predicates. We illustrate this with examples including type classes, explicit subtyping and extensible records.
Much of the thesis deals with a simple, implicitly typed, functional language. Extending the Damas/Milner approach to type inference, we define an ordering between the constrained type schemes used in our system and show that the set of all possible typings for a given term has a greatest element with respect to this ordering. Furthermore, this principal type scheme can be calculated using a type inference algorithm.
Using an abstract notion of evidence, we show how the meaning of a program in this system can be described by translating it into a language that includes constructs for manipulating evidence values. Since any given term may have many distinct translations it is necessary to give coherence conditions which guarantee that the meaning of a term is well defined. This thesis introduces a new technique for establishing results of this kind, using a semantic interpretation of the ordering relation on type schemes.
We also address more practical issues concerning the use of qualified types, both for the general system and for specific applications. This includes a promising new representation for extensible records, based on the use of evidence. In addition, we describe the implementation of type classes in Haskell and Gofer, an experimental system developed by the author.