Type-Safe Tic-tac-toe

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 instances 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 == othen 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

Advertisements
This entry was posted in Computers and tagged , , . Bookmark the permalink.

Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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 )

Google+ photo

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

Connecting to %s