Fun with type functions

Tony Hoare has always been a leader in writing down and proving properties of programs. To prove properties of programs automatically, the most widely used technology today is by far the ubiquitous type checker. Alas, static type systems inevitably exclude some good programs and allow some bad ones. This dilemma motivates us to describe some fun we’ve been having with Haskell, by making the type system more expressive without losing the benefits of automatic proof and compact expression.

Haskell’s type system extends Hindley-Milner with two distinctive features: polymorphism over type constructors and overloading using type classes. These features have become integral to Haskell, and they are widely used and appreciated. More recently, Haskell has been enriched with type families, which allows functions on types to be expressed as straightforwardly as functions on values. This facility makes it easier for programmers to effectively extend the compiler by writing functional programs that execute during type-checking.

This paper gives a programmer’s tour of type families as they are supported in GHC today.

• wiki page for comment and discussion
• source code
• slides