Programming in the Haskell Type System

In The Monad.Reader Issue 8 contains a highly amusing article by Conrad Parker titled Type-Level Instant Insanity. From the abstract:

We illustrate some of the techniques used to perform computations in the Haskell Type System by presenting a complete type-level program. Programming at this level is often considered an obscure art with little practical value, but it need not
be so. We tame this magic for the purpose of practical Haskel l programming.

It’s a bold claim, and the article lives up to it.

The basic idea isn’t as bad as you might first think. Here are the major ideas:

  1. The Haskell Type System allows for types that contain information (for instance, parameterized data types contain information in their parameters).
  2. You can instantiate any type by using the Haskell undefined value, which is a member of every type, and can thus be used as a vehicle for moving typed data around.
  3. Functions can be used to cast undefined from one type to another, and can therefore be used to “act” on typing information.

Here’s an example from the article, which I present here in the hopes that it will motivate you to read the paper:

Begin by defining some empty types, which we will use to represent colors:

data R -- Red
data G -- Green
data B -- Blue
data W -- White

We now define a parameterized data type that will represent a 6-sided cube, where each face is colored:

data Cube u f r b l d

The cube’s typing gives us a way for orienting the cube. By convention, the u parameter gives us the color of the top of the cube, f is the front, r the right, b the back, l the left, and d the bottom.

Of course, we might want a function that can “rotate” the cube. Easy:

rot :: Cube u f r b l d -> Cube u r b l f d
rot c = undefined

Isn’t that cute?

The paper goes on to do some very cool things. A very good read for people who want to practice the art of thinking in Haskell.

Leave a comment

1 Comment

  1. jphaas

     /  1 November, 2012

    Fyi it looks like the article in question now lives here:

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: