Mike's World-O-Programming

Ahh, summer! A time for backyard barbeques, ice cold beer, baseball games, and playing with experimental Haskell type system extensions. Or in my case, just the latter. In this article I'll show you how to compute factorials using Haskell's type system, i.e. at compile time.

Why would we want to do this? you may well ask. The real reason is "because it's neat". This is a really beautiful construction; it took my breath away when I figured it out. But another reason is that the techniques I'll illustrate are useful in many other contexts. For instance, you can use something like this to define a data type of a list which carries its length around with it (so that e.g. taking the head of an empty list is a compile-time error). This is very powerful; the more errors you can check at compile-time, the better.

Nothing in this article is even remotely original. The direct inspiration for it came from a blog post by Brent Yorgey, which I've shamelessly stolen from and extended (thanks, Brent!). The indirect inspiration was from some comments on my previous blog post on Scala, which suggested that I look at a paper on embedding object-oriented programming in Haskell. That paper, called Haskell's Overlooked Object System, by Oleg Kiselyov and Ralf Lammel, is an amazing piece of work. In order to understand it fully, though, you first have to read another paper called Strongly Typed Heterogeneous Collections, by Oleg, Ralf and Keean Schupke. So that's what I did, and in the process learned quite a bit, which I'll use to good effect below. Both of these papers are strongly recommended if you're ready for them and if you enjoy having your mind blown.

To understand this article you need to know Haskell up to and including polymorphic types and (single parameter) type classes. I'll explain everything else as we go. If you want to run the examples you'll need the GHC Haskell compiler (Hugs may also work, but I haven't tried it). I used GHC version 6.12.1 to test this code.