First version almost finished

19 files changed, 882 insertions, 61 deletions

diff --git a/paper/While/Common.dcl b/paper/While/Common.dcl
index 6945c08..c2d58d4 100644
--- a/paper/While/Common.dcl
+++ b/paper/While/Common.dcl
@@ -32,6 +32,7 @@ instance toString Error
 (<+) infixr 5 :: a b -> String | toString a & toString b
 
 ($) infixr 0 :: (a -> b) a -> b
+(on) infix 0 :: (b -> c) (a a -> b) -> (a a -> c)
 
 (*>) infixl 4 :: (f a) (f b) -> f b | Applicative f
 (<*) infixl 4 :: (f a) (f b) -> f a | Applicative f
diff --git a/paper/While/Common.icl b/paper/While/Common.icl
index 4f6e4c4..2c28933 100644
--- a/paper/While/Common.icl
+++ b/paper/While/Common.icl
@@ -28,6 +28,9 @@ where
 ($) infixr 0 :: (a -> b) a -> b
 ($) f x = f x
 
+(on) infix 0 :: (b -> c) (a a -> b) -> (a a -> c)
+(on) f g = \x y -> f (g x y)
+
 (*>) infixl 4 :: (f a) (f b) -> f b | Applicative f
 (*>) fa fb = const id <$> fa <*> fb
 
diff --git a/paper/While/Makefile b/paper/While/Makefile
new file mode 100644
index 0000000..8125af0
--- /dev/null
+++ b/paper/While/Makefile
@@ -0,0 +1,11 @@
+CLM=clm
+CLMFLAGS=-I $$CLEAN_HOME/lib/Generics
+OBJ=SimpleTest
+
+all: $(OBJ)
+
+$(OBJ): %: $(wildcard *.icl) $(wildcard *.dcl)
+	$(CLM) $(CLMFLAGS) $@ -o $@
+
+clean:
+	rm -rfv Clean\ System\ Files $(OBJ)
diff --git a/paper/While/Simple.dcl b/paper/While/Simple.dcl
index 5a08e85..df49964 100644
--- a/paper/While/Simple.dcl
+++ b/paper/While/Simple.dcl
@@ -3,11 +3,11 @@ definition module Simple
 from StdOverloaded import class toString
 import WhileCommon
 
-:: Stm = Ass Var AExpr
-       | If BExpr Stm Stm
-       | While BExpr Stm
-       | Skip
-       | Compose Stm Stm
+:: Stm   = Ass Var AExpr
+         | If BExpr Stm Stm
+         | While BExpr Stm
+         | Skip
+         | Compose Stm Stm
 
 instance toString Stm
 instance run Stm
diff --git a/paper/While/Simple.icl b/paper/While/Simple.icl
index 4c226c9..7ef042f 100644
--- a/paper/While/Simple.icl
+++ b/paper/While/Simple.icl
@@ -15,15 +15,16 @@ where
 
 instance run Stm
 where
-	run (Ass v e) st
-		= pure (\w -> if (w==v) (eval e st) (st w))
-	run (If b s1 s2) st
+	run :: Stm State -> Either Error State
+	run (Ass v e) st       // Assign e to v
+		= pure (\w -> if (w == v) (eval e st) (st w))
+	run (If b s1 s2) st    // If b then s1 else s2
 		= eval b st >>= \r -> run (if r s1 s2) st
-	run w=:(While b s) st
+	run w=:(While b s) st // While b do s
 		= eval b st >>= \r -> if r
 			(run s st >>= run w)
 			(pure st)
-	run Skip st
+	run Skip st            // Skip
 		= pure st
-	run (Compose s1 s2) st
+	run (Compose s1 s2) st // s1 ; s2
 		= run s1 st >>= run s2
diff --git a/paper/While/WhileCommon.dcl b/paper/While/WhileCommon.dcl
index b813641..6d1c148 100644
--- a/paper/While/WhileCommon.dcl
+++ b/paper/While/WhileCommon.dcl
@@ -7,14 +7,15 @@ from WhileLexer import ::Token
 from Yard import ::Parser
 
 :: Var :== String
-
 :: State :== Var -> Either Error Int
 
+:: Operator = Add | Sub | Mul | Div
+
 :: AExpr = Var Var
          | Lit Int
          | Op AExpr Operator AExpr
 
-:: Operator = Add | Sub | Mul | Div
+:: Comparator = Eq | Ne | Le | Lt | Ge | Gt
 
 :: BExpr = Bool Bool
          | Not BExpr
@@ -22,8 +23,6 @@ from Yard import ::Parser
          | Or BExpr BExpr
          | Comp AExpr Comparator AExpr
 
-:: Comparator = Eq | Ne | Le | Lt | Ge | Gt
-
 derive gEq AExpr, Operator, BExpr, Comparator
 
 instance zero State
diff --git a/paper/While/WhileCommon.icl b/paper/While/WhileCommon.icl
index a76458f..ce4f8fe 100644
--- a/paper/While/WhileCommon.icl
+++ b/paper/While/WhileCommon.icl
@@ -9,7 +9,8 @@ import Yard
 
 derive gEq AExpr, Operator, BExpr, Comparator
 
-instance zero State where zero = \v -> Left (Runtime "Undefined variable")
+instance zero State
+where zero = \v -> Left (Runtime "Undefined")
 
 instance toString AExpr
 where
@@ -38,32 +39,36 @@ where
 
 instance eval AExpr Int
 where
+	eval :: AExpr State -> Either Error Int
 	eval (Var v) st = st v
-	eval (Lit i) st = pure i
-	eval (Op a1 op a2) st = eval a1 st >>= \r1 -> eval a2 st >>= toOp op r1
+	eval (Lit i) _  = pure i
+	eval (Op a1 op a2) st
+		= eval a1 st >>= \r1 ->
+		  eval a2 st >>= app op r1
 	where
-		toOp :: Operator -> Int Int -> Either Error Int
-		toOp Add = \i j -> pure (i + j)
-		toOp Sub = \i j -> pure (i - j)
-		toOp Mul = \i j -> pure (i * j)
-		toOp Div = \i j ->
-			if (j == 0) (Left (Runtime "Division by 0")) (pure (i / j))
+		app :: Operator -> Int Int -> Either Error Int
+		app Add = pure on (+)
+		app Sub = pure on (-)
+		app Mul = pure on (*)
+		app Div = \i j -> if (j == 0)
+			(Left (Runtime "Division by 0"))
+			(pure (i / j))
 
 instance eval BExpr Bool
 where
 	eval (Bool b) st = pure b
-	eval (Not b) st = eval b st >>= pure o not
+	eval (Not b) st = not <$> eval b st
 	eval (And b1 b2) st = liftM2 (&&) (eval b1 st) (eval b2 st)
 	eval (Or b1 b2) st = liftM2 (||) (eval b1 st) (eval b2 st)
 	eval (Comp a1 cmp a2) st = liftM2 (toCmp cmp) (eval a1 st) (eval a2 st)
 	where
 		toCmp :: Comparator -> Int Int -> Bool
-		toCmp Eq = \i j -> i == j
-		toCmp Ne = \i j -> i <> j
-		toCmp Le = \i j -> i <= j
-		toCmp Lt = \i j -> i < j
-		toCmp Ge = \i j -> i >= j
-		toCmp Gt = \i j -> i > j
+		toCmp Eq = (==)
+		toCmp Ne = (<>)
+		toCmp Le = (<=)
+		toCmp Lt = (<)
+		toCmp Ge = (>=)
+		toCmp Gt = (>)
 
 pbexpr :: Parser Token BExpr
 pbexpr = liftM2 Or pbconj (item OrToken *> pbexpr) <|> pbconj
diff --git a/paper/ast.tex b/paper/ast.tex
new file mode 100644
index 0000000..07553bd
--- /dev/null
+++ b/paper/ast.tex
@@ -0,0 +1,31 @@
+\section{The Abstract Syntax Tree}
+\label{sec:ast}
+
+In functional programming languages it is trivial to create new types. A
+formally defined syntax as we have seen for While in \autoref{sec:intro:while}
+translates almost directly to a type definition:
+
+\lstinputlisting[firstline=12,lastline=24]{While/WhileCommon.dcl}
+\lstinputlisting[firstline=6,lastline=10]{While/Simple.dcl}
+
+Note that we have added common binary operators like \CI{Lt} that did not exist
+in the grammar of \autoref{sec:intro:while}. These operators could also be
+constructed from other boolean expressions. We have also added \CI{Div} for
+integer division. It is a useful addition in this example, as it will force us
+to implement error handling in the evaluation of arithmetic expressions when we
+divide by zero.
+
+As an example, the example program from \autoref{sec:intro:while} would be
+stored in the AST as follows:
+
+\begin{lstlisting}
+Compose
+	(Ass "x" (Var "y"))
+	(While
+		(Not (Comp (Var "x") Le (Lit 0)))
+		(Compose
+			(Ass "x" (Op (Var "x") Sub (Lit 2)))
+			(Ass "y" (Op (Var "y") Sub (Lit 1)))
+		)
+	)
+\end{lstlisting}
diff --git a/paper/clean.sty b/paper/clean.sty
new file mode 100644
index 0000000..15c50fc
--- /dev/null
+++ b/paper/clean.sty
@@ -0,0 +1,73 @@
+\usepackage{listings}
+
+\lstdefinelanguage{Clean}{%
+	alsoletter={ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz_`1234567890},
+	alsoletter={~!@\#$\%^\&*-+=?<>:|\\.},
+	morekeywords={generic,implementation,definition,dynamic,module,import,from,where,in,of,case,let,infix,infixr,infixl,class,instance,with,if,derive},
+	sensitive=true,
+	morecomment=[l]{//},
+	morecomment=[n]{/*}{*/},
+	morestring=[b]",
+	morestring=[b]',
+	emptylines=1,
+	basicstyle=\small,
+	identifierstyle=\small\ttfamily,
+	commentstyle=\itshape,
+	keywordstyle=\bfseries,
+	stringstyle=\ttfamily,
+	numbers=none,
+	showstringspaces=false,
+	basewidth=0.45em,
+	columns=[c]fixed,
+	keepspaces=true,
+	breaklines=false,
+	tabsize=4,
+	texcl=true,
+	escapeinside={(\#}{\#)},
+	literate=%
+		% Basic Clean constructs
+		{\\}{{$\lambda\:$}}1
+		{A.}{{$\forall\;\,$}}1
+		{E.}{{$\exists\;\,$}}1
+		{>}{{$>$}}1
+		{<}{{$<$}}1
+		{`}{{\texttt{'}}}1
+		{<=}{{$\leq$}}1
+		{>=}{{$\geq$}}1
+		{<>}{{$\neq$}}1
+		{->}{{$\rightarrow$}}2
+		{<-}{{$\leftarrow$}}1
+		{=}{{$=$}}1
+		{~}{{$\sim$}}1
+		{*}{{$\star$}}1
+		{\#}{{$\sharp$}}1
+		{\{|}{{$\{\!|\!$}}1
+		{|\}}{{$\!|\!\}$}}1
+		{:=}{{$:=$}}2
+		{=:}{{$\>=:$}}3
+		{==}{{$==$}}2
+		{++}{{$+\!\!+$}}2
+		{+++}{{$+\!\!\!\!+\!\!\!\!+$}}2
+		{:==}{{$:==$}}3
+		{\{|*|\}}{{$\{\!|\!\!\star\!\!|\!\}$}}3
+		%
+		% Basic iTask constructs
+		{>||>}{{$\triangleright\triangleright$}}2
+		{>>=}{{\texttt{>>=}}}3
+		{>>|}{{\texttt{>>|}}}3
+		{?>>}{{\texttt{?>>}}}3
+		{!>>}{{\texttt{!>>}}}3
+		{-||-}{{\texttt{-||-}}}4
+		{.||.}{{\texttt{.||.}}}4
+		{.&&.}{{\texttt{.\&\&.}}}4
+}
+
+\newcommand{\CleanInline}[1]{\lstinline[language=Clean]¦#1¦}
+\newcommand{\CI}[1]{\CleanInline{#1}}
+
+\lstdefinestyle{numbers}{numbers=left, stepnumber=1, numberstyle=\tiny, numbersep=5pt}
+
+\lstnewenvironment{CleanCode}{\lstset{language=Clean,identifierstyle=\ttfamily}}{}
+\lstnewenvironment{CleanCodeN}{\lstset{language=Clean,style=numbers}}{}
+\lstnewenvironment{CleanCodeB}{\lstset{language=Clean,frame=single}}{}
+\lstnewenvironment{CleanCodeNB}{\lstset{language=Clean,style=numbers,frame=single}}{}
diff --git a/paper/eval.tex b/paper/eval.tex
new file mode 100644
index 0000000..14246f8
--- /dev/null
+++ b/paper/eval.tex
@@ -0,0 +1,66 @@
+\section{Evaluation}
+\label{sec:eval}
+
+The \CI{Either} type that we use both in the \CI{State} and in the result of
+\CI{eval} implements the \CI{Monad} class. Monads provide an convenient way to
+simulate effects found in other language, as has been argued by \cite{monads}.
+In this case, we want to simulate exception handling: the evaluation of an
+arithmetic may fail, for example in the case of an undefined variable or when
+we try to divide by zero. These errors may occur in different places: the first
+occurs in the \CI{State} function, while the latter will occur in the \CI{eval}
+implementation of \CI{AExpr}. Using monads, we can easily pass through errors.
+An example will clarify:
+
+\lstinputlisting[firstline=40,lastline=55]{While/WhileCommon.icl}
+
+Recall that the second argument to \CI{eval}, here \CI{st}, is of type
+\CI{State}. That is, it is a function that yields an \CI{Either Error Int}. In
+the first alternative of \CI{eval}, for variables, we implicitly use this: if
+looking up the variable in the state fails, a \CI{Left Error} will be returned.
+
+The last case is more interesting, however. Here, we use bind (\CI{>>=}) to
+simulate exception handling: the two evaluations of \CI{a1} and \CI{a2} may
+fail, as may the application of the operator to its two arguments. Even though
+we don't know at this point \emph{why} or \emph{where} the evaluation failed,
+\CI{>>=} will conveniently pass through any errors.
+
+The abstraction of monad binding allows us to work with data or errors, without
+knowing if we still have data to work with. This gives a very basic and
+readable evaluator.
+
+\medskip
+The \CI{eval} instance for \CI{BExpr} is not very different from the one for
+\CI{AExpr} and is omitted here for brevity.
+
+\subsection{Using a lookup table as state}
+\label{sec:eval:lookup}
+We have defined our \CI{State} as a function. Another solution, that may seem
+more straightforward for people coming from the imperative paradigm, would be
+to model it as a lookup table:
+
+\begin{lstlisting}
+:: State :== [(Var, Int)]
+\end{lstlisting}
+
+While possible, this has several drawbacks. First of all, we would need a
+separate function to look up a variable in this store. We could implement that
+function as follows:
+
+\begin{lstlisting}
+lookup :: Var State -> Either Error Int
+lookup _ []   = Left (Runtime "Undefined")
+lookup v [(w:i):st]
+	| v == w    = pure i
+	| otherwise = lookup v st
+\end{lstlisting}
+
+We did not get a rid of a function: a lookup table forces us to write an extra
+function to look up values. Higher order functions provide a more natural way
+to reason about something which, in the end, really is a function. Functional
+programming allows us to work intuitively with higher order functions, which
+lets us stay closer to the specification.
+
+This brings us at the second drawback. Implementing the state as a lookup table
+distances us from the specification, making it more difficult to verify that
+the implementation is correct. In a functional style it is trivial to check
+that an implementation matches the specification.
diff --git a/paper/ftypes.tex b/paper/ftypes.tex
new file mode 100644
index 0000000..fda4152
--- /dev/null
+++ b/paper/ftypes.tex
@@ -0,0 +1,8 @@
+\section{Used functions and types}
+\label{sec:ftypes}
+
+The following functions are considered known. If not, looking them up is easy
+using Cloogle~\citep{cloogle}.
+
+\lstinputlisting[firstline=5,lastline=23]{While/Common.dcl}
+\lstinputlisting[firstline=34]{While/Common.dcl}
diff --git a/paper/interp.tex b/paper/interp.tex
new file mode 100644
index 0000000..0f73b2d
--- /dev/null
+++ b/paper/interp.tex
@@ -0,0 +1,127 @@
+\section{Interpreting}
+\label{sec:interp}
+
+The semantics of While have been specified mathematically~\citep{semantics}.
+While difficult in other paradigms, translating these semantic rules to a
+functional program is trivial. Consider, as an example, the composition rule:
+
+$$
+\begin{prooftree}
+	\trans{S_1}{s}{s'}\quad
+	\trans{S_2}{s'}{s''}
+	\justifies
+	\trans{\whcomp{S_1}{S_2}}{s}{s''}
+	\using{\rcompns}
+\end{prooftree}
+$$
+
+This specifies nothing else than the intuition: the composition
+$\whcomp{S_1}{S_2}$ executed in state $s$ will yield a state $s''$ which we get
+by executing $S_1$ and $S_2$ in $s$, consecutively.
+
+The translation of this rule in a functional program looks as follows:
+
+\begin{lstlisting}
+run (Compose s1 s2) st
+	= run s1 st >>= \st` -> run s2 st`
+\end{lstlisting}
+
+Or, shorter, we can use currying:
+
+\begin{lstlisting}
+run (Compose s1 s2) st
+	= run s1 st >>= run s2
+\end{lstlisting}
+
+Again, using the monadic bind, any errors in running \CI{s1} will propagate,
+and \CI{s2} will not be interpreted. More importantly in this case, the monad
+lets us specify execution order in a convenient and readable way.
+
+\medskip
+Another case where we can clearly see the advantages of functional programming
+is in the assignment rule. Updating a state $st$ works as
+follows~\citep{semantics}:
+
+$$
+	(st[v\mapsto e])w =
+	\begin{cases}
+		e    & \text{if $v=w$} \\
+		st~v & \text{if $v\neq w$.}
+	\end{cases}
+$$
+
+This gives the assignment rule:
+
+$$
+\begin{prooftree}
+	\axjustifies
+	\trans{\whass{x}{a}}{s}{s\left[x\mapsto\mathcal A\llbracket a\rrbracket s\right]}
+	\using{\rassns}
+\end{prooftree}
+$$
+
+It is easy to see that assignment will never fail. The only thing we need to do
+is update the state. This is done easily with a lambda expression:
+
+\begin{lstlisting}
+run (Ass v e) st
+	= pure (\w -> if (w == v) (eval e st) (st w))
+\end{lstlisting}
+
+The lambda expression is the direct translation of the update function used by
+\cite{semantics} as described above. This is much more intuitive than using,
+for example, a lookup table to model the state. Again, functional programming
+lets us stay close to the mathematical definitions.
+
+The only possible reason we would \emph{not} want to model the state as a
+function is efficiency. This approach has linear fetch complexity, as has the
+lookup table from \autoref{sec:eval:lookup}. However, storing the function on
+the heap will in virtually any implementation be less efficient than storing a
+list of simple tuples. Furthermore, the lookup table approach can be modified
+using a different data structure to give a better complexity: logarithmic, if a
+binary search tree is used, or even constant if the variables can be mapped to
+array indices.
+
+\medskip
+The full instance of \CI{run} for \CI{Stm} is given below. It exploits monads
+for error reporting and execution order. Four of the five alternatives are
+derived trivially from their corresponding semantic rules. Only the \CI{If}
+alternative had to be adapted; it will be discussed in the next paragraph.
+
+\lstinputlisting[firstline=16]{While/Simple.icl}
+
+\subsection{Conditions}
+\label{sec:interp:cond}
+\cite{semantics} define two rules for the \CI{If} statement. The first
+specifies that if $b$ holds in state $s$, the statement $\whif{b}{S_1}{S_2}$ in
+$s$ will be equivalent to $S_1$:
+
+$$
+\begin{prooftree}
+	\trans{S_1}{s}{s'}
+	\justifies
+	\trans{\whif{b}{S_1}{S_2}}{s}{s'}
+	\using{\rifttns}
+	\quad\text{if $\mathcal B\llbracket b\rrbracket s$}
+\end{prooftree}
+$$
+
+A similar rule exists for $S_2$ in the case that $\mathcal B\llbracket
+b\rrbracket s$ does not hold.
+
+The problem with these rules is that they can only be applied when some
+condition is met. In this case, the condition is still relatively easy. In
+other cases, it may also depend on the transitions above the line: for example,
+we may want to check that $b$ holds in $s'$ rather than in $s$. If we would
+want to support that kind of functionality, we would need to try to satisfy the
+antecedent, then verify if the condition holds and only apply the rule if it
+does. In the end this is possible (although we will not show it here) --- the
+\CI{Alternative} class provides a nice infrastructure for this.
+
+In the case of the \CI{If} statement this problem can be avoided as shown
+above. This is however only possible thanks to the fact that the two rules for
+this construct are very similar, and because the condition depends only on
+the initial state and statement.
+
+It is outside the scope of this paper to discuss the possibilities for
+implementing rules with complex conditionals.
diff --git a/paper/intro-org.tex b/paper/intro-org.tex
index 55231b7..ee2a38d 100644
--- a/paper/intro-org.tex
+++ b/paper/intro-org.tex
@@ -2,10 +2,16 @@
 \label{sec:intro:org}
 In this paper we present different advantages of working with imperative code
 in a functional style. We do this by means of a case study, an interpreter of
-the language While~\citep{proganal}. After describing While briefly in
-\autoref{sec:intro:while}, we will iteratively build our interpreter: the lexer
-in \autoref{sec:lexer}, the parser in \autoref{sec:parser} and the actual
-interpreter in \autoref{sec:interpreter}. As an intermezzo, in
-\autoref{sec:evaluation} we discuss different possibilities of evaluating
-mathematical expressions. Finally, in \autoref{sec:conclusions} we precisely
-articulate the advantages of functional interpretation.
+the language While~\citep{proganal}. We will describe this example language
+briefly in \autoref{sec:intro:while}. Before discussing our interpreter, we
+will discuss basic definition that will be helpful in \autoref{sec:predefs}.
+Since extensive research has already been done into lexing and parsing
+\citep[see e.g.][]{yard}, will skip these steps and assume we already have an
+abstract syntax tree (AST). This AST is described in \autoref{sec:ast}. In
+\autoref{sec:eval} we will discuss different possibilities of evaluating
+mathematical expressions. Finally, in \autoref{sec:interp} we will propose a
+While interpreter. We finish by articulating the advantages of functional
+interpretation in \autoref{sec:conclusions}.
+
+\autoref{sec:ftypes} lists the functions and types that the reader is supposed
+to know.
diff --git a/paper/intro-while.tex b/paper/intro-while.tex
index 30d8efd..128244a 100644
--- a/paper/intro-while.tex
+++ b/paper/intro-while.tex
@@ -23,26 +23,25 @@ The syntax we will use is:
 
 	<BExpr> ::= `true'
 		| `false'
-		| $a_1 = a_2$
+		\alt $a_1 = a_2$
 		| $a_1 \le a_2$
 		| $\lnot b$
 		| $b_1 \land b_2$
 
 	<Stm> ::=
 		  $x$ `:=' $a$
-		| $S_1$ `;' $S_2$
 		| `skip'
-		| `if' $b$ `then' $S_1$ `else' $S_2$ `endif'
-		| `while' $b$ `do' $S$ `done'
+		| `while' $b$ `do' $S$
+		\alt `if' $b$ `then' $S_1$ `else' $S_2$
+		| $S_1$ `;' $S_2$
 \end{grammar}
 
-The syntax of statements has been adapted slightly to make it deterministic.
-The grammar for \<Aexpr> and \<BExpr> has not been made deterministic for
-brevity's sake; standard operator precedence applies.
-
-We assume that composition (\whcomp{$S_1$}{$S_2$}) is right associative. We
-ignore all whitespace, and do not allow variable names that are reserved
-keywords such as \whskip.
+Since we do not discuss parsing in this paper, we need not modify the syntax to
+make it deterministic. Standard operator precedence applies for \<AExpr> and
+\<BExpr>; for \`while' and \`if' we let it be clear from the context where the
+block ends. Lastly, we assume that composition (\whcomp{$S_1$}{$S_2$}) is right
+associative. We ignore all whitespace, and do not allow variable names that are
+reserved keywords such as \whskip.
 
 The semantics of these syntax constructs should be intuitive. As an example,
 after executing the following program, \verb$y$ will have been divided by $2$:
@@ -52,8 +51,10 @@ after executing the following program, \verb$y$ will have been divided by $2$:
 		{\whass{x}{y}}
 		{\whwhile{\whnotp{\whle{x}{0}}}%
 			{\whcomp%
-				{x := x - 2}%
-				{y := y - 1}%
+				{\whass{x}{x-2}}
+				{\whass{y}{y-1}}
 			}
 		}
 \end{while}
+
+While programs are executed in a \emph{state} which maps variables to integers.
diff --git a/paper/paper.bib b/paper/paper.bib
index 93588fe..f43c91e 100644
--- a/paper/paper.bib
+++ b/paper/paper.bib
@@ -6,6 +6,20 @@
 	year = {1999}
 }
 
+@book{semantics,
+	title = {Semantics with Applications: A Formal Introduction},
+	author = {Nielson, H. R. and Nielson, F.},
+	edition = {1999 Revised},
+	publisher = {John Wiley \& Sons},
+	year = {1992}
+}
+
+@article{monads,
+	author = {Wadler, P.},
+	title = {Monads for functional programming},
+	year = {1995}
+}
+
 @article{algol,
  author = {Backus, J. W. and Bauer, F. L. and Green, J. and Katz, C. and McCarthy, J. and Perlis, A. J. and Rutishauser, H. and Samelson, K. and Vauquois, B. and Wegstein, J. H. and van Wijngaarden, A. and Woodger, M.},
  editor = {Naur, Peter},
@@ -26,3 +40,16 @@
  address = {New York, NY, USA},
 } 
 
+@article{yard,
+	author = {Jager, P.T.},
+	title = {Analysing embedded domain specific languages in Haskell from Core},
+	year = {2014}
+}
+
+@misc{cloogle,
+	author = {Lubbers, M. and Staps, C.},
+	title = {Cloogle},
+	year = {2016},
+	howpublished = "\mbox{\url{http://cloogle.org/}}",
+	note = "Accessed June 2, 2016"
+}
diff --git a/paper/paper.tex b/paper/paper.tex
index d036bda..7d63d8c 100644
--- a/paper/paper.tex
+++ b/paper/paper.tex
@@ -1,11 +1,14 @@
 \documentclass[a4paper]{article}
 
 \usepackage[english]{babel}
-\usepackage{geometry}
+\usepackage[margin=2cm,bottom=3.5cm]{geometry}
 \usepackage[hidelinks]{hyperref}
 \usepackage{natbib}
 
+\usepackage{amsmath}
 \usepackage{enumitem}
+\usepackage{multicol}
+\usepackage{stmaryrd}
 
 \usepackage{syntax}
 \renewcommand\litleft{\bgroup\tt}
@@ -13,6 +16,20 @@
 \def\<#1>{\synt{#1}}
 \def\`#1'{\lit{#1}}
 
+\usepackage{clean}
+\usepackage[dvipsnames]{xcolor}
+\lstdefinestyle{coloured}{
+	keywordstyle=\bfseries\color{NavyBlue},
+	stringstyle=\ttfamily\color{BrickRed}
+}
+\lstset{
+	language=Clean,
+	breaklines,
+	tabsize=2,
+	xleftmargin=\parindent,
+	style=coloured
+}
+
 \usepackage{while}
 
 \title{Imperative code interpretation in a functional style}
@@ -20,13 +37,26 @@
 
 \begin{document}
 
-\maketitle
+\abovedisplayshortskip=-4pt
+\abovedisplayskip=\abovedisplayshortskip
+\belowdisplayshortskip=7pt
+\belowdisplayskip=\belowdisplayshortskip
 
+\maketitle
 \input{abs}
-\input{intro}
 
-\bibliographystyle{jfp}
-\bibliography{paper}
+\begin{multicols}{2}
+	\input{intro}
+	\input{predefs}
+	\input{ast}
+	\input{eval}
+	\input{interp}
+
+	\appendix
+	\input{ftypes}
 
-\end{document}
+	\bibliographystyle{jfp}
+	\bibliography{paper}
+\end{multicols}
 
+\end{document} 
diff --git a/paper/predefs.tex b/paper/predefs.tex
new file mode 100644
index 0000000..d6c7ff8
--- /dev/null
+++ b/paper/predefs.tex
@@ -0,0 +1,48 @@
+\section{Preliminary definitions}
+\label{sec:predefs}
+
+A number of types will turn out to be useful in general. We define:
+
+\lstinputlisting[firstline=25,lastline=28]{While/Common.dcl}
+
+The \CI{Error} type distinguishes between different kinds of errors, that can
+be further identified with a descriptive string. We could add more information
+to these types, like the position (file, line and column) of the input token
+that causes the error. The implementation thereof is straightforward and will
+for the sake of brevity be omitted here.
+
+We can model the partial state function as a function that yields an \CI{Either
+Error Int}. Whenever a variable is not defined, a \CI{Left (Runtime
+"Undefined")} will be returned.  Otherwise, a \CI{Right n} is returned. The
+initial state, which maps any variable to a \CI{Left} result, is implemented as
+an instance of the \CI{zero} class.
+
+\lstinputlisting[firstline=9,lastline=10]{While/WhileCommon.dcl}
+\lstinputlisting[firstline=12,lastline=13]{While/WhileCommon.icl}
+
+In order to build up our interpreter modularly, we wouldn't want to fix the
+type of the AST just yet. Rather, we want it to be possible to implement
+different kinds of abstract syntax trees: for example, it may be interesting to
+implement a While program as a list of statements (making composition
+implicit), while the straightforward AST would use a compositional constructor.
+To allow for different ASTs, we make the \CI{run} function, that will interpret
+a While program in some state, overloaded:
+
+\lstinputlisting[firstline=35,lastline=35]{While/WhileCommon.dcl}
+
+Similarly, we want to be able to use the same terminology of \emph{evaluation}
+for both arithmetic and boolean expressions. This can be done using overloading
+as well:
+
+\lstinputlisting[firstline=37,lastline=39]{While/WhileCommon.dcl}
+
+The \CI{eval} function may yield an error, for example when an undefined
+variable is used. It makes sense to separate evaluation and interpretation,
+because evaluation does not depend on the type for statements. Any AST using
+\CI{AExpr} may now use this \CI{eval} function (while it is also possible to
+create an AST that uses a different representation of arithmetic expressions).
+
+Although all these functions are presented in an overloaded fashion, we will
+only consider one implementation, the AST from \autoref{sec:ast} below. Other
+models do not introduce additional problems that would be interesting for the
+purposes of this paper.
diff --git a/paper/prooftree.sty b/paper/prooftree.sty
new file mode 100644
index 0000000..b611d67
--- /dev/null
+++ b/paper/prooftree.sty
@@ -0,0 +1,374 @@
+\message{<Paul Taylor's Proof Trees, 2 August 1996>}
+%% Build proof tree for Natural Deduction, Sequent Calculus, etc.
+%% WITH SHORTENING OF PROOF RULES!
+%% Paul Taylor, begun 10 Oct 1989
+%% *** THIS IS ONLY A PRELIMINARY VERSION AND THINGS MAY CHANGE! ***
+%%
+%% 2 Aug 1996: fixed \mscount and \proofdotnumber
+%%
+%%      \prooftree
+%%              hyp1            produces:
+%%              hyp2
+%%              hyp3            hyp1    hyp2    hyp3
+%%      \justifies              -------------------- rulename
+%%              concl                   concl
+%%      \thickness=0.08em
+%%      \shiftright 2em
+%%      \using
+%%              rulename
+%%      \endprooftree
+%%
+%% where the hypotheses may be similar structures or just formulae.
+%%
+%% To get a vertical string of dots instead of the proof rule, do
+%%
+%%      \prooftree                      which produces:
+%%              [hyp]
+%%      \using                                  [hyp]
+%%              name                              .
+%%      \proofdotseparation=1.2ex                 .name
+%%      \proofdotnumber=4                         .
+%%      \leadsto                                  .
+%%              concl                           concl
+%%      \endprooftree
+%%
+%% Within a prooftree, \[ and \] may be used instead of \prooftree and
+%% \endprooftree; this is not permitted at the outer level because it
+%% conflicts with LaTeX. Also,
+%%      \Justifies
+%% produces a double line. In LaTeX you can use \begin{prooftree} and
+%% \end{prootree} at the outer level (however this will not work for the inner
+%% levels, but in any case why would you want to be so verbose?).
+%%
+%% All of of the keywords except \prooftree and \endprooftree are optional
+%% and may appear in any order. They may also be combined in \newcommand's
+%% eg "\def\Cut{\using\sf cut\thickness.08em\justifies}" with the abbreviation
+%% "\prooftree hyp1 hyp2 \Cut \concl \endprooftree". This is recommended and
+%% some standard abbreviations will be found at the end of this file.
+%%
+%% \thickness specifies the breadth of the rule in any units, although
+%% font-relative units such as "ex" or "em" are preferable.
+%% It may optionally be followed by "=".
+%% \proofrulebreadth=.08em or \setlength\proofrulebreadth{.08em} may also be
+%% used either in place of \thickness or globally; the default is 0.04em.
+%% \proofdotseparation and \proofdotnumber control the size of the
+%% string of dots
+%%
+%% If proof trees and formulae are mixed, some explicit spacing is needed,
+%% but don't put anything to the left of the left-most (or the right of
+%% the right-most) hypothesis, or put it in braces, because this will cause
+%% the indentation to be lost.
+%%
+%% By default the conclusion is centered wrt the left-most and right-most
+%% immediate hypotheses (not their proofs); \shiftright or \shiftleft moves
+%% it relative to this position. (Not sure about this specification or how
+%% it should affect spreading of proof tree.)
+%
+% global assignments to dimensions seem to have the effect of stretching
+% diagrams horizontally.
+%
+%%==========================================================================
+
+\def\introrule{{\cal I}}\def\elimrule{{\cal E}}%%
+\def\andintro{\using{\land}\introrule\justifies}%%
+\def\impelim{\using{\Rightarrow}\elimrule\justifies}%%
+\def\allintro{\using{\forall}\introrule\justifies}%%
+\def\allelim{\using{\forall}\elimrule\justifies}%%
+\def\falseelim{\using{\bot}\elimrule\justifies}%%
+\def\existsintro{\using{\exists}\introrule\justifies}%%
+
+%% #1 is meant to be 1 or 2 for the first or second formula
+\def\andelim#1{\using{\land}#1\elimrule\justifies}%%
+\def\orintro#1{\using{\lor}#1\introrule\justifies}%%
+
+%% #1 is meant to be a label corresponding to the discharged hypothesis/es
+\def\impintro#1{\using{\Rightarrow}\introrule_{#1}\justifies}%%
+\def\orelim#1{\using{\lor}\elimrule_{#1}\justifies}%%
+\def\existselim#1{\using{\exists}\elimrule_{#1}\justifies}
+
+%%==========================================================================
+
+\newdimen\proofrulebreadth \proofrulebreadth=.05em
+\newdimen\proofdotseparation \proofdotseparation=1.25ex
+\newdimen\proofrulebaseline \proofrulebaseline=2ex
+\newcount\proofdotnumber \proofdotnumber=3
+\let\then\relax
+\def\hfi{\hskip0pt plus.0001fil}
+\mathchardef\squigto="3A3B
+%
+% flag where we are
+\newif\ifinsideprooftree\insideprooftreefalse
+\newif\ifonleftofproofrule\onleftofproofrulefalse
+\newif\ifproofdots\proofdotsfalse
+\newif\ifdoubleproof\doubleprooffalse
+\let\wereinproofbit\relax
+%
+% dimensions and boxes of bits
+\newdimen\shortenproofleft
+\newdimen\shortenproofright
+\newdimen\proofbelowshift
+\newbox\proofabove
+\newbox\proofbelow
+\newbox\proofrulename
+%
+% miscellaneous commands for setting values
+\def\shiftproofbelow{\let\next\relax\afterassignment\setshiftproofbelow\dimen0 }
+\def\shiftproofbelowneg{\def\next{\multiply\dimen0 by-1 }%
+\afterassignment\setshiftproofbelow\dimen0 }
+\def\setshiftproofbelow{\next\proofbelowshift=\dimen0 }
+\def\setproofrulebreadth{\proofrulebreadth}
+
+%=============================================================================
+\def\prooftree{% NESTED ZERO (\ifonleftofproofrule)
+%
+% first find out whether we're at the left-hand end of a proof rule
+\ifnum  \lastpenalty=1
+\then   \unpenalty
+\else   \onleftofproofrulefalse
+\fi
+%
+% some space on left (except if we're on left, and no infinity for outermost)
+\ifonleftofproofrule
+\else   \ifinsideprooftree
+        \then   \hskip.5em plus1fil
+        \fi
+\fi
+%
+% begin our proof tree environment
+\bgroup% NESTED ONE (\proofbelow, \proofrulename, \proofabove,
+%               \shortenproofleft, \shortenproofright, \proofrulebreadth)
+\setbox\proofbelow=\hbox{}\setbox\proofrulename=\hbox{}%
+\let\justifies\proofover\let\leadsto\proofoverdots\let\Justifies\proofoverdbl
+\let\using\proofusing\let\[\prooftree
+\ifinsideprooftree\let\]\endprooftree\fi
+\proofdotsfalse\doubleprooffalse
+\let\thickness\setproofrulebreadth
+\let\shiftright\shiftproofbelow \let\shift\shiftproofbelow
+\let\shiftleft\shiftproofbelowneg
+\let\ifwasinsideprooftree\ifinsideprooftree
+\insideprooftreetrue
+%
+% now begin to set the top of the rule (definitions local to it)
+\setbox\proofabove=\hbox\bgroup$\displaystyle % NESTED TWO
+\let\wereinproofbit\prooftree
+%
+% these local variables will be copied out:
+\shortenproofleft=0pt \shortenproofright=0pt \proofbelowshift=0pt
+%
+% flags to enable inner proof tree to detect if on left:
+\onleftofproofruletrue\penalty1
+}
+
+%=============================================================================
+% end whatever box and copy crucial values out of it
+\def\eproofbit{% NESTED TWO
+%
+% various hacks applicable to hypothesis list 
+\ifx    \wereinproofbit\prooftree
+\then   \ifcase \lastpenalty
+        \then   \shortenproofright=0pt  % 0: some other object, no indentation
+        \or     \unpenalty\hfil         % 1: empty hypotheses, just glue
+        \or     \unpenalty\unskip       % 2: just had a tree, remove glue
+        \else   \shortenproofright=0pt  % eh?
+        \fi
+\fi
+%
+% pass out crucial values from scope
+\global\dimen0=\shortenproofleft
+\global\dimen1=\shortenproofright
+\global\dimen2=\proofrulebreadth
+\global\dimen3=\proofbelowshift
+\global\dimen4=\proofdotseparation
+\global\count255=\proofdotnumber
+%
+% end the box
+$\egroup  % NESTED ONE
+%
+% restore the values
+\shortenproofleft=\dimen0
+\shortenproofright=\dimen1
+\proofrulebreadth=\dimen2
+\proofbelowshift=\dimen3
+\proofdotseparation=\dimen4
+\proofdotnumber=\count255
+}
+
+%=============================================================================
+\def\proofover{% NESTED TWO
+\eproofbit % NESTED ONE
+\setbox\proofbelow=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofover
+$\displaystyle
+}%
+%
+%=============================================================================
+\def\proofoverdbl{% NESTED TWO
+\eproofbit % NESTED ONE
+\doubleprooftrue
+\setbox\proofbelow=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofoverdbl
+$\displaystyle
+}%
+%
+%=============================================================================
+\def\proofoverdots{% NESTED TWO
+\eproofbit % NESTED ONE
+\proofdotstrue
+\setbox\proofbelow=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofoverdots
+$\displaystyle
+}%
+%
+%=============================================================================
+\def\proofusing{% NESTED TWO
+\eproofbit % NESTED ONE
+\setbox\proofrulename=\hbox\bgroup % NESTED TWO
+\let\wereinproofbit\proofusing
+\kern0.3em$
+}
+
+%=============================================================================
+\def\endprooftree{% NESTED TWO
+\eproofbit % NESTED ONE
+% \dimen0 =     length of proof rule
+% \dimen1 =     indentation of conclusion wrt rule
+% \dimen2 =     new \shortenproofleft, ie indentation of conclusion
+% \dimen3 =     new \shortenproofright, ie
+%                space on right of conclusion to end of tree
+% \dimen4 =     space on right of conclusion below rule
+  \dimen5 =0pt% spread of hypotheses
+% \dimen6, \dimen7 = height & depth of rule
+%
+% length of rule needed by proof above
+\dimen0=\wd\proofabove \advance\dimen0-\shortenproofleft
+\advance\dimen0-\shortenproofright
+%
+% amount of spare space below
+\dimen1=.5\dimen0 \advance\dimen1-.5\wd\proofbelow
+\dimen4=\dimen1
+\advance\dimen1\proofbelowshift \advance\dimen4-\proofbelowshift
+%
+% conclusion sticks out to left of immediate hypotheses
+\ifdim  \dimen1<0pt
+\then   \advance\shortenproofleft\dimen1
+        \advance\dimen0-\dimen1
+        \dimen1=0pt
+%       now it sticks out to left of tree!
+        \ifdim  \shortenproofleft<0pt
+        \then   \setbox\proofabove=\hbox{%
+                        \kern-\shortenproofleft\unhbox\proofabove}%
+                \shortenproofleft=0pt
+        \fi
+\fi
+%
+% and to the right
+\ifdim  \dimen4<0pt
+\then   \advance\shortenproofright\dimen4
+        \advance\dimen0-\dimen4
+        \dimen4=0pt
+\fi
+%
+% make sure enough space for label
+\ifdim  \shortenproofright<\wd\proofrulename
+\then   \shortenproofright=\wd\proofrulename
+\fi
+%
+% calculate new indentations
+\dimen2=\shortenproofleft \advance\dimen2 by\dimen1
+\dimen3=\shortenproofright\advance\dimen3 by\dimen4
+%
+% make the rule or dots, with name attached
+\ifproofdots
+\then
+        \dimen6=\shortenproofleft \advance\dimen6 .5\dimen0
+        \setbox1=\vbox to\proofdotseparation{\vss\hbox{$\cdot$}\vss}%
+        \setbox0=\hbox{%
+                \advance\dimen6-.5\wd1
+                \kern\dimen6
+                $\vcenter to\proofdotnumber\proofdotseparation
+                        {\leaders\box1\vfill}$%
+                \unhbox\proofrulename}%
+\else   \dimen6=\fontdimen22\the\textfont2 % height of maths axis
+        \dimen7=\dimen6
+        \advance\dimen6by.5\proofrulebreadth
+        \advance\dimen7by-.5\proofrulebreadth
+        \setbox0=\hbox{%
+                \kern\shortenproofleft
+                \ifdoubleproof
+                \then   \hbox to\dimen0{%
+                        $\mathsurround0pt\mathord=\mkern-6mu%
+                        \cleaders\hbox{$\mkern-2mu=\mkern-2mu$}\hfill
+                        \mkern-6mu\mathord=$}%
+                \else   \vrule height\dimen6 depth-\dimen7 width\dimen0
+                \fi
+                \unhbox\proofrulename}%
+        \ht0=\dimen6 \dp0=-\dimen7
+\fi
+%
+% set up to centre outermost tree only
+\let\doll\relax
+\ifwasinsideprooftree
+\then   \let\VBOX\vbox
+\else   \ifmmode\else$\let\doll=$\fi
+        \let\VBOX\vcenter
+\fi
+% this \vbox or \vcenter is the actual output:
+\VBOX   {\baselineskip\proofrulebaseline \lineskip.2ex
+        \expandafter\lineskiplimit\ifproofdots0ex\else-0.6ex\fi
+        \hbox   spread\dimen5   {\hfi\unhbox\proofabove\hfi}%
+        \hbox{\box0}%
+        \hbox   {\kern\dimen2 \box\proofbelow}}\doll%
+%
+% pass new indentations out of scope
+\global\dimen2=\dimen2
+\global\dimen3=\dimen3
+\egroup % NESTED ZERO
+\ifonleftofproofrule
+\then   \shortenproofleft=\dimen2
+\fi
+\shortenproofright=\dimen3
+%
+% some space on right and flag we've just made a tree
+\onleftofproofrulefalse
+\ifinsideprooftree
+\then   \hskip.5em plus 1fil \penalty2
+\fi
+}
+
+\endinput
+
+%==========================================================================
+% IDEAS
+% 1.    Specification of \shiftright and how to spread trees.
+% 2.    Spacing command \m which causes 1em+1fil spacing, over-riding
+%       exisiting space on sides of trees and not affecting the
+%       detection of being on the left or right.
+% 3.    Hack using \@currenvir to detect LaTeX environment; have to
+%       use \aftergroup to pass \shortenproofleft/right out.
+% 4.    (Pie in the sky) detect how much trees can be "tucked in"
+% 5.    Discharged hypotheses (diagonal lines).
+
+Date: Tue, 19 May 1998 16:45:32 +0100
+From: Simon Gay <simon@dcs.rhbnc.ac.uk>
+
+I've got another problem when combining
+your packages with elsart.cls. The code
+
+\documentclass{elsart}
+\input{prooftree}
+\input{diagrams}
+\begin{document}
+
+\[
+\begin{prooftree}
+A \rTo^{f} B
+\justifies
+p \rTo^{(a,c)} q
+\end{prooftree}
+\]
+
+\end{document}
+
+doesn't leave enough space below the line in the proof tree, so that
+the (a,c) label on the lower arrow runs into the line. It's fine with
+article.cls. 
diff --git a/paper/while.sty b/paper/while.sty
index 33b94b3..ed34c41 100644
--- a/paper/while.sty
+++ b/paper/while.sty
@@ -1,11 +1,21 @@
-\newenvironment{while}{\medskip}{\medskip}
+\usepackage{prooftree}
+
+\newenvironment{while}{\medskip\noindent}{\medskip}
 
 \def\whskip{\texttt{skip}}
 \def\whass#1#2{\texttt{#1 := #2}}
 \def\whcomp#1#2{#1\texttt{;} #2}
-\def\whif#1#2#3{\texttt{if #1 then #2 else #3 endif}}
-\def\whwhile#1#2{\texttt{while #1 do #2 done}}
+\def\whif#1#2#3{\texttt{if~}#1\texttt{~then~}#2\texttt{~else~}#3}
+\def\whwhile#1#2{\texttt{while~}#1\texttt{~do~}#2}
 
 \def\whnot#1{\texttt{$\lnot$#1}}
 \def\whnotp#1{\texttt{$\lnot$(#1)}}
-\def\whle#1#2{\texttt{#1 $\le$ #2}}
+\def\whle#1#2{\texttt{#1$\le$#2}}
+
+\def\axjustifies{\thickness0em\justifies}
+\def\trans#1#2#3{\left\langle#1,#2\right\rangle\rightarrow#3}
+
+\def\smbox#1{\mbox{\footnotesize{#1}}}
+\def\rcompns{[\mbox{comp}_{\smbox{ns}}]}
+\def\rassns{[\mbox{ass}_{\smbox{ns}}]}
+\def\rifttns{[\mbox{if}^{\smbox{tt}}_{\smbox{ns}}]}