You may want to inform yourself about human rights in China.

On Nix's Language: Lambda Calculus Interpreter

tags: computing nix
date: 2022-12-11
update: 2024-07-18

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:[+]
Morning in a pine forest (Утро в сосновом лесу, 1889), oil on canvas, 139×213 cm

Morning in a pine forest (Утро в сосновом лесу, 1889), oil on canvas, 139×213 cm by Ivan Ivanovich Shishkin (Ива́н Ива́нович Ши́шкин, 1832-1898) through wikimedia.orgPublic domain

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.

What do you think about testing those functions now?

Solution:[+]
Before a thunderstorm (Перед грозой, 1884), oil on canvas, 110×150cm

Before a thunderstorm (Перед грозой, 1884), oil on canvas, 110×150cm by Ivan Ivanovich Shishkin (Ива́н Ива́нович Ши́шкин, 1832-1898) through wikimedia.orgPublic domain

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:

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:[+]
Herd in the forest (Стадо в лесу, 1864), oil on canvas

Herd in the forest (Стадо в лесу, 1864), oil on canvas by Ivan Ivanovich Shishkin (Ива́н Ива́нович Ши́шкин, 1832-1898) through wikiart.orgPublic domain

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:[+]
Ship grove (Опушка леса, 1884), oil on canvas, 71×57cm

Ship grove (Опушка леса, 1884), oil on canvas, 71×57cm by Ivan Ivanovich Shishkin (Ива́н Ива́нович Ши́шкин, 1832-1898) through wikimedia.orgPublic domain

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:[+]
Ship grove (Корабельная роща, 1898), oil on canvas, 165×252cm

Ship grove (Корабельная роща, 1898), oil on canvas, 165×252cm by Ivan Ivanovich Shishkin (Ива́н Ива́нович Ши́шкин, 1832-1898) through wikimedia.orgPublic domain

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:[+]
Pine on sand (c. 1884), oil on canvas, 69×105cm

Pine on sand (c. 1884), oil on canvas, 69×105cm by Ivan Ivanovich Shishkin (Ива́н Ива́нович Ши́шкин, 1832-1898) through wikimedia.orgPublic domain

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
	 */

	# α-renaming, 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:

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:[+]
The road in the rye (Дорога во ржи, 1866), oil on canvas

The road in the rye (Дорога во ржи, 1866), oil on canvas by Ivan Ivanovich Shishkin (Ива́н Ива́нович Ши́шкин, 1832-1898) through wikiart.orgPublic domain


In the series:


Comments

By email, at mathieu.bivert chez:

email