This is the last article of this series. It’ll be a bit different than the previous ones: most of it will be about a step-by-step implementation of a λ-calculus interpreter (I’ll give you some starting points, in case you want to do it on your own).

We’ve already brushed upon the λ-calculus in the third article of this series on closures: Church encoding of booleans/integers/lists originates in the λ-calculus, where the only computation mean available precisely are functions/closures.

As a final conclusion, I’ll give you a few suggestions of code to read, and ideas to help you push your skills further, in continuation to what has been developed in those articles.

The code for this series remains available on github.

# Subject

** Exercise:** Look online for papers and course notes on the λ-calculus.
Shy away from existing implementation/code as much as possible: the more theoretical
the better. Try to implement an interpreter from them. The next section of this
article will be a step-by-step take on this exercise: I strongly encourage
you to give it a try without looking down further; it’s the hardest way, but also
the most profitable.

**[+]**

__Tip:__**[+]**

__Tip:__# Step-by-step

## Warm-up

** Exercise:** Find a precise definition of the
λ-calculus’ syntax, precise enough for you to be able to write
a parser.

You may want to sketch a potential parser, to see if the definition feels precise enough. When I say “sketch”, I mean to write enough convincing pseudo-code solving a representative subset of the parsing: the goal is to get acquainted with how to write the parser, not to write the parser.

**[+]**

__Solution:__** Exercise:** How would you translate Nix’s

`let ... in ...`

syntax
in λ-calculus? How would you express in λ-calculus the definitions of integers,
booleans and operations of them we established
earlier?**[+]**

__Solution:__** Exercise:** In order to familiarize yourself with the language,
try to manually evaluate the following λ-expressions:

```
(((λx. (λy. ((((λp. (λx. (λy. ((p x) y)))) x) (λx. (λy. x)))
((((λp. (λx. (λy. ((p x) y)))) y) (λx. (λy. x))) (λx. (λy. y))))))
(λx. (λy. x))) (λx. (λy. x)))
```

```
(((λx. (λy. ((((λp. (λx. (λy. ((p x) y)))) x)
((((λp. (λx. (λy. ((p x) y)))) y)
(λx. (λy. y))) (λx. (λy. x))))
((((λp. (λx. (λy. ((p x) y)))) y)
(λx. (λy. x))) (λx. (λy. y))))))
(λx. (λy. x))) (λx. (λy. x)))
```

**[+]**

__Tip:__**[+]**

__Solution:__** Exercise:** Interpreters/compilers are

*usually*written in a few different steps. The first one is about reading some input, breaking it into pieces and creating an internal representation of it (tokenizer, parser). How would you proceed to internally represent a parsed λ-term?

Define a few “constructors” for the different types of “objects” you’ll
be using to represent λ-terms; try to express the Church-encoded versions
of `true`

, `false`

and `and`

using such constructors.

(Interpreters/compilers are sometimes written in a single pass, but either those are exceptions, or the language is rather simple).

**[+]**

__Tip:__**[+]**

__Solution:__** Exercise:** Recall how we defined lists
earlier on, when we first
discovered how to recursively operate on them. What can you infer from
this regarding our λ-terms?

**[+]**

__Solution:__** Exercise:** Let’s put the previous observation into practice: write a

`toString t`

function which creates a string from a λ-term `t`

, where the
term is in the format previously described.*Write tests* to make sure `toString`

works, e.g. on our previously defined
Church-encoded booleans.

**[+]**

__Solution:__** Exercise:** Let’s keep practicing to write recursive functions on
λ-terms: a variable is said to be

*bound*if its name is captured by an abstraction. Otherwise, it’s said to be

*free*. For instance in \(\lambda\,x. y\,x\), \(x\) is bound while \(y\) is free.

- Write a function
`freeVars t`

which returns the*set*of free variables appearing in a λ-term`t`

; - Write a function
`allVars t`

which returns the*set*of all variables names used in a λ-term`t`

.

What do you think about testing those functions now?

**[+]**

__Solution:__## Parser

At this point, we can either develop the interpreter, or delve into the parser. However, having a parser can be convenient to write tests for the interpreter, because, as for the last exercise, not only we then don’t have to hand-compile λ-terms, but we also get more parsing tests for free.

So, we’re going to start with parsing.

Now, there are two main options for parsing: either you use the “basic” grammar of the language, the one we previously described in a previous exercise, or you allow “shortcuts”. Let’s recall the “basic” grammar:

\[\begin{aligned} T ::= x \mid\ ( \lambda x . \ T )\ \mid\ (T \, T) \\ x ::= \{a...z, A...Z\}+ \end{aligned}\]

** Exercise:** The issue with this grammar is that it’ll force
you to use parenthesis everywhere. From the examples we saw earlier,
this made things difficult to read/debug. But why could it still be
considered an interesting option, especially for a first try?

**[+]**

__Solution:__So, what’s a more convenient grammar? Well, here are some usual conventions: quoting [1], §2.1:

- We omit outermost parentheses. For instance, we write \(M\,N\) instead of \((M\,N)\);
- Applications associate to the left; thus, \(M\,N\,P\) means \((M\,N)\,P\). This is convenient when applying a function to a number of arguments, as in \(f\,x\,y\,z\), which means \(((f\,x)\,y)\,z\);
- The body of a lambda abstraction (the part after the dot) extends as far to the right as possible. In particular, \(λx.M\,N\) means \(λx.(M\,N)\), and not \((λx.M)\,N\);
- Multiple lambda abstractions can be contracted; thus \(λ\,x\,y\,z.M\) will abbreviate \(λx.λy.λz.M\).

** Note**: Regarding the last point, I’ll be using \(λ\,x.\,y.\,z.M\)
as an abbreviation for \(λx.λy.λz.M\). You may wonder why: I’m furthermore
allowing the λ to be optionals, so the previous λ-terms can also be
expressed as \(x.\,y.\,z.M\): I could have (I didn’t but it’s trivial to do)
allowed colons instead besides/instead of dots, and would have had a syntax
very close to Nix’s functions!

** Exercise:** Write a

`pretty t`

function which outputs the
λ-term `t`

as a string (like `toString`

then), but using similar conventions
instead.The goal is mainly to reduce the number of parentheses, so you don’t have
to strictly adhere to such conventions (well, for `pretty`

; we still do
for the parsing).

**[+]**

__Solution:__** Exercise:** What do you think about those simplifications? What
kind of issues do you expect to encounter?

**[+]**

__Solution:__Consider the first two rules. This is a typically
“annoying” problem given the strategy we’ve been using so far for parsing,
because if we want to parse \(M\,N\,P\), assuming we’re in `parseApply`

function, responsible for parsing an application (or delegating the parsing
to something else) the first thing we need to do, is to try to parse an application
(that is, \(M\,N\)). Meaning, we would start `parseApply`

by directly
calling `parseApply`

; this can’t end well…

We didn’t had the issue before, because for instance, when we had `T + T`

the first, leftmost `T`

we wanted to parse in `parseTerm`

wasn’t reached
by directly calling `parseTerm`

again, as `T`

was a factor, and thus should
be parsed by calling `parseFact`

.

Well nevermind you say. I can start by parsing something else, either a variable, a term, or something between parentheses, whatever (that is, \(M\)). Then look to the right to see there are some spaces followed by something else. “Ah-ah” you say! There is a \(N\), so its an application, and we have its left/right parts.

This is fine for parsing \(M\,N\), but what about \(M\,N\,P\)
(or \(M\,N\,P\,Q\))? Easy you say, I’ll just call `parseApply`

on
the right. But then you would have parsed \(M\,(N\,P)\), and your
applications are now *right*-associative instead of left-associative!

No problem you say, I’ll just rearrange the terms a little to get \((M\,N)\,P\), and voilà.

** Exercise:** What’s the problem with this solution? How would you
make it work?

**[+]**

__Tip:__**[+]**

__Solution:__** Exercise:** I guess we now have everything to write the
complete parser. You may want to test it “systematically”: it’s very easy
to make small mistakes that can alter previously working code. Unless
you’re really smart, having some written tests is a good “long-term”
investment. This also allows you to implement the parser incrementally,
one feature at a time, one convention at a time.

**[+]**

__Solution:__## Interpreter

I think writing a parser for the non-“basic” grammar was actually the most difficult part of this exercise. The interpreter feels easier: the algorithms are essentially those you’ve been using since you’ve started to program. That’s to say, the hardest part is behind us.

** Exercise:** (α-equivalence) Write a function

`rename m y x`

, which
renames the variable named `x`

to `y`

in the λ-term `t`

(`x/y`

are strings
then); for instance,
noting \(M_{\{y/x\}}\) to rename \(x\) by \(y\) in \(M\):\[\begin{aligned} (\lambda\ x.x\ x)_{\{y/x\}} & \qquad\rightarrow & (\lambda\ y.y\ y) \\ (z\ x)_{\{x/y\}} & \qquad\rightarrow & (z\ x) \end{aligned}\]

Terms obtained by such a renaming operations are said to be **α-equivalent**.

**[+]**

__Tip:__**[+]**

__Solution:__** Exercise:** (β-substitution) Write a function

`substitute m n x`

,
which substitute the *term*

`x`

by the *term*

`y`

in the λ-term `t`

,
for instance, noting \(M_{[N/x]}\) to replace \(x\) by \(N\) in \(M\):\[\begin{aligned} (\lambda\ x.x\ x)_{[N/x]} &\qquad\rightarrow & (\lambda\ x.x\ x) \\ (z\ x)_{[\lambda\ z.\ y\ x/x]} &\qquad \rightarrow & (z\ (\lambda\ z.\ y\ x)) \\ (\lambda\ x.y\ x)_{[(\lambda\ z.\ y\ x)/y]} &\qquad\rightarrow & (\lambda\ x_0.\ (\lambda\ z.\ y\ x)\ x_0) \\ \end{aligned}\]

**[+]**

__Tip:__**[+]**

__Solution:__Strictly speaking, the λ-calculus doesn’t come with an evaluation strategy, and thus isn’t a real programming language, nor can it be evaluated. But by abuse of language, we often say that it can, and I will follow this habit.

So, how should we “evaluate” the λ-calculus? We’ll simply try
to perform all possible **β-reductions** on a λ-term, until we can’t
reduce things any further.

** Exercise:** Write a function

`eval t`

, which evaluates
a given λ-term `t`

.**[+]**

__Tip:__**[+]**

__Solution:__Here’s the final implementation:

```
#!/usr/bin/env -S nix-instantiate --eval
with builtins;
with (import ./string/strings.nix);
with (import ./string/ascii.nix);
rec {
/*
* "Types"/constructors
*/
# (m n)
mkApply = m: n: { type = "apply"; left = m; right = n; };
# (λx. m)
mkLambda = x: m: { type = "lambda"; bound = x; expr = m; };
# x
mkVar = x: { type = "var"; name = x; };
/*
* Auxiliary
*/
# isPunct could have been in string/ascii.nix
isPunct = c: hasAttr c {
"(" = true;
")" = true;
"." = true;
};
# skipBlacks could have been in string/strings.nix
skipBlacks = s: n: if !isWhite (charAt s n) && !isPunct(charAt s n) && charAt s n != ""
then skipBlacks s (n + 1) else n;
toString = m:
if m.type == "var" then
m.name
else if m.type == "lambda" then
"(λ"+m.bound+"."+" "+(toString m.expr)+")"
else
"("+(toString m.left)+" "+(toString m.right)+")"
;
# prettier toString
pretty = m: let aux = m: inLambda: inApp:
if m.type == "var" then
m.name
else if m.type == "lambda" then
if inLambda then
m.bound+"."+" "+(aux m.expr true false)
else
"(λ"+m.bound+"."+" "+(aux m.expr true false)+")"
else if inApp then
(aux m.left false true)+" "+(aux m.right false false)
else
"("+(aux m.left false true)+" "+(aux m.right false false)+")"
; in aux m false false;
freeVars = m:
if m.type == "var" then { ${m.name} = true; }
else if m.type == "apply" then
(freeVars m.left) // (freeVars m.right)
else
removeAttrs (freeVars m.expr) [m.bound];
allVars = m:
if m.type == "var" then { ${m.name} = true; }
else if m.type == "apply" then
(allVars m.left) // (allVars m.right)
else
{ ${m.bound} = true; } // (allVars m.expr);
# Computes a relatively fresh variable name from a set of
# used names
getFresh = xs:
let aux = n:
if hasAttr "x${builtins.toString n}" xs then
aux (n + 1)
else "x${builtins.toString n}"
; in aux 0;
isFree = m: x: hasAttr x (freeVars m);
/*
* Parsing
*/
start = {
# input buffer
s = "";
# pointer to input buffer
p = 0;
err = null;
# parsed expression
expr = {};
};
atEOF = s: s.p == (stringLength s.s);
hasErr = s: s.err != null;
peek1 = s: charAt s.s (skipWhites s.s s.p);
next1 = s: s // { p = (skipWhites s.s s.p) + 1; };
peekw = s: let q = skipWhites s.s s.p; in
substring q ((skipBlacks s.s q) - q) s.s;
nextw = s: s // {
p = skipBlacks s.s (skipWhites s.s s.p);
};
parseUnary = s:
if atEOF s then s // { err = "unexpected EOF"; }
else if (peek1 s) == "(" then let
t = parseExpr (next1 s);
in if hasErr t then t
else if (peek1 t) != ")" then
t // { err = "expecting ')'"; }
else
next1 t
else let w = peekw s; in
if w == "" then s // { err = "word expected"; }
else nextw s // { expr = mkVar w; }
;
# no utf-8 support; "λ" is two bytes long
hasLambda = s: p: substring (skipWhites s p) 2 s == "λ";
skipLambda = s: next1 (next1 s);
# the lambda is optional, i.e (f. x) <=> (λf. x)
parseLambda = s:
let
b = hasLambda s.s s.p;
t = if b then skipLambda s else s;
in let
w = peekw t;
u = nextw t;
in if peek1 u == "." then let v = parseExpr (next1 u); in
if hasErr v then v
else v // { expr = mkLambda w v.expr; }
else if b then
u // { err = ". expected after λ"; }
else parseUnary s;
hasMore = s:
let
q = skipWhites s.s s.p;
c = charAt s.s q;
in q != stringLength s.s &&
(c == "(" || (hasLambda s.s q) || !(isPunct c));
parseApply = s:
let aux = acc: s: let t = parseLambda s; in
if hasErr t then t
else let
a = if acc == {} then t.expr else mkApply acc t.expr;
in if hasMore t then aux a (t // { expr = {}; })
else t // { expr = a; }
; in aux {} (s // { expr = {}; });
parseExpr = s: parseApply s;
parse = s: parseExpr (start // { s = s; });
/*
* Interpretation/evaluation
*/
# α-equivalence, M{y,x} (renaming x as y in M)
rename = m: y: x:
if m.type == "var" then m // {
name = if m.name == x then y else m.name;
} else if m.type == "apply" then m // {
left = rename m.left y x;
right = rename m.right y x;
} else m // {
bound = if m.bound == x then y else m.bound;
expr = rename m.expr y x;
};
# β-substitution, M[N/x] (substituing x for N in M)
substitute = m: n: x:
if m.type == "var" then
if m.name == x then n else m
else if m.type == "apply" then m // {
left = substitute m.left n x;
right = substitute m.right n x;
} else
if m.bound == x then m
else if ! (isFree n m.bound) then m // {
expr = substitute m.expr n x;
} else let
y = getFresh (
(allVars m.expr) //
(allVars n) //
{ ${x} = true; /* ?? "${m.bound}" = true; */ }
);
in m // {
bound = y;
expr = substitute (rename m.expr y m.bound) n x;
};
reduce = m: /* trace(pretty m) */ (
if m.type == "lambda" then
m // { expr = reduce m.expr; }
else if m.type == "var" then
m
else if m.left.type == "lambda" then
substitute m.left.expr m.right m.left.bound
else
m // { left = reduce m.left; right = reduce m.right; }
);
eval = m: let n = reduce m; in
if n == m then n else eval n;
}
```

# Going further

If you’ve made it this far, working all the exercises, and didn’t knew much of this material before starting, then congratulations. Some of this stuff isn’t “easy” (well, for most people, there are always some offbeat fellows). Anyway, here are a few additional pointers that you may find interesting:

**De Bruijn index**: One can bypass having
to name bound variables in λ-calculus, and replace them by well-chosen
integers. You could try to start by parsing λ-terms represented with
De Bruijn indexes to get a feel for them, and then see if you could
use them internally; this should avoid the need for α-renaming.

**Typed λ-calculus**: a natural way to continue where we just stopped;
Selinger’s notes have a good introduction to the
topic. You could also try to use a more strongly typed functional
programming languages such as Haskell or OCaml.

**Parsing/interpreters in Nix**: If you want to read Nix code building
on the topics we’ve covered in this series:

- A Lisp interpreter (nixlisp) written in Nix;
- A parsec Nix implementation (nix-parsec); parsec is originally a Haskell library to help write parsers, used by nixlisp.

**C and/or assembly language:** the ability to write low-level code is very
orthogonal to the skills developed here, much more practical, down to
Earth. If you enjoyed interpreters, you could try to write *compilers*,
emitting C or assembly. You could also take the time to study
operating systems: wiki.osdev.org must be one of the best starting
point.

**Compilation**: There *lots* of tutorials and books on the subject.
A few months ago, I’ve spent some time reading some parts of
craftinginterpreters.com: its author do use
recursive descent parsing to write the first version of his interpreter.
This might be a great way to smoothly transition from a minuscule
language to something more realistic.

**SICP, Lisp & Scheme**: Already mentioned lightly earlier: the
SICP
is a (free) introduction to computer science used at the MIT, showcasing
Scheme/Lisp. Still in the functional realm, but away from strongly-typed languages. A
specificity of Lisp & co. is their powerful macro-system due to Lisp’s
homoiconicity: Lisp programs *are* lists, that you
can alter/generate with Lisp code.

# Ninix

** Challenge:** Write an as-complete as possible Nix interpreter,
in Nix. I won’t be posting a solution because I won’t have time to tackle it
in the near future, but I guess this is a fun project. You could also to use an
other language to implement the interpreter.

**[+]**

__Tip:__
## Comments

By email, at mathieu.bivert chez: