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 esentially 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...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.