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

• Type: Conference
• Year: 2002
• Where: ICFP
• Authors: Matthias Neubauer, Peter Thiemann
• Keywords: ICFP 2002, Kind-preserving Unification, Programming Languages, Unification Procedure, Unification Rules