Type Reconstruction for Type Classes

Tobias Nipkow, Christian Prehofer

We study the type inference problem for a system with type classes as in the functional programming language Haskell. Type classes are an extension of ML-style polymorphism with overloading. We generalize Milner's work on polymorphism by introducing a separate context constraining the type variables in a typing judgement. This leads to simple type inference systems and algorithms which closely resemble those for ML. In particular we present a new unification algorithm which is an extension of syntactic unification with constraint solving. The existence of principal types follows from an analysis of this unification algorithm.



@article{Nipkow-Prehofer-JFP95, author={Tobias Nipkow and Christian Prehofer}, title={Type Reconstruction for Type Classes}, journal={Journal of Functional Programming},volume=5,number=2, year=1995,pages={201--224}}