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.

BibTeX:

@inproceedings{Nipkow-Snelting,
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},
year=1991,publisher=Springer,series=LNCS,volume=523,pages={1--14}}

This paper is superseded by the work of Nipkow and Prehofer.