\section{Implementation of $\lamtwo$}
The source of Sections 2 and 3 of this paper is a literate Haskell
script implementing normalization for $\lamtwo$ and is available from
\begin{verbatim}
http://www.cs.nott.ac.uk/~txa/publ/Nbe2.lhs
\end{verbatim}
% Hence we start with
% \begin{code}
% module Nbe2 where
% \end{code}
We start by introducing types $\Ty \in \type$, variables $\Var \in
\type$, typing contexts $\Con \in \type$ and untyped terms $\UTm \in
\type$ of the object language by the following Haskell datatype
definitions:
% (We use \texttt{TTrue}, \texttt{TTFalse} instead
% of $\True$, $\False$ as constructor overloading is not possible in
% Haskell.)
\begin{code}
data Ty = Bool | Ty :-> Ty
deriving (Show, Eq)
type Var = String
type Con = [ (Var, Ty) ]
\end{code}
\begin{code}
data Tm = Var Var
| TTrue | TFalse | If Tm Tm Tm
| Lam Ty String Tm | App Tm Tm
deriving (Show, Eq)
\end{code}
We view these recursive definitions as inductive definitions, i.e., we
do not consider infinite terms. All the functions we define are total
wrt. their precise type-theoretic types.
Implementing typed terms $\Tm \in \Con \to \Ty \to \type$ would take
inductive families, which we cannot use in Haskell. But we can
implement type inference $\infer \in \Con \to \UTm \to \Maybe\ \Ty$
(where $\Maybe\ X = 1 + X$ as usual):
\begin{code}
infer :: Con -> Tm -> Maybe Ty
infer gamma (Var x) =
do sigma <- lookup x gamma
Just sigma
infer gamma TTrue = Just Bool
infer gamma TFalse = Just Bool
infer gamma (If t u0 u1) =
do Bool <- infer gamma t
sigma0 <- infer gamma u0
sigma1 <- infer gamma u1
if sigma0 == sigma1 then Just sigma0 else Nothing
infer gamma (Lam sigma x t) =
do tau <- infer ((x, sigma) : gamma) t
Just (sigma :-> tau)
infer gamma (App t u) =
do (sigma :-> tau) <- infer gamma t
sigma' <- infer gamma u
if sigma == sigma' then Just tau else Nothing
\end{code}
This implementation is correct in the sense that $t \in \Tm_\G\ \si$
iff $\infer_\G\ t = \Just\ \si$.
% We write
% $t\in\Tm^\si$ if the above relation holds for the empty context.
% The semantics of types is given by providing an interpretation of
% $\Bool$ and $\Arr$, which gives rise to an interpretation of types
% $\tyeval{-} \in \Ty \to \type$.
Evaluation of types $\tyeval{-} \in \Ty \to \type$ is again an
inductive family, which we cannot implement in Haskell, and the
workaround is to have all $\tyeval{\si}$ coalesced into one
metalanguage type $\el$ (of untyped elements) much the same way as
all $\Tm_\G\ \sigma$ appear coalesced in $\UTm$. We use a type class
$\Sem$ to state what we require of such a coalesced type $\el$:
\begin{code}
class Sem el where
true :: el
false :: el
xif :: el -> el -> el -> el
lam :: Ty -> (el -> el) -> el
app :: el -> el -> el
\end{code}
Evaluation of types $\tyeval{-} \in \Ty \to \type$ naturally induces
evaluation of contexts $\coneval{-} \in \Con \to \type$, defined by
\ax{ [] \in \coneval{[]}}
\quad
\ru{ \rho \in \coneval{\G}\quad d\in\tyeval{\sigma}}
{(x,d):\rho \in \coneval{(x,\sigma):\G}}
We write $\Tm\ \G = \qtyeval{\G}$ for the set of closed substitutions,
which arises as in instance when using $\qtyeval{\sigma} = \Tm_{[]}
\sigma$ as the interpretation of types.
In the Haskell code we approximate evaluation of contexts by $\UEnv$:
\begin{code}
type Env el = [ (Var, el) ]
\end{code}
Given $t\in \Tm_\G\,\sigma$ we define the evaluation of terms
$\tmeval{t}\in \coneval{\G} \to \tyeval{\sigma}$. In Haskell
this is implemented as $\mathsf{eval}$:
\begin{code}
eval :: Sem el => Env el -> Tm -> el
eval rho (Var x) = d
where (Just d) = lookup x rho
eval rho TTrue = true
eval rho TFalse = false
eval rho (If t u0 u1) =
xif (eval rho t) (eval rho u0) (eval rho u1)
eval rho (Lam sigma x t) =
lam sigma (\ d -> eval ((x, d) : rho) t)
eval rho (App t u) = app (eval rho t) (eval rho u)
\end{code}
%This implementation is correct in the sense that if $\rho\in \Env\ \G$
%and $t\in\Tm_\G\ \si$, then $\mathsf{eval}\ \rho\ t = \tmeval{t}\ \rho$.
%%\tmeval{t}\ \rho\in\tyeval{\sigma}$.
% Semantically, contexts are interpreted by environments, we write
% $\rho\in\tyeval{\G}$, if $\rho$ assigns to each variable in $\Gamma$
% an element of the appropriate type.
The standard set-theoretic semantics is given by
\begin{eqnarray*}
\styeval{\Bool} & = & \Bool \\
\styeval{\sigma \Arr \tau} & = & \styeval{\sigma}\to\styeval{\tau}
\end{eqnarray*}
This can be represented in Haskell as
an instance of $\Sem$:
\begin{code}
data El = STrue | SFalse | SLam Ty (El -> El)
instance Sem El where
true = STrue
false = SFalse
xif STrue d _ = d
xif SFalse _ d = d
lam = SLam
app (SLam _ f) d = f d
\end{code}
%We write $\stmeval{-}$ to emphasize evaluation in the set-theoretic
%semantics (this is automatically inferred by Haskell).
Since sets form a cartesian closed category with a boolean object, the
set-theoretic semantics validates all $\beta\eta$-equalities. This is
to say that $\stmeval{-}$ is equationally sound:
\begin{proposition}[Soundness]
\label{prop:soundness}
If $\rho\in\coneval{\G}$ and $t \eqbe t' \in\Tm_\G\ \si$, then
$\stmeval{t}\ \rho = \stmeval{t'}\ \rho$.
\end{proposition}
Since all the sets we consider are finite, semantic equality can be
implemented in Haskell, by making use of the function $\enum \in (\si
\in \Ty) \to \Tree\ \tyeval{\si}$, which we will provide later:
\begin{code}
instance Eq El where
STrue == STrue = True
SFalse == SFalse = True
(SLam sigma f) == (SLam _ f') =
and [f d == f' d | d <- flatten (enum sigma)]
_ == _ = False
\end{code}
Using on the same function we can also print elements of $\El$:
\begin{code}
instance Show El where
show STrue = "STrue"
show SFalse = "SFalse"
show (SLam sigma f) =
"SLam " ++ (show sigma) ++ " " ++
(show [ (d, f d) | d <- flatten (enum sigma) ])
\end{code}
The equational theory of the calculus itself gives rise to another
semantics---the free semantics, or typed terms up to
$\beta\eta$-convertibility. This can be approximated by the
following Haskell code, which uses a redundancy-avoiding version
$\mathtt{if'}$ of $\If$ which produces a shorter but $\beta\eta$-equivalent
term:
\begin{code}
if' :: Tm -> Tm -> Tm -> Tm
if' t TTrue TFalse = t
if' t u0 u1 = if u0 == u1 then u0 else If t u0 u1
instance Sem Tm where
true = TTrue
false = TFalse
xif = if'
lam sigma f = Lam sigma "x" (f (Var "x"))
app = App
\end{code}
We also observe that the use of a fixed variable is only justified by
the fact that our algorithm uses at most one bound variable at the
time. A correct dependently typed version of the free semantics
requires the use of presheaves to ensure that the argument to $\Lam$
is stable under renaming. We refrain from presenting the details here.
It is well known that this semantics is equationally sound.
%This semantics can be implemented as
%another instance of $\Sem$.
%%(although of course we have to replace
%%typed closed terms with $\UTm$).
%To do this properly, we would have to
%take care of fresh name generation. But it turns out that in our uses
%of typed closed terms later as names of semantic elements there will
%be at most one bound variable at any time. We also notice that we get
%shorter normal forms by implementing a redundancy-avoiding version
%$\mathtt{if'}$ of $\If$ which produces a shorter but $\beta\eta$-equivalent
%term:
%\begin{code}
%if' :: Tm -> Tm -> Tm -> Tm
%if' t TTrue TFalse = t
%if' t u0 u1 = if u0 == u1 then u0 else If t u0 u1
%instance Sem Tm where
% true = TTrue
% false = TFalse
% xif = if'
% lam sigma f = Lam sigma "x" (f (Var "x"))
% app = App
%\end{code}
%Also this semantics is clearly equationally sound.
% =======================================================================
% =======================================================================
\section{Implementation of $\qquote$}
We now proceed to implementing $\qquote \in (\si \in \Ty) \to
\styeval{\si} \to \Tm\ \si$.
To define $\qquote^{\sigma\to\tau}$ we use $\enum^\sigma$, which
generates a decision tree whose leaves are all the elements of
$\tyeval{\si}$, and $\questions^\si$, which generates the list of
questions, i.e. elements of $\tyeval{\sigma}\to\tyeval{\Bool}$, based
on answers to whom an element of $\tyeval{\sigma}$ can be looked up in
the tree $\enum^\sigma$. (Since our decision trees are perfectly
balanced and we use the same list questions along each branch of a
tree, we separate the questions labelling from the tree.)
Decision trees $\Tree \in \Ty \to \type$ are provided by
\begin{code}
data Tree a = Val a | Choice (Tree a) (Tree a) deriving (Show, Eq)
\end{code}
We will exploit the fact that $\Tree$ is a monad
\begin{code}
instance Monad Tree where
return = Val
(Val a) >>= h = h a
(Choice l r) >>= h = Choice (l >>= h) (r >>= h)
\end{code}
(\texttt{return} and \texttt{>>=} are Haskell for the unit resp.\ the
bind or Kleisli extension operation of a monad) and hence a functor
\begin{code}
instance Functor Tree where
fmap h ds = ds >>= return . h
\end{code}
(\texttt{fmap} is Haskell for the action of a functor on morphisms).
It is convenient to use the function $\flatten$ which calculates
the list of leaves of a given tree:
\begin{code}
flatten :: Tree a -> [ a ]
flatten (Val a) = [ a ]
flatten (Choice l r) = (flatten l) ++ (flatten r)
\end{code}
We implement $\enum^\sigma$ and $\questions^\sigma$ by mutual
induction on $\si\in\Ty$. The precise typings of the functions are
$\enum \in (\si \in \Ty) \to \Tree\ \tyeval{\sigma}$ and $\questions
\in (\si \in \Ty) \to [ \tyeval{\sigma} \to \tyeval{\Bool} ]$. As
usual, Haskell cannot express those subtleties due to its lack of
dependent types, but we can declare
\begin{code}
enum :: Sem el => Ty -> Tree el
questions :: Sem el => Ty -> [ el -> el ]
\end{code}
The base case is straightforward: A boolean is true or false and to
know which one it is it suffices to know it.
\begin{code}
enum Bool = Choice (Val true) (Val false)
\end{code}
\begin{verbatim}
questions Bool = [ \ b -> b ]
\end{verbatim}
% --Haskell dislikes a function definition spread
The implementation of $\enum^{\si \Arr \ta}$ and $\questions^{\si \Arr
\ta}$ proceeds from the idea that a function is determined by its
graph: to know a function it suffices to know its value on all
possible argument values. The main idea in the implementation of
$\enum^{\si \Arr \ta}$ is therefore to start with $\enum^\tau$ and to
duplicate the tree for each question in $\questions^\sigma$ using the
bind of $\Tree$:
\begin{code}
enum (sigma :-> tau) =
fmap (lam sigma) (mkEnum (questions sigma) (enum tau))
mkEnum :: Sem el => [ el -> el ] -> Tree el -> Tree (el -> el)
mkEnum [] es = fmap (\ e -> \ d -> e) es
mkEnum (q : qs) es = (mkEnum qs es) >>= \ f1 ->
(mkEnum qs es) >>= \ f2 ->
return (\ d -> xif (q d) (f1 d) (f2 d))
\end{code}
%
$\questions^{\si\Arr\tau}$ produces the appropriate questions by
enumerating $\si$ and using questions from $\tau$:
\begin{comment}
\begin{code}
questions Bool = [ \ b -> b ]
\end{code}
\end{comment}
% --repeated from above
\begin{code}
questions (sigma :-> tau) =
[ \ f -> q (app f d) | d <- flatten (enum sigma),
q <- questions tau ]
\end{code}
As an example, the enumeration and questions for $\Bool \Arr \Bool$
return:
\begin{verbatim}
Choice
(Choice
(Val (lam Bool (\ d -> xif d true true)))
(Val (lam Bool (\ d -> xif d true false))))
(Choice
(Val (lam Bool (\ d -> xif d false true )))
(Val (lam Bool (\ d -> xif d false false))))
\end{verbatim}
resp.\
\begin{verbatim}
(\ f -> app f true :
(\ f -> app f false :
[]))
\end{verbatim}
We can look up an element in the decision tree for a type by answering
all the questions, this is realized by the function $\find$ below. To
define the domain of $\find$ precisely we define a relation between
lists of questions and trees of answers $\lockstep \subseteq [a] \times \Tree\ b$
inductively:
\ax{[] \lockstep (\Val\ t)}
\qquad
\ru{\as \lockstep l \quad \as \lockstep r}
{a:\as \lockstep \Choice\ l\ r}
%=======
%Let us define a relation $\lockstep \subseteq [A] \times \Tree\ B$
%inductively as follows:
%\begin{itemize}
%\item if $t \in B$, then $[] \lockstep \ts$,
%\item if $a \in A$, $\as \lockstep l$, $\as \lockstep r$, then $a : \as \lockstep \Choice\ l\ r$.
%\end{itemize}
%We have that $\questions^\si \lockstep \enum^\si$.
%>>>>>>> 1.31
Now given $\as \in [\tyeval{\Bool}]$, $\ts \in \Tree\,\tyeval{\si}$, s.t.
$\as \lockstep \ts$ we obtain $\find\ \as\ ts\in \tyeval{\si}$, implemented in Haskell:
\begin{code}
find :: Sem el => [ el ] -> Tree el -> el
find [] (Val t) = t
find (a : as) (Choice l r) = xif a (find as l) (find as r)
\end{code}
We are now ready to implement $\qquote^\sigma \in \styeval{\sigma} \to
\Tm\ \sigma$, with Haskell typing
\begin{code}
quote :: Ty -> El -> Tm
\end{code}
by induction on $\si\in\Ty$. As usual, the base case is easy:
\begin{code}
quote Bool STrue = TTrue
quote Bool SFalse = TFalse
\end{code}
$\qquote^{\si\Arr\tau}$ is more interesting: Our strategy is to map
$\qquote^\tau \circ f$ to the set-theoretic $\enum^\tau$ and to then
build a tree of $\If$ expressions by using the syntactic
$\questions^\sigma$ in conjunction with the syntactic $\find$:
\begin{code}
quote (sigma :-> tau) (SLam _ f) =
lam sigma (\ t -> find [ q t | q <- questions sigma ]
(fmap (quote tau . f) (enum sigma)))
\end{code}
(Notice that in Haskell it is inferred automatically which semantics
is meant where.)
As already discussed in the introduction, we implement normalization
$\nf \in (\sigma \in \Ty) \to \Tm\ \sigma \to \Tm\ \sigma$ by
\begin{code}
nf :: Ty -> Tm -> Tm
nf sigma t = quote sigma (eval [] t)
\end{code}
Since we can infer types, we can implement $\nf' \in \UTm \to \Maybe\
(\Sigma_{\sigma \in \Ty} \Tm\ \sigma)$:
\begin{code}
nf' :: Tm -> Maybe (Ty, Tm)
nf' t = do sigma <- infer [] t
Just (sigma, nf sigma t)
\end{code}
We test our implementation with the example from the introduction:
\begin{code}
b2b = Bool :-> Bool
once = Lam b2b "f" (Lam Bool "x" (App (Var "f") (Var "x")))
twice = Lam b2b "f" (Lam Bool "x" (App (Var "f")
(App (Var "f") (Var "x"))))
thrice = Lam b2b "f"
(Lam Bool "x" (App (Var "f")
(App (Var "f")
(App (Var "f") (Var "x")))))
\end{code}
and convince ourselves that $(\nf'\ \once \eq \nf'\ \thrice) =
\mathsf{true}$ but $(\nf'\ \once \eq \nf'\ \twice) = \mathsf{false}$.
Since semantic equality is decidable we do not actually have to
construct the normal forms to decide convertibility.
Since testing can only reveal the presence of errors we shall use the
rest of this paper to prove that $\qquote$ and hence $\nf$ behave
correctly.