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:
- The Haskell Type System allows for types that contain information (for instance, parameterized data types contain information in their parameters).
- You can instantiate any type by using the Haskell
undefinedvalue, which is a member of every type, and can thus be used as a vehicle for moving typed data around.
- Functions can be used to cast
undefinedfrom 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.