A theory of qualified types

A theory of qualified types

Mark P. Jones, In ESOP '92: European Symposium on Programming, Rennes, France, Springer-Verlag Lecture Notes in Computer Science, 582, February 1992.


This paper describes a general theory of overloading based on a system of qualified types. The central idea is the use of predicates in the type of a term, restricting the scope of universal quantification. A corresponding semantic notion of evidence is introduced and provides a uniform framework for implementing applications of this system, including Haskell style type classes, extensible records and subtyping.

Working with qualified types in a simple, implicitly typed, functional language, we extend the Damas/Milner approach to type inference. As a result, we show that the set of all possible typings for a given term can be characterized by a principal type scheme, calculated by a type inference algorithm.

(Supported in part by the Science and Engineering Research Council of Great Britain.)

A revised version of this paper, published in a special edition of Science of Computer Programming, is available by http in pdf, PostScript, or gzipped dvi.