Type classes with more higher-order polymorphism

10 years 10 months ago
Type classes with more higher-order polymorphism
We propose an extension of Haskell's type class system with bstractions in the type language. Type inference for our extension relies on a novel constrained unification procedure called guided higher-order unification. This unification procedure is more general than Haskell's kind-preserving unification but less powerful than full higher-order unification. The main technical result is the soundness and completeness of the unification rules for the fragment of lambda calculus that we admit on the type level. Categories and Subject Descriptors D.3.2 [Programming Languages]: Language Classifications-Applicative (functional) languages; D.3.3 [Programming Languages]: Language Constructs and Features--Polymorphism; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs--Type Structure General Terms Languages, Theory Keywords type classes, higher-order unification, type inference, Haskell
Matthias Neubauer, Peter Thiemann
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2002
Where ICFP
Authors Matthias Neubauer, Peter Thiemann
Comments (0)