\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.