# 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.

### 1 Comment

1. #### jphaas

/  1 November, 2012

Fyi it looks like the article in question now lives here: http://www.haskell.org/wikiupload/d/dd/TMR-Issue8.pdf

• ## Status

• @furan Solidarity man. I'm kicking it in Renton, it's Ahead of the Curve! 1 day ago
• @midnite_runr Looking around, I’d say somewhere before the first round of bypass/fix. 3 days ago
• Bad: projects which leave build artifacts in the source directory. Worse: entire language platforms which do this. 5 days ago
• @halvarflake Neat fact, the zlib source has dirs like "amiga" and "qnx." It also has an "old" dir which contains "os2," but not "amiga" ! 1 week ago
• Ok friends, I've got Verifiable C, so what should I verify? A data structure? An algorithm? *morphs into powerful d… twitter.com/i/web/status/1… 1 week ago