This is Tic Tac Type. The long version. I presented this content as a talk at YOW! LambdaJam 2014, but like most talks there is weeks of research, code, interesting asides and deeper explanation that can not be accomodated in a 30 minute talk. This article is an attempt to capture that.

Tic Tac Toe

To the uninitiated, dependent types and programming proofs can appear confronting and difficult to understand. To ease the introduction and explanation of these topics we are going to use the hopefully familiar (or if not, fairly straight forward to learn) game Tic Tac Toe [1].

Tic Tac Toe is a basic pencil and paper game played between two opponents, X and O. Played on a 3 x 3 grid, players play in turn by marking a position on the grid until one of the players can win by marking 3 positions in a line, or the game is drawn when there are no remaining squares on the board.

Whose turn is it?

Lets look at a game.

 x |   |
-----------
 o | o | x
-----------
 x |   |

So whose turn is it?

There are a number of strategies for how you could quickly work out who should play next on this game board. A simple mechanism may be just counting the number of moves on the board:

• There have been 3 x moves made.
• There have been 2 o moves made.
• Given that players must make moves in turn, no one should ever have played more than 1 move more than their opponent.
• Therefore it must be o to play next.

From this, it would not be difficult to write a program that given a board would tell us whose turn it is. But we want to do better. We want to ensure, at compile time, that only the correct player can make a move.

“Data is validated with respect to other data. If types are to capture valid data precisely, we must let them depend on terms.” - Conor McBride, Winging It [2]

McBride’s key insight here is that validation is always context dependent. The ability to validate who can play on a given board is dependent on the value of the board in question. And this is a core motivation for dependent types, we want to be able to make these value dependent assertions in our types.

So whose turn is it? Lets find out by building up the game a step at a time. In this naive example, the only property we want to verify is the notion of whose turn it is, so using some pseudo type notation we will express this as Board { Player }, where the player lets us know whose turn it currently is.

If we start with an empty board.

   |   |
-----------
   |   |
-----------
   |   |

Board { x }

And each time we make a move, we want to update the type of the board to reflect whose turn it is.

 x |   |
-----------
   |   |
-----------
   |   |

Board { o }

As the game continues, we can see whose turn it is without ever looking at the actual board.

 x |   |
-----------
   | o |
-----------
   |   |

Board { x }

The Board type would allow us to construct move functions that can only be called by the correct player.

 x |   |
-----------
   | o |
-----------
 x |   |

Board { o }

It is worth noting the type of the board undergoes only a simple transition at each move.

 x |   |
-----------
 o | o |
-----------
 x |   |

Board { x }

We are establishing an invariant that is carried in the type and does not need to be re-calculated from the value each time, we just transform the type at each step.

 x |   |
-----------
 o | o | x
-----------
 x |   |

Board { o }

In terms of values in haskell this transformation may look something like:

data Player = X | O
data Board = Board Player

next :: Player -> Player
next X = O
next O = X

move :: Board Player -> Board Player
move (Board p) = Board (next p)

But what we need is functions that operate on types, then we could also write our type level transformation in such a straight forward manner. And this is our motivation for dependently-typed languages.

To extends this example, we will temporarily invent a new language haskell’, where we can remove this distinction between values and types, directly expressing our “whose turn is it” constraint in our Board type.

data Player = X | O
data Board { Player }  = Board

next :: Player -> Player
next X = O
next O = X

move :: Board p -> Board (next p)

In haskell’, we have declared a function move that takes a board with player p to play next, and returns a board with the next player. We have shown the utmost contempt for :: that normally separates out our values from our types. Embedding a Player value in our Board type, and we have applied a value level function on Player at the type level to obtain a new Board type.

This disreguard for :: is what is meant by having a single term language for both types and values. We get to treat types and values equally, manipulating them in the same language.

If this was a step too far, don’t panic (yet), just take it as a rough guide to where we are heading with our look at dependent types.

While haskell’ is a made up language, it is possible to express this in haskell with a number of extensions in enabled (DataKinds, Gadts, TypeFamilies and KindSignatures all contribute to dependent types in Haskell), but we want something a little more elegant to explain these concepts. Idris is a language built with dependent types as a first class citizen, and provides us with a nice platform to continue our investigation of using dependent types to build a production quality game of tic-tac-toe.

Idris a Primer

Idris syntax has a significant Haskell influence. We are going to rely on that similarity to start introducing Idris syntax and concepts.

Note that this is not a complete introduction to Idris syntax, just enough to continue on. For the a more compete treatment try the Idris tutorial

Data Types and Functions

Idris has syntax for algebraic(-ish) data types, that is almost identical to Haskell. For example, lets compare how we would declare the player data type for out Tic-Tac-Type game.

Haskell

data Player =
  X | O

Idris

data Player =
  X | O

So far, so good, we have exactly the same code. So how aboat a function that gives us the opposite player:

Haskell

next :: Player -> Player
next X = O
next O = X

Idris

next : Player -> Player
next X = O
next O = X

Our first (albeit minor) differents. In Haskell type signatures are declared ::, where as in Idris, they are declared with :. Other than that, we can declare functions and pattern match, in the similar ways.

Idris also has type-classes - kind-of anyway, they are actually quite different to type-classes in Haskell, but syntactically they look the same, and for the point of this discussion can be treated in a similar way:

Haskell

instance Show Player where
  show X = "x"
  show O = "o"

Idris

instance Show Player where
  show X = "x"
  show O = "o"

Of course in haskell we could also write deriving Show, but Idris does not yet have automatic instance derivation.

A slightly more complicated type is List, which again get declared much how it would in Haskell.

Haskell

data List a
  = Nil
  | a :. List a

Idris

data List a
  = Nil
  | (:.) a List a

The only point worth noting here is that we were not able to use infix notation when declaring the symbolic data constructor.

Fixity declarations work the same way:

Haskell

infixr 7 :.

Idris

infixr 7 :.

Dependent Types in Idris

idris

Correspondence

Curry-Howard ….. Logic…..

Building Programs with Types: An Intuition

There is a cadence to doing so. Build up to strong guarantees, and relax constraints (whilst retainging guarantees).

Value Level Tic Tac Type

values are easy

Types and Proofs

gain knowledge through pattern matching

Constraints for Better APIs

apis are better

Break on Through to the Other Side

Type Level Tic Tac Type

Positive Types

Type Level Tests

Existentals for Free

information hiding

Effect Handlers

io monads vs effects

Rules as Effects

games rules

Interaction

Single Player cli Tic Tac Type

Constraints are Context Dependent

Multi Player Tic Tac Type

Restoring Context

Multi Player Tic Tac Type

Network Programming in Idris

networks concurrency?

Reflection

Type Systems

Proof by Parametricity vs Dependent Types

Haskell vs Idris

Future

References

ref

Scratch Pad

Some code

{-# LANGUAGE OverloadedStrings #-}
module Fred (afasf) where

import Data.Text (Text, unpack)
import qualified Date.Text.IO as IO

data Fred = Fred Text


-- FIX fasfasf
afasf :: [Text]
afasf = ["ads"]

asf = 1314
asf = error "todo"

[1] Of course, where I am from Tic Tac Toe is more correctly known as Naughts and Crosses, but as that doesn’t pun quite as well, we will let this slight against our english dialect go without punishment this time.

[2] McBride’s Winging It explanations are exceptional, and if you haven’t looked at the diagrams (or his ICFP keynote on a closely related theme) you should do it now.