Understanding Type Classes via Constraint Handling Rules

Type classes are a systematic approach to support ad-hoc polymorphism in Hindley/Milner style systems and have important applications in areas such as generic programming. Type classes have clear connections to Java interfaces and C++ templates and arguably provide a formal model for these concepts.

I co-developed a system that explains type classes in terms of Tom Früwirth's Constraint Handling Rules (CHRs).CHRs are a rule-based language for writing incremental constraint solvers and they turned out to be a highly useful tool to specify the valid type class relations. The most important results [12] include a general characterization of tractable type inference and a coherent semantics, i.e. the meaning of programs is unambiguous. In [7], I uncover some subtle problems in existing description of Haskell's dictionary-passing translation scheme and introduce a revised design which includes recursive dictionaries.

CHRs have also proven useful to specify other ad-hoc extensions of the Hindley/Milner system such as security checking and dimension inference [38].

Another particular application of CHRs includes the explanation of type improvement for type classes [32,9] such as Mark Jones' functional dependencies.

My CHR 2005 invited talk [18] gives an overview of some of the above results.

Martin Sulzmann 2006-07-19