Type Classes and Overloading Resolution via Order-Sorted Unification

Tobias Nipkow, Gregor Snelting

We present a type inference algorithm for a Haskell-like language based on order-sorted unification. The language features polymorphism, overloading, type classes and multiple inheritance. Class and instance declarations give rise to an order-sorted algebra of types. Type inference essentially reduces to the Hindley/Milner algorithm where unification takes place in this order-sorted algebra of types. The theory of order-sorted unification provides simple sufficient conditions which ensure the existence of principal types. The semantics of the language is given by a translation into ordinary lambda-calculus. We prove the correctness of our type inference algorithm with respect to this semantics.


author={Tobias Nipkow and Gregor Snelting},
title={Type Classes and Overloading Resolution via Order-Sorted Unification},
booktitle={Proc.\ 5th ACM Conf.\ Functional Programming Languages and
Computer Architecture},
editor={J. Hughes},
This paper is superseded by the work of Nipkow and Prehofer.