I recently had occasion to screw around Haskell’s type system. The end goal was to produce a Tic-tac-toe game in which all type-correct moves are legal and where all illegal moves produce type errors. I decided call the following moves *illegal*

- attempts to move on a cell already occupied
- attempts to make a move on a game that has already been won

While it does not make sense to compile the program into an executable the game is quite “playable” from the `ghci` REPL. The code is up on github [1].

In fact, Haskell’s type system, with the `UndecidableInstances` extension is Turing complete, so it isn’t a surprise that such a thing is possible. But type level programming has its own set of rules and I had a lot of fun figuring things out in such a foreign domain (*Type-Level Instant Insanity* [2] was extremely helpful). This post is about some of the things I observed.

**Tuples are the type-level lists**

This seems obvious now that I say it, since a tuple is the most straightforward way to represent a list of types. However, the direct way to do so is not very useful — instead of encoding the types `A`, `B`, `C` as the tuple type `(A, B, C)` it is clearer to represent them using the usual recursive cons idiom: `(A, (B, (C, ())))`. Here `()` is the *nil* element and `cons X Y` is `(X, Y)`.

**Functional dependencies**

Haskell normally doesn’t allow typeclasses on more than one type. Adding proper functional dependencies can fix this [3]. A multi-parameter typeclass is essentially a n-ary relation between types and a functional dependency constrains the relations that a multi-parameter typeclass can represent. This has interesting consequences when programming with types.

The functional dependency in `X a b c | a b -> c` constrains the relation it defines by forcing `c` to be a function of `a` and `b`. This can be used to defined type-level functions. Specifically, a function that maps two types to a third type can be represented just like the typeclass `X` in the example above. The *body* of the function can then be defined as a bunch of instance declarations. If you’re doing something like Peano arithmetic and representing, for instance, `2` by the type `S (S ())` (`S` is a type constructor here), you can implement addition as shown below:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-} data S x class Add x y z | x y -> z where add :: x -> y -> z instance Add () x x where add = undefined instance (Add x y z) => Add (S x) y (S z) where add = undefined

The functional dependency in `Add` states that the *output* of `Add` is a function of the first two types, which is correct. Note how we’re building up the induction.

I had a hard time figuring out how predicates like “two things are *foo* if they are not *bar*” are to be represented. The reverse was easy, you use a context — `instance (Foo x, Foo y) => Bar x y`, but there isn’t any way in Haskell to say `instance (NOT Foo x, Not Foo y) => Bar x y`. If you think about it, there is no reason to have such a feature either — the only reason for saying “if `x` is in the typeclass `X` then it is also in the typeclass `Y`” is to be able to use `X`‘s functions in defining `Y`‘s, so having “`x` is not in the typeclass `X`” in the context is absolutely useless! The solution (which I read in [2]) is to instead have such predicates “return” a type (which is a *value* in this weird world we’re working in). For better readability, defining two types, `data T` and `data F` for this purpose is useful. [1], for instance, is littered with `instance`s like

-- When a is X then it isn't Y and vice versa. Silly example, but I -- think it demonstrates the point instance (X a T) => Y a F instance (X a F) => Y a T

**Inverted Induction**

Finally, the way you write “function bodies” at the type level is a bit different. Instead of breaking down a function into smaller bits and then recursion on those, you conditionally build smaller structures into larger structures. For instance, to check if an element is in a list, you say “if the object `o` is in a list `l` or if `x == o`then it is in the list `cons x l` for all x”. It isn’t any different really, once you get used to it.

—

[1] https://raw.github.com/sanjoy/Snippets/master/TicTacToe.hs

[2] http://www.haskell.org/wikiupload/d/dd/TMR-Issue8.pdf

[3] http://www.haskell.org/haskellwiki/Functional_dependencies