The meaning of programs in a language with implicit overloading can be described by translating them into a second language that makes the use of overloading explicit. A single program may have many distinct translations and it is important to show that any two translations are semantically equivalent to ensure that the meaning of the original program is well-defined. This property is commonly known as coherence.
This paper deals with an implicitly typed language that includes support for parametric polymorphism and overloading based on a system of qualified types. Typical applications include Haskell type classes, extensible records and subtyping. In the general case, it is possible to find examples for which the coherence property does not hold. Extending the development of a type inference algorithm for this language to include the calculation of translations, we give a simple syntactic condition on the principal type scheme of a term that is sufficient to guarantee coherence for a large class of programs.
One of the most interesting aspects of this work is the use of terms in the target language to provide a semantic interpretation for the ordering relation between types that is used to establish the existence of principal types.
On a practical level, our results explain the importance of unambiguous type schemes in Haskell.
(This paper summarizes work carried out while the author was a member of the Programming Research Group, Oxford, supported by a SERC studentship.)