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.