Some time ago, I presented an article on this blog about functional programming and lambda calculus. Today, I’ll try to implement lambda calculus simply in Haskell. For a more casual introduction to lambda calculus, I invite you to read my other article.
I will mostly follow the book “Types and Programming Languages” by Benjamin C. Pierce from the section 5.1 to 5.4, but I will implement it from scratch using Haskell instead of ML. The code is freely available on my github repository.
Abstract and concrete syntax
The first step in implementing a programming language is to define its syntax. The syntax of a programming language is usually defined by a grammar, which is a set of rules that describe how to form valid programs in the language. There are two kinds of syntax: abstract syntax and concrete syntax.
The abstract syntax of a programming language is a set of data structures that represent the structure of programs in the language, usually represented as Abstract Syntax Trees ( ASTs) while the concrete syntax is the textual representation of the programs in the language. The first step is then to convert the strings of character representing the program into a AST using a parser (and optionally a lexer and a tokenize).
Syntax of the untyped lambda calculus
The untyped lambda calculus is a simple programming language that has only three constructs: variables, abstractions, and applications. The syntax of the language is defined by the following grammar:
$$ \begin{aligned} \text{Term} &::= \text{Variable} \mid \text{Abstraction} \mid \text{Application} \\ \text{Variable} &::= \text{x} \\ \text{Abstraction} &::= \lambda \text{x } . \text{ t} \\ \text{Application} &::= \text{t } \text{ t}\\ \end{aligned} $$
It means that in this language, any term is either a variable $x$ by itself, an abstraction $\lambda x . M$ or an application $M N$, where $M$ and $N$ are any terms. Any of those terms represent a valid program, which means that the language is very simple and expressive.
Here, $x$ is variable while $t$ is a metavariable representing any term. The symbol $\lambda$ is the lambda symbol, and the dot is the body of the abstraction. The application is left-associative, which means that $M N P$ is equivalent to $(M N) P$.
Semantics of the untyped lambda calculus
Paying attention to the definition of lambda calculus, we remark that there is no built-in constant or primitive operators. Computing is equivalent to applying a function to an argument (application) and writing a function is equivalent to use a lambda abstraction. This makes the lambda calculus a very simple, expressive language and powerful language.
Thus, the computation or evaluation of a lambda expression is applying the application of functions to argument (which themselves are functions). It leads to a reduction of the expression, until we reach a normal form, which is a term that cannot be reduced anymore. Each step of the evaluation consists of replacing a subterm of the form $(\lambda x . M) N$ by $M[x := N]$, where $M[x := N]$ is the term obtained by replacing all the free occurrences of $x$ in $M$ by $N$. This is called $\beta$-reduction. The final values of the program can then be any abstraction.
There exists different strategies to reduce the expression, but we will only discuss the most use, which is the call by value strategy. In this strategy, only outermost redexes are reduced, and the argument of a function is reduced to a value before the function is applied.
This strategy can be defined formally by the following rules: $$ \begin{aligned} t_1 \rightarrow t_1’ &\implies t_1 t_2 \rightarrow t_1’ t_2 \\ t_2 \rightarrow t_2’ &\implies v_1 t_2 \rightarrow v_1 t_2’ \\ (\lambda x . t) v &\rightarrow t[x := v] \\ \end{aligned} $$
Nameless representation of terms
In the previous section, we defined the syntax of the untyped lambda calculus using variable names. However, in practice, it is more convenient to use a nameless representation of terms. In this representation, variables are replaced by de Bruijn indices, which are natural numbers that represent the number of binders between the variable and its corresponding abstraction. For example, the term $\lambda x . \lambda y . x y$ can be represented as $\lambda . \lambda . 1 0$. This representation is more convenient because it avoids the need to deal with variable names, which can be tricky to handle in practice. It also makes it easier to implement substitution and $\alpha$-conversion, which are two important operations in lambda calculus.
The difficulty is to keep track of the number of free variables in the term, and to shift the indices when we add or remove abstractions. This is a bit tricky, but it is a very important step in the implementation of the lambda calculus. The implementation of the lambda calculus needs to define the substitution operation using a shift operator. The shift operator is a function that takes a term and a number n, and returns a new term in which all the free variables have been shifted by n. The substitution operation can then be defined in terms of the shift operator.
Implementing the untyped lambda calculus in Haskell
We will now implement the untyped lambda calculus in Haskell. We will start by defining the abstract syntax of the language, and then we will implement the semantics of the language. We will also implement the shift and substitution operations, and we will define a function that reduces a term to its normal form using the call by value strategy.
Now, let’s start by showing an example of what a program will look like. The following is a simple program that represents the identity function:
LAMBDA x. x
In this representation, application are written with operator LAMBDA and .. Application will be represented by two terms separated by a space like in the following abstraction : LAMBDA x. (x x).
Implementing the parser with Parsec
Let’s open a new Haskell project and define a file called Parser.hs in src. We will use the Parsec package in order to write the parser which will convert the string representation of the program into an AST. Let’s start by defining what is a term, following our previous definition:
module Parser
( parseLambda,
parserLambda',
Term(..)
) where
import Data.List
import Text.Parsec
import Text.Parsec.String (Parser)
import Text.Parsec.Expr
import Control.Monad.Identity (Identity)
-- Define a data type for lambda calculus expressions
data Term
= Abstraction String Term -- Abstraction: (LAMBDA x. T)
| Application Term Term -- Application: (T1 T2)
| Var String -- Variable: x
deriving Show
```
Now let's define the parser for the lambda calculus which will convert the string representation of the program into a `Term`:
```haskell
-- Define a parser for lambda calculus expressions
lambdaTerm :: Parser Term
lambdaTerm = lambdaAbstraction <|> lambdaApplication <|> simple
simple :: Parser Term
simple = lambdaVar <|> paren <|> churchNum <|> encodings
Now let’s define more specifically what is a lambda abstraction:
lambdaAbstraction :: Parser Term
lambdaAbstraction = do
string "LAMBDA"
spaces
var <- letter -- <|> char '$' <|> char '#'
char '.'
spaces
body <- lambdaTerm
return(Abstraction [var] body)
We see indeed that the lambda abstraction is defined by the keyword LAMBDA followed by a variable and a dot, and then the body of the abstraction. The variable is defined by a letter, and the body is any term. The Parsec package make it very easy to define such a parser, and it is very readable.
Now let’s move to the definition of the parser of a variable, which should be single letter:
lambdaVar :: Parser Term
lambdaVar = do
var <- letter
return(Var [var])
We can also define the lambda application parser easily:
lambdaApplication :: Parser Term
lambdaApplication = do
t1 <- simple
spaces
t2 <- many lambdaApplication <|> many simple
return(foldl Application t1 t2)
We still needs to define some terms defined in simple, meaning paren which is a simple parenthesis parser, churchNum which is a parser for church numerals, and encodings which is a parser for some encoding specific encodings corresponding to particular lamnda expressions.
paren :: Parser Term
paren = between (char '(') (char ')') lambdaTerm
-- Parse positive integers as Church numerals
churchNum :: Parser Term
churchNum = do
v <- many1 digit
return(Abstraction "s" (Abstraction "z" (applyTimes (read v :: Int))))
-- Apply the successor function n times
applyTimes 0 = Var "z"
applyTimes n = Application (Var "s") (applyTimes (n-1))
encodings :: Parser Term
encodings = do
char '@'
datatype <- many letter
return(stringToTerm (case datatype of
"succ" -> "(LAMBDA n. (LAMBDA f. (LAMBDA x. f (n f x))))"
"pred" -> "(LAMBDA n. LAMBDA f. LAMBDA x. n (LAMBDA g. LAMBDA h. h (g f)) (LAMBDA u. x) (LAMBDA u. u))"
"plus" -> "(LAMBDA m. (LAMBDA n. (LAMBDA f. (LAMBDA x. ((m f) (n (f x)))))))"
"sub" -> "(LAMBDA m. LAMBDA n. LAMBDA s. LAMBDA z. (m s) (n (s z)))"
"true" -> "(LAMBDA t. (LAMBDA f. t))"
"false" -> "(LAMBDA t. (LAMBDA f. f))"
"and" -> "(LAMBDA p. LAMBDA q. (p q) p)"
"or" -> "(LAMBDA p. LAMBDA q. (p p) q)"
"not" -> "(LAMBDA p. (p @false) @true)"
))
This will allow to represent with this encoding some specific lambda expressions which represent usual objects like integers and booleans. For more information about this encoding, you can refer to the Church Encoding page on Wikipedia. You can note that this encoding is somewhat arbitrary and everything is indeed a lambda abstraction.
We can now define the main parser for the lambda calculus:
-- Parse a lambda expression from a string
parseLambda :: String -> Either ParseError Term
parseLambda = parse lambdaTerm ""
stringToTerm :: String -> Term
stringToTerm str = case (parse lambdaTerm "" str) of
Left msg -> error $ show msg
Right term' -> term'
parserLambda' :: String -> String
parserLambda' x = case parseLambda x of
Left err -> error $ show err
Right expr -> show expr
The stringToTerm function will be used to return a Term directly and throw an error if the expression is unparsable, which will be used by the evaluator.
The parserLambda' function will be used to return a string representation of the Term and throw an error if the expression is unparsable, which is used for debugging purpose. We will the latter to show the result of the parsing to transform the code to AST.
$ stack ghci
Let’s try our module in the REPL:
λ> parserLambda' "LAMBDA x. x"
"Abstraction \"x\" (Var \"x\")"
λ> parserLambda' "LAMBDA x. (x x)"
"Abstraction \"x\" (Application (Var \"x\") (Var \"x\"))"
We can see that the parser is working well, and that it is able to parse the string representation of the program into an AST. We will now be able to implement the semantics of the language, and then we will be able to reduce the expression to its normal form.
Implementing the Evaluator in Haskell
We will now implement the semantics of the untyped lambda calculus in Haskell. The task is more difficult because of the handling of the nameless representation. Let’s start by opening a new file in src called Evaluator.hs.
module Evaluator
( evaluator
) where
import Data.List
import Parser (Term(..), parseLambda)
import Control.Exception
type Info = Integer
type Context = [(String, Binding)]
data Binding = NameBind deriving Show
data NlTerm = NlVar Info Integer Integer
| NlAbs Info String NlTerm
| NlApp Info NlTerm NlTerm
deriving (Show, Eq)
We are defining a new data type NlTerm which is the nameless representation of the term. We will also define a new type Context which is a list of bindings, and a new type Binding which is a simple data type to represent a binding. We will also define a new type Info which is a simple alias for Integer.
Let’s start by writting a function to plot the NLTerm in the result based on a context, which will allow nice final values once an expression is evaluated:
termToString :: Context -> NlTerm -> String
termToString ctx (NlAbs info x t1) =
let (x', ctx') = freshName x ctx
in "(LAMBDA " ++ x' ++ ". " ++ termToString ctx' t1 ++ ")"
termToString ctx (NlApp info t1 t2) = termToString ctx t1 ++ " " ++ termToString ctx t2
termToString ctx (NlVar info x n) = fst (getIndexElement ctx (fromIntegral x))
Now let’s start the fun and define a function termShift which will shift the indices of the free variables in a term by a given amount:
termShift :: Integer -> NlTerm -> NlTerm
termShift d t =
let
walk :: Integer -> NlTerm -> NlTerm
walk c (NlVar info x n) =
if x >= c then (NlVar info (x + d) (n + d)) else (NlVar info x (n + d))
walk c (NlAbs info x t1) = NlAbs info x (walk (c + 1) t1)
walk c (NlApp info t1 t2) = NlApp info (walk c t1) (walk c t2)
in
walk 0 t
In this function, we are defining a function walk which will walk through the term and shift the indices of the free variables by a given amount. We are using a simple recursion to walk through the term and apply the shift to the free variables. We are also using a simple if statement to check if the variable is free, and if it is, we are applying the shift to it. If the argument is a variable, we are applying the shift to it.
We will also define a function termSubst which will substitute a term for a variable in another term:
termSubst :: Integer -> NlTerm -> NlTerm -> NlTerm
termSubst j s t =
let
walk :: Integer -> NlTerm -> NlTerm
walk c (NlVar info x n) = if x == j + c then termShift c s else (NlVar info x n)
walk c (NlAbs info x t1) = NlAbs info x (walk (c + 1) t1)
walk c (NlApp info t1 t2) = NlApp info (walk c t1) (walk c t2)
in
walk 0 t
Similarly, the walk function will recursively apply the substitution to the term. Notice that when we are crossing an abstraction, we are increasing the counter by 1 in order to keep track of the number of free variables in the term.
The termSubstTop function will simply the term substitution at the top level:
termSubstTop :: NlTerm -> NlTerm -> NlTerm
termSubstTop s t = termShift (-1) (termSubst 0 (termShift 1 s) t)
Now let’s finally define the evaluation process it self with:
isvalfunction which will check if a term is a value:
isval :: NlTerm -> Bool
isval (NlAbs _ _ _) = True
isval _ = False
eval'function which will do one step of beta reduction:
eval' :: Context -> NlTerm -> NlTerm
eval' ctx t = case t of
NlApp info (NlAbs _ x t12) v2 | isVal ctx v2 ->
termSubstTop v2 t12
NlApp info v1 t2 | isVal ctx v1 ->
let t2' = eval' ctx t2 in
NlApp info v1 t2'
NlApp info t1 t2 ->
let t1' = eval' ctx t1 in
NlApp info t1' t2
_ ->
t
evalfunction which will reduce the term to its normal form:
eval :: Context -> NlTerm -> NlTerm
eval ctx t = let t' = (eval' ctx) t
in (if t' == t then t else eval ctx t')
Everything is almost ready, now the final touch is to write the code which will convert term to nameless representation.
---------------- Convert Term to Nameless representation
-- Function to convert a lambda term to its nameless representation
termToNlTerm :: Term -> Context -> (NlTerm, Context)
termToNlTerm (Var x) ctx =
case lookupIndex x ctx of
Just index -> (NlVar 0 (toInteger index) (toInteger $ length ctx), ctx)
Nothing -> error "Variable not found in context"
termToNlTerm (Abstraction x body) ctx =
let newCtx = (x, NameBind) : ctx
(newBody, updatedCtx) = termToNlTerm body newCtx
in (NlAbs 0 x newBody, updatedCtx)
termToNlTerm (Application t1 t2) ctx =
let (nlT1, ctx1) = termToNlTerm t1 ctx
(nlT2, ctx2) = termToNlTerm t2 ctx1
in (NlApp 0 nlT1 nlT2, ctx2)
-- Helper function to generate a fresh name
freshName :: String -> Context -> (String, Context)
freshName x ctx = case lookupIndex x ctx of
Just index -> (x ++ "'", (x ++ "'", NameBind) : ctx)
Nothing -> (x, ctx)
-- Helper function to lookup the index of a variable in the context
lookupIndex :: String -> Context -> Maybe Int
lookupIndex x ctx = elemIndex x (map fst ctx)
getIndexElement :: [a] -> Int -> a
getIndexElement list index
| index < 0 = error ":'(" -- Index is negative
| index < length list = (head (drop index list)) -- Index is within bounds
| otherwise = error ":'(" -- Index is out of bounds
In this piece of code, termToNlTerm is a function that takes a term and a context, and returns the nameless representation of the term and the updated context. The function is defined using pattern matching on the term, and it uses a helper function freshName to generate a fresh name for the variable. The freshName function takes a variable and a context, and it returns a fresh name for the variable and the updated context. The lookupIndex function is a helper function that takes a variable and a context, and it returns the index of the variable in the context. The getIndexElement function is a helper function that takes a list and an index, and it returns the element at the given index in the list.
The exposed function of the module, evaluator is simply something which parse a lambda expression, and then convert it to a nameless representation, and then evaluate it to its normal form.
---------------- Complete Evaluator
evaluator :: String -> String
evaluator x = case parseLambda x of
Left err -> show err
Right expr ->
let (term, ctx) = termToNlTerm expr []
in termToString ctx (eval ctx term)
Now let’s try our module in the REPL:
ghci> evaluator "LAMBDA x. x"
"(LAMBDA x'. x')"
ghci> evaluator "LAMBDA x. (x x)"
"(LAMBDA x'. x' x')"
ghci> evaluator "(LAMBDA x. x) (LAMBDA t. t) (LAMBDA e. (e e))"
"(LAMBDA e'. e' e')"
We also implemented church numerals and booleans, let’s try it out:
ghci> evaluator "@true"
"(LAMBDA t'. (LAMBDA f'. t'))"
ghci> evaluator "@false"
"(LAMBDA f'. (LAMBDA t'. f'))"
ghci> evaluator "@succ"
"(LAMBDA n'. (LAMBDA f'. (LAMBDA x'. f' n' f' x')))"
ghci> evaluator "@sub"
"(LAMBDA m'. (LAMBDA n'. (LAMBDA s'. (LAMBDA z'. m' s' n' s' z'))))"
ghci> evaluator "(@or @true) @false"
"(LAMBDA t'. (LAMBDA f'. t'))"
ghci> evaluator "1"
"(LAMBDA s'. (LAMBDA z'. s' z'))"
ghci> evaluator "2"
"(LAMBDA s'. (LAMBDA z'. s' (s' z')))"
ghci> evaluator "3"
"(LAMBDA s'. (LAMBDA z'. s' (s' (s' z'))))"
ghci> evaluator "@(plus 1) 1"
"(LAMBDA f'. (LAMBDA x'. (LAMBDA f'. (LAMBDA x'. f' x')) f' (LAMBDA f'. (LAMBDA x'. f' x')) f' x'))"
The implementation is working well, except the last line where there is problem when using the numeral operators, which seems to be due to the parsing of the expression or the evaluation which does not terminate well. We will need to fix this issue, and also to add some tests to make sure that the implementation is working well. If you have a solution for this email me!
Conclusion
In this article, we’ve built the untyped lambda calculus in Haskell. We handled everything from defining the language’s structure to making it work with shift and substitution operations. Our implementation includes a parser for turning program strings into code and an evaluator to run it. While our tests show it’s mostly working fine, we’ve noticed some glitches with numeral operators that need fixing. Next steps involve smoothing out these issues and beefing up our testing game.