Technical reports

Type classes and overloading resolution via order-sorted unification

Tobias Nipkow, Gregor Snelting

August 1990, 16 pages

DOI: 10.48456/tr-200

Abstract

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 is given by a translation into ordinary λ-calculus. We prove the correctness of our type inference algorithm with respect to this semantics.

Full text

PDF (1.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-200,
  author =	 {Nipkow, Tobias and Snelting, Gregor},
  title = 	 {{Type classes and overloading resolution via order-sorted
         	   unification}},
  year = 	 1990,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-200.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-200},
  number = 	 {UCAM-CL-TR-200}
}