%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Type-Level Instant Insanity
%
% Conrad Parker , February 2007
%
% This file is literate Haskell.
\documentclass{tmr}
\usepackage{amsmath}
\usepackage{xspace}
% Processing instructions for lhs2TeX
%include polycode.fmt
%options ghci -fglasgow-exts -fallow-undecidable-instances
% LaTeX macros
\newcommand\HTS{the Haskell Type System\xspace}
\def\boldroman#1{\mbox{\boldmath $\mathrm{#1}$}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{Type-Level Instant Insanity}
\author{Conrad Parker\email{conrad@@dl.kuis.kyoto-u.ac.jp}}
\begin{document}
%\maketitle
\begin{introduction}
We illustrate some of the techniques used to perform computations in \HTS
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 Haskell programming.
\end{introduction}
\section{Overview}
This article discusses an implementation of Instant Insanity, an appropriately
named puzzle game. We will first familiarize ourselves with a straightforward
Haskell solution to the puzzle, and then translate that solution so
that it is evaluated by \HTS at compile time.
By discussing the implementation of a complete solution to a problem, we
necessarily provide more than just the flavour of programming in \HTS.
Rather than simply demonstrating clever tricks, we progressively introduce
useful type-level programming features.
We introduce constructs similar to the functions, lists, maps and filters of
conventional functional programming, and in so doing make clear the basic
techniques required to construct programs in this manner.
Only after building an understanding of the syntactical oddities and
transformations involved in programming in \HTS do we consider the practical
aspects of using these techniques in conventional Haskell programming.
Familiarity with the syntax of \HTS is a prerequisite for understanding the
details of general Haskell programming. What better way to build familiarity
with something than to hack it to bits?
Through this tutorial, we hope to show that \HTS is not as scary as it first
seems.
\newpage
\section{Textbook implementation}
In a discussion of problem-solving via back-tracking,
Bird and Wadler~\cite{bird-wadler} introduce the following puzzle,
\emph{Instant Insanity}:
\begin{quotation} \noindent
It consists of four cubes, with faces coloured blue, green, red or white.
The problem is to arrange the cubes in a vertical pile such that each
visible column of faces contains four distinct colours.
\end{quotation}
\noindent
The solution provided in Listing~\ref{BW-solution} stacks the cubes
one at a time, trying each possible orientation of each cube.
%When I first read it
%% (about a week ago while I was learning Haskell LOLZ!)
%I was quite inspired by its elegance:
\begin{listing}
\begin{verbatim}
cubes = ["BGWGBR", "WGBWRR", "GWRBRR", "BRGGWW"]
-- Rotate a cube 90 degrees over its Z-axis, leaving up and down in place.
rot [u, f, r, b, l, d] = [u, r, b, l, f, d]
-- Twist a cube around the axis running from the upper-front-right
-- corner to the back-left-down corner.
twist [u, f, r, b, l, d] = [f, r, u, l, d, b]
-- Exchange up and down, front and left, back and right.
flip [u, f, r, b, l, d] = [d, l, b, r, f, u]
-- Compute all 24 ways to orient a cube.
orientations c =
[c''' | c' <- [c, rot c, rot (rot c), rot (rot (rot c))],
c'' <- [c', twist c', twist (twist c')],
c''' <- [c'', flip c'']]
-- Compute which faces of a cube are visible when placed in a pile.
visible [u, f, r, b, l, d] = [f, r, b, l]
-- Two cubes are compatible if they have different colours on every
-- visible face.
compatible c c' = and [x /= x' | (x, x') <- zip (visible c) (visible c')]
-- Determine whether a cube can be added to pile of cubes, without
-- invalidating the solution.
allowed c cs = and [compatible c c' | c' <- cs]
-- Return a list of all ways of orienting each cube such that no side of
-- the pile has two faces the same.
solutions [] = [[]]
solutions (c:cs) = [c' : cs' | cs' <- solutions cs,
c' <- orientations c,
allowed c' cs']
main = print $ solutions cubes
\end{verbatim}
\caption{The Bird-Wadler solution to Instant Insanity}
\label{BW-solution}
\end{listing}
Our task is to translate this solution into \HTS.
\section{Type-Level Implementation}
The Haskell Type System is a completely symbolic language with very few amenities.
You are swimming in a sea of atomic constants, like \boldroman{X}.
These aren't numeric constants; they do not hold a value. They simply exist,
and all you can do is create relations between them. If you want features like
numbers and arithmetic, or even boolean logic, then you have to create them yourself.
In order to discuss our implementation, we will treat \HTS as a programming
system in its own right. Although the keywords such as |data| and |class| are
named for their purpose in Haskell, when introducing them we will ignore that
purpose and provide an alternative interpretation within \HTS. Only after completing the
implementation of Instant Insanity will we relate these concepts back to
conventional Haskell programming.
Of course, \HTS wasn't explicitly designed for programming, and there are some
limitations which we'll cover later. But for now, let's jump right in!
\subsection{Type system features}
This tutorial uses the Haskell98 type system extended with multi-parameter
type-classes and undecidable instances.
We need to enable some GHC extensions to play with this type-hackery:
\begin{verbatim}
$ ghci -fglasgow-exts -fallow-undecidable-instances
\end{verbatim}
\noindent
These are included in your GHC; you just need to pass the options to
enable them, as they were not part of the Haskell98 language specification.
\subsection{Flipping out}
We are going to declare new functions called |all|, |flip|, |map| and
|filter|, so we hide the versions in Prelude.
> import Prelude hiding (all, flip, map, filter)
\subsection{|undefined| (Bottom)}
As we are working in the type system we don't actually care about the values
of any of our variables, only their types. There is one special value which
is a member of every type (i.e.~it can be ``cast'' as any type we choose). For
historical reasons it is called \emph{bottom}, and in Haskell it is written
\boldroman{undefined}.
When it is typeset here, it looks like this: |undefined|.
For example:
\begin{verbatim}
*Main> :type undefined::Int
\end{verbatim}
\eval{:t undefined:: Int}
\bigskip\\
\noindent
This simply confirms that the type of the value |undefined::Int| is |Int|.
> u = undefined
To shorten expressions later in this article, we have abbreviated
\boldroman{undefined} (|undefined|) to the variable |u|.
This is often convenient when programming in \HTS.
\subsection{Simple types}
Ok, let's get started.
We note that there are four possible colours. Rather than using arbitrary
characters to represent colours, we make some type-safe definitions.
% Using 'strict' here is a bit misleading...
% Rather than using arbitrary lists as the data structure to represent a cube,
% we make a strictly defined |Cube|.
In this problem, the colours of the faces of cubes are \emph{atomic}. They
cannot be divided any further, and it is irrelevant to the problem to define
them in terms of any other values. The puzzle is no easier if the red faces
are pink instead.
In \HTS, we use the keyword |data| to introduce atomic constants:
> data R -- Red
> data G -- Green
> data B -- Blue
> data W -- White
These constants are concrete types, which means that it is possible to
instantiate variables in these types. However, as we have not given these
types any constructors, the only valid value for each is |undefined|.
We use them to represent atomic constants in \HTS.
We can check that |undefined| is a valid value of type |R|:
\begin{verbatim}
*Main> :type undefined::R
\end{verbatim}
\eval{:type undefined::R}
\subsection{Parameterized types}
A cube is a thing that can have six faces. In \HTS, we use the keyword
|data| to introduce such a thing:
> data Cube u f r b l d
Wait a minute -- didn't we just use the keyword |data| to introduce atomic
constants? Yes, and |Cube| is also atomic. That is to say, the concept of
\emph{a thing that can have six faces} is atomic, in the context of this
puzzle. No matter how big your hammer is or how frustrated you are, it's not
within the rules of the puzzle to break down a cube into something with
more, or fewer, faces.
So, |R|, |G|, |B|, |W| and |Cube| are all atomic, but they are different
\emph{kinds} of thing.
\begin{verbatim}
*Main> :kind R
\end{verbatim}
\eval{:kind R}
\begin{verbatim}
*Main> :kind Cube
\end{verbatim}
\eval{:kind Cube}
\bigskip\\
In \HTS, the word \emph{kind} is used to describe the structure of a type,
and types must be of the same kind in order to be used in the same way.
Whereas |R| is a concrete type that we could instantiate variables in,
|Cube| is not:
\begin{verbatim}
*Main> :type undefined :: Cube
:1:13:
Kind error: `Cube' is not applied to enough type arguments
In an expression type signature: Cube
In the expression: undefined :: Cube
\end{verbatim}
The |Cube| type needs to be applied to \emph{type arguments}, namely
|u f r b l d|. If we substitute concrete types for these arguments,
the result is a concrete type. So, one way to think about |Cube| is
that it is like a function, but at the type level: it takes
\emph{types} as arguments and returns \emph{types}. We say that
|Cube| is \emph{parameterized} over the type arguments |u f r b l
d|.
Now we can use the types we prepared earlier, |R|, |G|, |B|, |W|, as
type arguments to the type-level function |Cube| to produce concrete types:
\begin{verbatim}
*Main> :type undefined :: Cube R R R R R R -- a red cube
\end{verbatim}
\eval{:type undefined :: Cube R R R R R R}
\begin{verbatim}
*Main> :type undefined :: Cube R G B R G B -- a colourful cube
\end{verbatim}
\eval{:type undefined :: Cube R G B R G B}
\begin{verbatim}
*Main> :type undefined :: Cube B W G G R G -- another cube
\end{verbatim}
\eval{:type undefined :: Cube B W G G R G}
\subsection{Type aliases}
Now we can define the actual cubes in our puzzle as ``outputs'' of the
type function |Cube|, and in order to write clear code (in \HTS) we will
create some handy aliases.
In \HTS, we use the keyword |type| to introduce type aliases:
A completely red cube:
> type CubeRed = Cube R R R R R R
A completely blue cube:
> type CubeBlue = Cube B B B B B B
The cubes available in the problem at hand:
\begin{verbatim}
cubes = ["BGWGBR", "WGBWRR", "GWRBRR", "BRGGWW"]
\end{verbatim}
> type Cube1 = Cube B G W G B R
> type Cube2 = Cube W G B W R R
> type Cube3 = Cube G W R B R R
> type Cube4 = Cube B R G G W W
\begin{verbatim}
*Main> :kind Cube1
\end{verbatim}
\eval{:kind Cube1}
We see that |Cube1| has the same \emph{kind} as the color red, |R|, has.
And indeed, |Cube1| is a concrete type:
\begin{verbatim}
*Main> :type undefined::Cube1
\end{verbatim}
\eval{:type undefined::Cube1}
\subsection{Multi-parameter type classes}
We would like to define the following transformations on |Cube|s:
\begin{verbatim}
rot [u, f, r, b, l, d] = [u, r, b, l, f, d]
twist [u, f, r, b, l, d] = [f, r, u, l, d, b]
flip [u, f, r, b, l, d] = [d, l, b, r, f, u]
\end{verbatim}
\noindent
In \HTS, we use the keyword |class| to introduce functions. At first, we
will simply introduce a collection of plain Haskell functions. These are
grouped under the parameterized type class |Transforms|:
> class Transforms u f r b l d where
> rot :: Cube u f r b l d -> Cube u r b l f d
> twist :: Cube u f r b l d -> Cube f r u l d b
> flip :: Cube u f r b l d -> Cube d l b r f u
This collection of declarations defines an interface, and that
interface consists of three functions |rot|, |twist| and |flip|.
For example, |rot| takes a |Cube| as input, and outputs a different type
of |Cube|. The exact types of these |Cube|s are related to the class
parameters.
Two different substitutions of the |class| parameters would define different
interfaces, as the resulting types of the functions |rot|, |twist| and |flip|
would be different. Hence |Transforms| is actually a class constructor --
we can use it to generate new classes, but it is not itself a concrete class
definition.
Programming in \HTS, we are only interested in the types of these functions,
which are dictated by the |class| definition. Accordingly, we don't need to
specify anything about their implementation when we create an |instance|; we
can simply declare the functions to be |undefined|.
%multi-parameter type classes are enabled by the GHC option
%\tt-fglasgow-exts\rm.
For example, we could create an instance of |Transforms| which applies only
if all six parameters (faces of cubes) are green:
> instance Transforms G G G G G G where
> rot = undefined
> twist = undefined
> flip = undefined
%It is for this reason that we pass the option
%\tt-fallow-undecidable-instances\rm{} to GHC.
However, there is no need to instantiate |Transforms| for every
possible combination of faces. We can fill in any or all parameters with
variables, which can represent any concrete type (of \emph{kind *}):
> instance Transforms u f r b l d where
> rot = undefined
> twist = undefined
> flip = undefined
We are now able to evaluate some simple type transformations, such as:
\begin{verbatim}
*Main> :type rot (undefined::Cube1)
\end{verbatim}
\eval{:type rot (undefined::Cube1)}
\begin{verbatim}
*Main> :type flip (rot (undefined::Cube1))
\end{verbatim}
\eval{:type flip (rot (undefined::Cube1))}
\begin{verbatim}
*Main> :type twist (flip (rot (undefined::Cube1)))
\end{verbatim}
\eval{:type twist (flip (rot (undefined::Cube1)))}
\bigskip\\
You can see that we can already perform some basic computations, entirely
in the type system.
Now, do you take the red cube, or the blue cube?
\subsection{Functional Dependencies}
So far we have seen how to construct simple types, and perform type
transformations that transform a parameterized type into a
differently parameterized type.
For this puzzle we will need some boolean algebra, so let's create it.
First we make the truth values:
> data True
> data False
The first boolean function we will need is |And| that relates three
values: two inputs and one output. We express the fact that the output |b| is
dependent on the two inputs |b1|, |b2| by adding the dependency annotation
|b1 b2 -> b|. We use a vertical bar to append this dependency annotation:
> class And b1 b2 b | b1 b2 -> b where
> and :: b1 -> b2 -> b
We can define |And| by simply listing out its complete truth table:
> instance And True True True where and = undefined
> instance And True False False where and = undefined
> instance And False True False where and = undefined
> instance And False False False where and = undefined
When using functional dependencies in this way, we are doing logic
programming in \HTS, using |class| to introduce type-level functions and
using the last class parameter as the ``output.''
\subsection{Lists}
We can define lists in the type system using the following atoms:
> data Nil
> data Cons x xs
The data type |Nil| represents the empty list; the |Cons| data type
is used to append an element to a list. With this syntax, |Cons x
Nil| denotes a list containing only one element; we
can use |Cons| multiple times to build longer lists. However,
this quickly becomes difficult to read. For example, the list |[R,
G, B]| would be represented by \mbox{\tt Cons R (Cons G (Cons B
Nil))\rm}.
GHC allows us to introduce an alternative infix notation to represent |Cons|.
Type-level infix operators must begin with a colon, so we choose |:::|
and define:
> data x ::: xs
>
> infixr 5 :::
The |infixr 5| here sets the precedence level; we make |:::| bind tightly so
that we do not need to use parentheses inside of lists.
Now the list |[R, G, B]| can be represented more clearly by
\mbox{\tt R ::: G ::: B ::: Nil\rm}.
%and the list of the empty list, |[[]]|, is simply \mbox{\tt Nil ::: Nil\rm}.
\subsection{Type constraints}
We can define recursive functions in \HTS using this representation of lists.
However, in order to do so we must use a
\emph{type constraint}. For a recursively defined list function, we use a type constraint to say that the value for |x ::: xs|
uses a recursive call on |xs|. In general, a type constraint is used to set
preconditions on a function; the given function definition is only valid
when the preconditions are met. By carefully constructing the constraints
you can set up a recursion, or call out to other type-level functions.
For example, to concatenate two arbitrary lists we would write:
> class ListConcat l1 l2 l | l1 l2 -> l where
> listConcat :: l1 -> l2 -> l
> instance ListConcat Nil l l where listConcat = undefined
> instance (ListConcat xs ys zs)
> => ListConcat (x ::: xs) ys (x ::: zs) where listConcat = undefined
\begin{verbatim}
*Main> :type listConcat (u:: R ::: G ::: B ::: Nil) (u:: W ::: Nil)
\end{verbatim}
\eval{:type listConcat (u:: R ::: G ::: B ::: Nil) (u:: W ::: Nil)}
\bigskip\\
Note that the type constraint, |ListConcat xs ys zs| justifies the
recursive call.
\subsection{Applyable type functions}
For this puzzle, we need to be able to do things like |flip| each of the
cubes in a list, so let's build towards something like |map|, at the type
level. First we will need a way of abstracting the application of a
type-level function, so we introduce a class |Apply|:
> class Apply f a b | f a -> b where
> apply :: f -> a -> b
The |Apply| class takes a function |f| of one argument, and an argument |a|, and
returns the application of |f| to |a|.
Unfortunately, the functions |rot|, |twist|, and |flip| that we defined earlier
are not declared at the type level; they cannot be passed to our type-level
|Apply|. If we try to do so, we end up with:
\begin{verbatim}
*Main> :type apply rot (u::Cube1)
\end{verbatim}
< apply rot (u::Cube1) :: forall u f r b l d b1.
< (Transforms u f r b l d,
< Apply (Cube u f r b l d -> Cube u r b l f d) Cube1 b1) => b1
Instead, we need to create types to name each of these operations:
> data Rotation
> data Twist
> data Flip
We defined |Apply| as a parameterized interface. Let's instantiate it for
each of our transform types:
> instance Apply Rotation (Cube u f r b l d) (Cube u r b l f d)
> where apply = undefined
> instance Apply Twist (Cube u f r b l d) (Cube f r u l d b)
> where apply = undefined
> instance Apply Flip (Cube u f r b l d) (Cube d l b r f u)
> where apply = undefined
With all these pieces in place, we can now apply our |Rotation|
function to an example cube:
\begin{verbatim}
*Main> :type apply (u::Rotation) (u::Cube1)
\end{verbatim}
\eval{:type apply (u::Rotation) (u::Cube1)}
\subsection{Map and Filter}
We can now create a function that recurses over a list and |Apply|s another
function |f| to each element. This is the type-level equivalent of
fthe |map| function from the Haskell Prelude.
> class Map f xs zs | f xs -> zs where
> map :: f -> xs -> zs
If we call |Map| over the empty list, we get an empty list:
> instance Map f Nil Nil where map = undefined
In the |Cons| case we use two type constraints: one to call |Apply| on
the head element, and one to call |Map| on the tail. The result will simply
join these two values. As we recurse down the list |x:::xs|, we build the
result |z:::zs|:
> instance (Apply f x z, Map f xs zs)
> => Map f (x ::: xs) (z ::: zs) where map = undefined
Once again, we show the |map| function in action, by mapping the
|Flip| operation on a list of two cubes:
\begin{verbatim}
*Main> :type map (u::Flip) (u:: Cube1 ::: (Cube2 ::: Nil))
\end{verbatim}
\begin{equation*}
\begin{split}
\Varid{map}&\;(\Varid{u}\mathbin{::}\Conid{Flip})\;(\Varid{u}\mathbin{::}
\Conid{Cube1}\mathbin{:::}(\Conid{Cube2}\mathbin{:::}\Conid{Nil}))\; \mathbin{::}\\
& (\mathbin{:::})\;(\Conid{Cube}\;\Conid{R}\;\Conid{B}\;\Conid{G}\;\Conid{W}\;\Conid{G}\;\Conid{B})\;((\mathbin{:::})\;(\Conid{Cube}\;\Conid{R}\;\Conid{R}\;\Conid{W}\;\Conid{B}\;\Conid{G}\;\Conid{W})\;\Conid{Nil})
\end{split}
\end{equation*}
%\eval{:type map (u::Flip) (u:: Cube1 ::: (Cube2 ::: Nil))}
%\bigskip\\
%LAYOUT%
We can build a |Filter| function similarly:
> class Filter f xs zs | f xs -> zs where
> filter :: f -> xs -> zs
> instance Filter f Nil Nil where filter = undefined
> instance (Apply f x b, Filter f xs ys, AppendIf b x ys zs)
> => Filter f (x ::: xs) zs where filter = undefined
Here we have introduced a third constraint, |AppendIf|, which takes
a boolean value |b|, a value x, and a list |ys|. The given value |x|
is appended to |ys| only if |b| is |True|, otherwise |ys| is
returned unaltered:
\label{AppendIf}
> class AppendIf b x ys zs | b x ys -> zs
> instance AppendIf True x ys (x ::: ys)
> instance AppendIf False x ys ys
Hence, |Filter| recurses down a list |x:::xs|, and builds the list |zs| by
appending only those values of |x| for which |f x| is |True|.
\subsection{List Comprehensions}
Unfortunately we cannot directly mimic list comprehensions in \HTS,
but we can translate the meaning of a given list comprehension using
the type-level list functions that we have defined.
For example, building a list of the possible orientations of a cube involves
appending a list of the possible applications of |flip|, so we will
need to be able to map over a list and append the original list. The
original list comprehension we are translating was:
\begin{verbatim}
orientations c
= [c''' | ..., c''' <- [c'', flip c'']]
\end{verbatim}
We create a |MapAppend| class in order to compose |Map| and
|ListConcat|:
%\begin{align*}
% MapAppend F [c, d]& \to [c, d] ++ Map F [c, d]
% & \to [c, d, Fc, Fd]
%\end{align*}
> class MapAppend f xs zs | f xs -> zs where
> mapAppend :: f -> xs -> zs
The |MapAppend| class has two instances:
> instance MapAppend f Nil Nil where mapAppend = undefined
> instance (Map f xs ys, ListConcat xs ys zs)
> => MapAppend f xs zs where mapAppend = undefined
Further, we will need to be able to do the same twice for |twist|:
\begin{verbatim}
orientations c
= [c''' | ..., c'' <- [c', twist c', twist (twist c')], ...]
\end{verbatim}
%\begin{align*}
% MapAppend2 F [c, d]& \to [c, d] ++ Map F (MapAppend F [c, d]) \\
% & \to [c, d] ++ Map F [c, d, Fc, Fd] \\
% & \to [c, d, Fc, Fd, FFc, FFd]
%\end{align*}
> class MapAppend2 f xs zs | f xs -> zs where
> mapAppend2 :: f -> xs -> zs
> instance MapAppend2 f Nil Nil where mapAppend2 = undefined
> instance (Map f xs ys, MapAppend f ys ys', ListConcat xs ys' zs)
> => MapAppend2 f xs zs where mapAppend2 = undefined
and three times for |rot|:
\begin{verbatim}
orientations c
= [c''' | c' <- [c, rot c, rot (rot c), rot (rot (rot c))], ...]
\end{verbatim}
%\begin{align*}
%MapAppend3 F [c,d]& \to [c, d] ++ Map F (MapAppend2 F [c, d]) \\
% & \to [c, d] ++ Map F [c, d, Fc, Fd, FFc, FFd] \\
% & \to [c, d, Fc, Fd, FFc, FFd, FFFc, FFFd]
%\end{align*}
> class MapAppend3 f xs zs | f xs -> zs where
> mapAppend3 :: f -> xs -> zs
> instance MapAppend3 f Nil Nil where mapAppend3 = undefined
> instance (Map f xs ys, MapAppend2 f ys ys', ListConcat xs ys' zs)
> => MapAppend3 f xs zs where mapAppend3 = undefined
\subsection{Orientations}
The full list comprehension for generating all possible orientations of a
cube builds upon all combinations of |rot|, |twist| and |flip|:
\begin{verbatim}
orientations c =
[c''' | c' <- [c, rot c, rot (rot c), rot (rot (rot c))],
c'' <- [c', twist c', twist (twist c')],
c''' <- [c'', flip c'']]
\end{verbatim}
\noindent
We will implement Orientations as an |Apply|able type function. In turn, it
is defined in terms of applications of |Rotation|, |Twist| and |Flip|,
invoked via the various |MapAppend| functions:
> data Orientations
>
> instance (MapAppend Flip (c ::: Nil) fs, MapAppend2 Twist fs ts,
> MapAppend3 Rotation ts zs)
> => Apply Orientations c zs
> where apply = undefined
For any |Cube|, this function generates the 24 possible orientations:
%\begin{verbatim}
%*Main> :type apply (u::Orientations) (u::Cube1)
%\end{verbatim}
%\eval{:type apply (u::Orientations) (u::Cube1)}
\begin{verbatim}
*Main> :type apply (u::Orientations) (u::Cube1)
\end{verbatim}
< apply (u::Orientations) (u::Cube1) ::
< (:::) (Cube B G W G B R) ((:::) (Cube R B G W G B)
< ((:::) (Cube G W B B R G) ((:::) (Cube B G R G B W)
< ((:::) (Cube W B G R G B) ((:::) (Cube G R B B W G)
< ((:::) (Cube B W G B G R) ((:::) (Cube R G W G B B)
< ((:::) (Cube G B B R W G) ((:::) (Cube B R G B G W)
< ((:::) (Cube W G R G B B) ((:::) (Cube G B B W R G)
< ((:::) (Cube B G B G W R) ((:::) (Cube R W G B G B)
< ((:::) (Cube G B R W B G) ((:::) (Cube B G B G R W)
< ((:::) (Cube W R G B G B) ((:::) (Cube G B W R B G)
< ((:::) (Cube B B G W G R) ((:::) (Cube R G B G W B)
< ((:::) (Cube G R W B B G) ((:::) (Cube B B G R G W)
< ((:::) (Cube W G B G R B) ((:::) (Cube G W R B B G)
< Nil)))))))))))))))))))))))
\subsection{Stacking Cubes}
%Now we start to get more of a flavour of how type constraints are used as
%combinators when programming in \HTS.
Given two cubes |(Cube u1 f1 r1 b1 l1 d1)| |(Cube u2 f2 r2 b2 l2
d2)|, we now want to check that none of the corresponding visible
faces are the same colour: the front sides |f1| and |f2| are not
equal, and the right sides |r1| and |r2| are not equal, and so
on. In short, we want to determine whether:
\[(|f1| \neq |f2|) \wedge (|r1| \neq |r2|) \wedge (|b1| \neq |b2|) \wedge (|l1| \neq |l2|)\]
In order to do this, we will first need to define the $\neq$ relation
for all four colours. Given two cubes, we can then apply this relations
to each pair of visible faces to get four boolean values. To check
that all of these are True, we will construct a list of those four values,
and then write a generic list function to check if all elements of a list
are True.
\subsection{Not Equal}
To define the $\neq$ relation, we introduce a new class:
> class NE x y b | x y -> b where
> ne :: x -> y -> b
We are going to use |NE| to instantiate type comparisons for the faces of
our cube. Recall that these faces are of the atomic types |R|, |G|, |B|, |W|,
and we have not yet defined any relation between these atomic types.
> instance NE R R False where ne = undefined
> instance NE R G True where ne = undefined
> instance NE R B True where ne = undefined
> instance NE R W True where ne = undefined
> instance NE G R True where ne = undefined
> instance NE G G False where ne = undefined
> instance NE G B True where ne = undefined
> instance NE G W True where ne = undefined
> instance NE B R True where ne = undefined
> instance NE B G True where ne = undefined
> instance NE B B False where ne = undefined
> instance NE B W True where ne = undefined
> instance NE W R True where ne = undefined
> instance NE W G True where ne = undefined
> instance NE W B True where ne = undefined
> instance NE W W False where ne = undefined
Note that our class |NE| is very different from the class |Eq| defined in
Haskell:
\begin{verbatim}
*Main> :info Eq
class Eq a where
(==) :: a -> a -> Bool
(/=) :: a -> a -> Bool
-- Imported from GHC.Base
...
\end{verbatim}
Whereas |Eq| is used to describe types for which it is possible to compare
\emph{instances} for equality, |NE| directly compares types.
\par\break
\subsection{All}
Now, we define a function |all| to check if all elements of a list
are True.
> class All l b | l -> b where
> all :: l -> b
>
> instance All Nil True where all = undefined
> instance All (False ::: xs) False where all = undefined
> instance (All xs b) => All (True ::: xs) b where all = undefined
The constraint |(All xs b) => All (True ::: xs) b|
says that the output |b| of |All (True ::: xs) b| has the same value as
the output |b| of |All xs b|; ie. that if the head of the list is |True|,
then the value of |All| is determined by the rest of the list.
Once again, we can check that |all| behaves as we expect:
\begin{verbatim}
*Main> :type all (u::Nil)
\end{verbatim}
\eval{:type all (u::Nil)}
\begin{verbatim}
*Main> :type all (u:: False ::: Nil)
\end{verbatim}
\eval{:type all (u:: False ::: Nil)}
\begin{verbatim}
*Main> :type all (u:: True ::: False ::: Nil)
\end{verbatim}
\eval{:type all (u:: True ::: False ::: Nil)}
\begin{verbatim}
*Main> :type all (u:: True ::: True ::: True ::: Nil)
\end{verbatim}
\eval{:type all (u:: True ::: True ::: True ::: Nil)}
\subsection{Compatible}
We can now write the compatibility check in the \HTS, that
corresponds to the original \texttt{compatible} function:
\begin{verbatim}
visible [u, f, r, b, l, d] = [f, r, b, l]
compatible c c' =
and [x /= x' | (x, x') <- zip (visible c) (visible c')]
\end{verbatim}
\noindent
We introduce a new |Compatible| class. It should check that no
corresponding visible faces are the same colour.
> class Compatible c1 c2 b | c1 c2 -> b where
> compatible :: c1 -> c2 -> b
We will do this by evaluating the relationship |NE| for each pair of
corresponding visible faces, giving four booleans |bF|, |bR|, |bB|, and |bL|.
Whether or not the two |Cube|s are
compatible is then determined by |All (bF ::: bR ::: bB ::: bL ::: Nil)|.
> instance (NE f1 f2 bF, NE r1 r2 bR, NE b1 b2 bB, NE l1 l2 bL,
> All (bF ::: bR ::: bB ::: bL ::: Nil) b)
> => Compatible (Cube u1 f1 r1 b1 l1 d1) (Cube u2 f2 r2 b2 l2 d2) b
> where compatible = undefined
A completely red cube is obviously compatible with a completely blue cube:
\begin{verbatim}
*Main> :type compatible (u::Cube R R R R R R) (u::Cube B B B B B B)
\end{verbatim}
\eval{:type compatible (u::Cube R R R R R R) (u::Cube B B B B B B)}
\bigskip\\
whereas if we paint their front sides green then they are no longer
compatible:
\begin{verbatim}
*Main> :type compatible (u::Cube R R G R R R) (u::Cube B B G B B B)
\end{verbatim}
\eval{:type compatible (u::Cube R R G R R R) (u::Cube B B G B B B)}
\subsection{Allowed}
The above |Compatible| class checks a cube for compatibility with another
single cube. In the puzzle, a cube needs to be compatible with all the other
cubes in the pile.
\begin{verbatim}
allowed c cs = and [compatible c c' | c' <- cs]
\end{verbatim}
\noindent
We write a class to check for compatibility with each of a list of cubes.
This class generalizes |Compatible| over lists:
> class Allowed c cs b | c cs -> b where
> allowed :: c -> cs -> b
> instance Allowed c Nil True where allowed = undefined
>
> instance (Compatible c y b1, Allowed c ys b2, And b1 b2 b)
> => Allowed c (y ::: ys) b where allowed = undefined
%\begin{verbatim}
%*Main> :type allowed (u::CubeRed) (u:: CubeRed ::: Nil)
%\end{verbatim}
%\eval{:type allowed (u::CubeRed) (u:: CubeRed ::: Nil)}
%\begin{verbatim}
%*Main> :type allowed (u::CubeRed) (u:: CubeBlue ::: Nil)
%\end{verbatim}
%\eval{:type allowed (u::CubeRed) (u:: CubeBlue ::: Nil)}
Sure enough, we can now test the |allowed| function:
\begin{verbatim}
*Main> :type allowed (u::CubeRed) (u:: CubeBlue ::: CubeRed ::: Nil)
\end{verbatim}
\eval{:type allowed (u::CubeRed) (u:: CubeBlue ::: CubeRed ::: Nil)}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Solution}
We are now ready to tackle the implementation of |solutions|:
\begin{verbatim}
solutions [] = [[]]
solutions (c:cs) = [c' : cs' | cs' <- solutions cs,
c' <- orientations c,
allowed c' cs']
\end{verbatim}
\noindent
We will create a corresponding class |Solutions|, which takes a list of
|Cube|s as input, and returns a list of possible solutions, where each solution is a list
of |Cube|s in allowed orientations.
> class Solutions cs ss | cs -> ss where
> solutions :: cs -> ss
The base case for |Solutions| is the list containing the empty list, |[[]]|, which we
represent by |Nil ::: Nil|. The recursive step considers all orientations of
the topmost |Cube|:
> instance Solutions Nil (Nil ::: Nil)
> where solutions = undefined
> instance (Solutions cs sols, Apply Orientations c os,
> AllowedCombinations os sols zs)
> => Solutions (c ::: cs) zs
> where solutions = undefined
The |AllowedCombinations| class recurses across the solutions so far, checking each
against the given orientations.
> class AllowedCombinations os sols zs | os sols -> zs
> instance AllowedCombinations os Nil Nil
> instance (AllowedCombinations os sols as, MatchingOrientations os s bs,
> ListConcat as bs zs)
> => AllowedCombinations os (s ::: sols) zs
Finally, the |MatchingOrientations| class recurses across the orientations of the new cube, checking
each against a particular solution |sol|.
> class MatchingOrientations os sol zs | os sol -> zs
> instance MatchingOrientations Nil sol Nil
> instance (MatchingOrientations os sol as,
> Allowed o sol b, AppendIf b (o ::: sol) as zs)
> => MatchingOrientations (o ::: os) sol zs
If the orientation is allowed, then the combination |o| is added to
the existing solutions |sol|, by forming the type |o ::: sol|.
Note that we have not been able to make use of the previously defined
|Filter| because it requires a one-argument |Apply|able function. As we
lack currying, we are unable to construct such a function on the fly.
However, we can make use of the more generic |AppendIf| (defined on page
\pageref{AppendIf}) to handle the filtering constraint.
%We first test that solutions correctly finds no solutions for two entirely
%blue cubes:
%
%\begin{verbatim}
%*Main> :type solutions (u::Cons CubeBlue (Cons CubeBlue Nil))
%\end{verbatim}
%\eval{:type solutions (u::Cons CubeBlue (Cons CubeBlue Nil))}
Finally, we can solve the puzzle for the given cubes:
> type Cubes = (Cube1 ::: Cube2 ::: Cube3 ::: Cube4 ::: Nil)
%\begin{verbatim}
%*Main> :type solutions (u::Cubes)
%\end{verbatim}
%\eval{:type solutions (u::Cubes)}
\begin{verbatim}
*Main> :type solutions (u::Cubes)
\end{verbatim}
< solutions (u::Cubes) ::
< (:::) ((:::) (Cube G B B R W G) ((:::) (Cube R G R W B W)
< ((:::) (Cube R W G B R R) ((:::) (Cube W R W G G B) Nil))))
< ((:::) ((:::) (Cube G B B W R G) ((:::) (Cube W R G B W R)
< ((:::) (Cube R G W R B R) ((:::) (Cube B W R G G W) Nil))))
< ((:::) ((:::) (Cube G W B B R G) ((:::) (Cube R B G R W W)
< ((:::) (Cube R R W G B R) ((:::) (Cube W G R W G B) Nil))))
< ((:::) ((:::) (Cube G R B B W G) ((:::) (Cube W W R G B R)
< ((:::) (Cube R B G W R R) ((:::) (Cube B G W R G W) Nil))))
< ((:::) ((:::) (Cube G R W B B G) ((:::) (Cube R W B G R W)
< ((:::) (Cube R B R W G R) ((:::) (Cube W G G R W B) Nil))))
< ((:::) ((:::) (Cube G W R B B G) ((:::) (Cube W B W R G R)
< ((:::) (Cube R R B G W R) ((:::) (Cube B G G W R W) Nil))))
< ((:::) ((:::) (Cube G B R W B G) ((:::) (Cube R R W B G W)
< ((:::) (Cube R G B R W R) ((:::) (Cube W W G G R B) Nil))))
< ((:::) ((:::) (Cube G B W R B G) ((:::) (Cube W G B W R R)
< ((:::) (Cube R W R B G R) ((:::) (Cube B R G G W W) Nil))))
< Nil)))))))
Changing the order of backtracking steps changes the order of solutions.
For comparison, here is the solution generated by the pure Haskell version:
\begin{verbatim}
[["GBWRBG","WGBWRR","RWRBGR","BRGGWW"],
["GBRWBG","RRWBGW","RGBRWR","WWGGRB"],
["GWRBBG","WBWRGR","RRBGWR","BGGWRW"],
["GBBRWG","RGRWBW","RWGBRR","WRWGGB"],
["GRBBWG","WWRGBR","RBGWRR","BGWRGW"],
["GWBBRG","RBGRWW","RRWGBR","WGRWGB"],
["GBBWRG","WRGBWR","RGWRBR","BWRGGW"],
["GRWBBG","RWBGRW","RBRWGR","WGGRWB"]]
\end{verbatim}
\section{Using types in Haskell}
\label{Haskell}
Now that we've seen how to use \HTS to solve a puzzle, let's review what it
was actually designed for: ensuring that your programs make sense. The
syntax of \HTS lets you tell the compiler what your program must or must not
do, while also giving you enough flexibility to implement useful shared and
extensible interfaces.
%It is more powerful than the na\"ive view of a type system as as simply some
%"metadata attached to values".
Let's review the features of \HTS from a Haskell programming perspective.
\subsection{Keywords}
%\emph{|undefined| (Bottom)
The most straightforward way to define your own types is with the keyword
\emph{data}. You can use this to define simple types or to introduce
structured records.
\emph{Type aliases} are a handy form of abbreviation; for example the Prelude
provides |type Rational = Ratio Integer|, to make code that manipulates
rational numbers easier to read and write; under the hood, code that works
with |Rational|s is actually dealing with the |Ratio Integer| type.
This is different from |newtype| which declares an entirely new type that
cannot be used in the same contexts.
\emph{Parameterized type-classes}, introduced by the keyword |class|, are
used to provide common interfaces for existing types. These interfaces are
composed of \emph{methods}, which may be functions or constant values. An
|instance| of a type-class simply provides an implementation of the class
methods. You can also provide default methods in a |class| declaration,
which are used unless overridden in an |instance|.
\subsection{Haskell98 features}
\emph{Parameterized types} are used to wrap types in general interfaces.
You use this technique when you want to ensure that you can't accidentally
use two variants of a parameterized type in the same call; \HTS ensures that
they are incompatible. You can also use this to create tainted versions of
existing types, in order to quarantine data that has come from untrusted
sources.
\emph{Type constraints}, introduced by |=>|, are often used to provide
sensible pre-conditions.
For example, the Haskell Prelude declares the type-class |Real| with the
constraint \mbox{|class (Num a, Ord a) => Real a|}, which expresses that you
can only try to implement the interface for |Real| for types which are
numeric and have an ordering; \HTS first ensures that that you have already
implemented |Num| and |Ord|.
When reading Haskell code, you will notice that type constraints can occur
in data and function definitions, not just in class instances.
Type constraints can also be used more creatively to encode post-conditions,
if these conditions are encoded into the function types.
For example, Kyselyov's Dependently Typed Append~\cite{oleg-dtype-append},
implements a list append with the assurance that the length of the output
list is the sum of the lengths of the input list.
\subsection{Extensions}
Some of the language features used in this tutorial are not part of the
Haskell98 specification, but are widely supported by Haskell compilers.
When building with GHC, these extensions can be enabled with the options
\tt\mbox{-fglasgow-exts}\rm~\cite{ghc-exts}.
The simplest of these extensions is the use of |data| types with no
constructors, such as
> data Red
> data Blue
As these types can only contain the value |undefined|, they are not much use
on their own. However, they can be used to construct other, more complex
types, and can be used as \emph{phantom types}~\cite{wiki-phantom}.
\emph{Multi-parameter type-classes} allow you to specify an interface which
can behave differently for each combination of ``input'' types. This is usually
used together with \emph{functional dependencies}~\cite{hallgren}, which make
it easier for the type-checker to infer type relationships, and make the
code easier to read. We enable the GHC option
\tt\mbox{-fundecidable-instances}\rm~\cite{ghc-exts}
to allow general recursion at the type-level.
GHC allows empty class declarations (with a warning), so the definitions in
this tutorial which specify |where something = undefined| are actually
unnecessary. However, we left them in in order to retain some semblance of
connection to conventional Haskell programming.
\section{Conclusion}
We have seen how to use \HTS as a programming language to solve a given
problem. Of course, its real purpose is not to solve problems directly, but
to express constraints on the behaviour of a system in Haskell. The type
level features we have seen allow us to express the pre- and post-conditions
of functions. By expressing these constraints in the type system, the compiler
statically verifies that the produced code operates as required, without
the need for run-time checks.
We reiterate that familiarity with the syntax of \HTS is a prerequisite for
general Haskell programming.
With a solid understanding of type and type-class parameterization, type
constraints and dependencies, you should be well on your way to understanding
the interfaces of interesting and useful types.
This tutorial introduced the most widely used type-level features in general
Haskell programming, extending Haskell98 with multi-parameter
type-classes and undecidable instances.
If you wish to go further with type-level programming there are many
interesting extensions to \HTS~\cite{ghc-exts}, and more advanced type systems
research explores topics like program verification and proof carrying code.
~\cite{wiki-types, oleg-types}.
%What better way to build familiarity with something than to hack it to bits?
Please enjoy hacking in \HTS, and wield it wisely in your program designs.
\section{Acknowledgements}
Thanks to Simon Horman, Patryk Zadarnowski, Shane Stephens and Wouter
Swierstra for their feedback on drafts of this article.
\section{About the author}
Conrad Parker (kfish on \#haskell) is a PhD student at Kyoto University.
Originally from Sydney, he graduated from UNSW with degrees in
Mathematics and Computer Engineering.
Hobbies include computer music and Japanese language.
\bibliography{instant-insanity}
\end{document}