Type Reconstruction for Type Classes

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. 1 Introduction The extension of Hindley/Damas/Milner polymorphism with the notion of type classes in the functional programming language Haskell (HJW92) has attracted much attention. Type classes permit the systematic overloading of function names while retaining the advantages of the Hindley/Damas/Milner system: every typable expression has a most general type ..