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.