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.
I advise you to start by getting acquainted with the λ-calculus first:
try to evaluate a few expressions by hand, get a feel for how it works. This
shouldn't be too difficult if you've been following this series: after all,
the λ-calculus merely encodes rewriting rules close to those of
ordinary function calls.
Regarding the code, spend some time thinking about your data structures,
and about the functions you'll need. Despite Nix not being statically
typed, as a programmer, you can always "type" your functions: it's good
habit to understand what they take as input, and what they take as output.
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.
As a main reference throughout this article, I'll be using
those notes by Peter Selinger:
they are clear, exhaustive, and contain a bunch of exercises. Section 2.1
contains a grammar; I'll tweak it a bit to make explicit that we'll
want multi-character variables names; all the involved tokens can be naturally
separated by whitespaces (spaces, tabs, newlines):
\[\begin{aligned}
T ::= x \mid\ ( \lambda x . \ T )\ \mid\ (T \, T) \\
x ::= \{a...z, A...Z\}+
\end{aligned}\]
I'll use from now on the following standard terminology:
\(T\) is a λ-term;
\(x\) is a variable;
\(( \lambda x . \ T )\) is an abstraction;
and \((T \, T)\) is an application.
As for the parser sketch, essentially, we'll want one parsing function
per "object" we can parse, and to chain all the function calls as we
did with the mathematical expression parser. I'll expand that sketch
some more in the beginning of the next subsection (Parser§), before
updating this grammar to something more practical (but more difficult
to parse).
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?
let ... in ... can be considered as some sort
of syntactic sugar over imbricated abstractions being applied to
the corresponding definitions. Here's an example how we could
for some Church booleans/integers related definitions:
I encourage you to revisit and deepen your appreciation of
Church integers/booleans. Selinger has a few exercises on the
topic, you should be able to find solutions on the Internet:
it's a great way to get familiar with the λ-calculus.
Perhaps a first thing to notice is how messy those look. One
reason being that, for now, our description of the language doesn't
allow us to avoid unnecessary parentheses.
Other reasons include the lack let ... in ...-like
sugar coating, and of any meaningful indentation.
Finally, we really haven't defined what do we mean by evaluating
a λ-term. You may still be able to find a way to do so,
as it should be rather intuitive for a programmer. But
a clear reformatting, some syntactic sugar, and identification
of Church-encoded booleans and related could be another
way to make things clear.
Here's what those two look like after some cleanup:
((λ ifelse.
(λ F.
(λ T.
(λ or.
((or T) T
))(λx. (λy. (((ifelse x) T)(((ifelse y) T) F)))))(λx. (λy. x)))(λx. (λy. y)))(λp. (λx. (λy. ((p x) y)))))
((λ ifelse.
(λ F.
(λ T.
(λ xor.
((xor T) T
))(λx. (λy. (((ifelse x)(((ifelse y) F) T))(((ifelse y) T) F)))))(λx. (λy. x)))(λx. (λy. y)))(λp. (λx. (λy. ((p x) y)))))
Finally, what do we mean by evaluating such an expression?
Well, intuitively, "we call functions with their arguments".
But more precisely, we perform β-reductions
until we can't do so anymore. And what's a β-reduction?
For now, we don't really need to know more than the previous
"intuitive" description. But your paper/notes should be clear
about it.
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).
You may want to take inspiration from the mathematical expressions
parser.
As a side note, there's an (important) saying in computer science:
"data dominates".
Meaning, the code and algorithms merely go through the data structures
you've chosen. Often, a wise choice of data structure can help make the
code dumb and simple, although perhaps subtle. On the other hand, poor
choices of data structures can contribute to complex code, difficult to
write and maintain.
Sketching the code as you design data-structures
is an excellent middle-ground: you can heuristically evaluate the quality
of your data structures by measuring the complexity of the induced functions.
Recall how Nix's authors made a special cases out of small lists of
one and two items to avoid memory allocation: such an optimization
looks reasonable,
but it also made lists less uniform within their C++ interpreter.
As a result, they needed to add a layer of abstraction to hide it.
That's a typical example of:
How a more complex data structure increases code complexity,
at best locally/in a controlled fashion;
How to voluntarily make things more complex for good reasons:
aiming at simple thing is nice, but in real life, one must also
meet practical requirements.
When parsing, trees are almost always the key data-structure. In
our case:
Variables will be the leaves of the tree;
Both abstractions and applications (e.g. respectively,
for \(M, N\) arbitrary λ-terms, \(( \lambda x . \ M )\) and
\((N \, M)\)) will be intermediate nodes;
As we've done earlier for the mathematical expression parser, we
can represent them by sets, and use some "constructors" to create
them:
#!/usr/bin/env -S nix-instantiate --evalrec {
# (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; };
}
Here's how we would represent Church encoded booleans with
such constructors:
T = L.mkLambda "x" (L.mkLambda "y" (L.mkVar "x"));
F = L.mkLambda "x" (L.mkLambda "y" (L.mkVar "y"));
and = L.mkLambda "x" (L.mkLambda "y" (L.mkApply (L.mkApply (L.mkVar "x") (L.mkVar "y")) F));
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?
Lists were defined as either being empty, or as a head attached to a tail.
The head was an element of the list, and the tail was a portion of the
list (ie. another list).
The good thing about such definition is that by managing two cases (empty
or head/tail), we were able to write recursive functions handling
arbitrarily complex lists. But we can apply the same line of thinking
here: a λ-term being either:
a variable (un-decomposable);
an abstraction (a variable name and a λ-term);
or an application (made out of two λ-terms).
We can then write recursive code on arbitrarily complex
λ-terms simply by following the recursive definitions.
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.
The grammar/format we have is correct, but as you can see, this
is a bit verbose. We'll switch to a more compact representation
when developing the parser: we'll be forced to adjust the grammar.
For now, we're just trying to get familiar with the language,
refinements are secondary.
#!/usr/bin/env -S nix-instantiate --evalwith builtins;
let ftests = (import../ftests.nix);
L = (import./toString.nix) // (import./mks.nix);
T = L.mkLambda "x" (L.mkLambda "y" (L.mkVar "x"));
F = L.mkLambda "x" (L.mkLambda "y" (L.mkVar "y"));
and = L.mkLambda "x" (L.mkLambda "y" (L.mkApply (L.mkApply (L.mkVar "x") (L.mkVar "y")) F));
tests = [
{
descr =''toString T'';
fun = L.toString;
args = T;
expected ="(λx. (λy. x))";
}
{
descr =''toString F'';
fun = L.toString;
args = F;
expected ="(λx. (λy. y))";
}
{
descr =''toString and'';
fun = L.toString;
args = and;
expected ="(λx. (λy. ((x y) (λx. (λy. y)))))";
}
];
in ftests.run tests
trace: OK :toString T
trace: OK :toString F
trace: OK :toString and
true
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?
I'll let you refer to Selinger's notes (or any others) for the
theoretical details.
Regarding the tests: we can write λ-terms by hands, via
our "constructors", but this is tedious: we can be lazy and wait
until we have a way to parse λ-terms from strings. Not only testing
freeVars/allVars will be easier, but we'll then get
a few more parsing tests for free.
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?
Imagine we're starting to parse an expression and must decide what
to do next. With such a grammar, you only have the following options
(obviously, assuming we ignore whitespaces):
Either the current character is a \(\{a...z, A...Z\}\), meaning,
we have to read a variable name and return that;
Or, the input starts with "\((\lambda...\)", meaning, we have
to parse a abstraction, and expects a closing parenthesis;
And otherwise, we're parsing an application of the form \((T\,T)\).
And, done. There's no ambiguity, no specific associativity rule to
be cautious about. Skip spaces, read the first two characters (3
bytes as "λ" is a 2-byte long UTF-8 character), wrap
in a data structure and recurse.
You can try to implement things this way if you want, especially
if you're not too confident about your parsing skills; I'll skip it
and directly work on a refined grammar.
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).
First, we definitely won't be able to parse things by ignoring spaces and
looking three bytes ahead at most to determine how to parse
what's coming.
Second, observe how we're essentially going to use parentheses as we
did in the mathematical expression parsers: they are optional, and will
only serve to alter the default associativity rules. As a result, we're
going to treat them as we did before, in the deepest recursive function
of the "parsing chain".
Third, we'll have to be careful when parsing things like \(M\,N\,P\),
and this will be our next topic.
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?
The problem with the previous example is that, after having recursed
to the right, you'd be receiving an application a b.
Then, you'd be trying to glue things with y, because
you know the y is being applied to whatever's on its right.
But then, how would you know that you're trying to parse y (a b)
and not y a b?
Here's how the code would look like:
insertLeft = t: v: mkApply (
if t.left.type !="apply"then mkApply v t.left
else insertLeft t.left v
) t.right;
parseApply = s: let t = parseSomething s; inif hasErr t then t
elseif hasWord t thenlet u = parseApply t; in# Here, we want to transform (M N P) in ((M N) P),# but not (M (N P)) in ((M N) P).# However, right now, we have M on one side (t.expr)# and N P (u.expr) on the other, and we don't know# how they were intended to be glued together anymore!if u.expr.type =="apply"then u // { expr = insertLeft u.expr t.expr; }
else u // { expr = mkApply t.expr u.expr; }
else t;
The fix is not to recurse one parseApply,
but to try to parse a list of "something", meaning try to
call parseSomething for as long as you can, and build
your left-associative applications along the way.
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.
There's a lot more tests in the final test file
lambda_test.nix.
You may also find there additional tests for pretty/allVars/freeVars.
#!/usr/bin/env -S nix-instantiate --evalwith builtins;
with (import../string/strings.nix);
with (import../string/ascii.nix);
with (import./mks.nix);
rec {
# 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;
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"; }
elseif (peek1 s) =="("thenlet t = parseExpr (next1 s);
inif hasErr t then t
elseif (peek1 t) !=")"then t // { err ="expecting ')'"; }
else next1 t
elselet w = peekw s; inif 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;
inlet w = peekw t;
u = nextw t;
inif peek1 u =="."thenlet v = parseExpr (next1 u); inif hasErr v then v
else v // { expr = mkLambda w v.expr; }
elseif 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; inif hasErr t then t
elselet a =if acc == {} then t.expr else mkApply acc t.expr;
inif 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; });
}
#!/usr/bin/env -S nix-instantiate --evalwith builtins;
let ftests = (import../ftests.nix);
L = (import./parse.nix) // (import./mks.nix) // (import./toString.nix);
T = L.mkLambda "x" (L.mkLambda "y" (L.mkVar "x"));
tests = [ {
descr =''parse ""'';
fun = L.parse;
args ="";
expected = L.start // { err ="unexpected EOF"; };
}
{
descr =''parse "123"'';
fun = L.parse;
args ="123";
expected = L.start // {
s ="123";
p =3;
expr = { type ="var"; name ="123"; };
};
}
{
descr =''parse "(123)"'';
fun = L.parse;
args ="(123)";
expected = L.start // {
s ="(123)";
p =5;
expr = { type ="var"; name ="123"; };
};
}
{
descr =''parse "((123))"'';
fun = L.parse;
args ="((123))";
expected = L.start // {
s ="((123))";
p =7;
expr = { type ="var"; name ="123"; };
};
}
{
descr =''parse " ( ( 123) )"'';
fun = L.parse;
args =" ( ( 123) )";
expected = L.start // {
s =" ( ( 123) )";
p =15;
expr = { type ="var"; name ="123"; };
};
}
{
descr =''parse "(λx(λy. x))"'';
fun = L.parse;
args ="(λx(λy. x))";
expected = L.start // {
err =". expected after λ";
s ="(λx(λy. x))";
p =4;
expr = {};
};
}
{
descr =''parse "x ("'';
fun = L.parse;
args ="x (";
expected = L.start // {
err ="unexpected EOF";
s ="x (";
p =3;
# parseApply "lose" the right hand side on error;# this is good enough. expr = { };
};
}
{
descr =''parse "x (yy"'';
fun = L.parse;
args ="x (yy";
expected = L.start // {
err ="expecting ')'";
s ="x (yy";
p =5;
expr = { type ="var"; name ="yy"; };
};
}
{
descr =''parse "(λx. )"'';
fun = L.parse;
args ="(λx. )";
expected = L.start // {
err ="word expected";
s ="(λx. )";
p =5;
expr = {};
};
}
{
descr =''parse "( λx. ( λy. x ))"'';
fun = L.parse;
args ="( λx. ( λy. x ))";
expected = L.start // {
s ="( λx. ( λy. x ))";
p =20; # 18 runes, 20 bytes expr = T;
};
}
{
descr =''parse "( λx. λy. x) "'';
fun = L.parse;
args ="( λx. λy. x) ";
expected = L.start // {
s ="( λx. λy. x) ";
p =16; # 14 runes expr = T;
};
}
{
descr =''parse "λx.λy.x"'';
fun = L.parse;
args ="λx.λy.x";
expected = L.start // {
s ="λx.λy.x";
p =9; # 7 runes expr = T;
};
}
{
descr =''parse "x. one two three four five"'';
fun = L.parse;
args ="x. one two three four five";
expected = L.start // {
s ="x. one two three four five";
p =26;
expr = {
type ="lambda";
bound ="x";
expr = {
type ="apply";
left = {
type ="apply";
left = {
type ="apply";
left = {
type ="apply";
left = { type ="var"; name ="one"; };
right = { type ="var"; name ="two"; };
};
right = { type ="var"; name ="three"; };
};
right = { type ="var"; name ="four"; };
};
right = { type ="var"; name ="five"; };
};
};
};
}
{
descr =''parse "((x y) (λx. λy. y))"'';
fun = L.parse;
args ="((x y) (λx. λy. y))";
expected = L.start // {
s ="((x y) (λx. λy. y))";
p =21;
expr = {
type ="apply";
left = {
type ="apply";
left = { type ="var"; name ="x"; };
right = { type ="var"; name ="y"; };
};
right = {
type ="lambda";
bound ="x";
expr = {
type ="lambda";
bound ="y";
expr = {
type ="var"; name ="y";
};
};
};
};
};
}
];
in ftests.run tests
trace: OK :parse ""trace: OK :parse "123"trace: OK :parse "(123)"trace: OK :parse "((123))"trace: OK :parse " ( ( 123) )"trace: OK :parse "(λx(λy. x))"trace: OK :parse "x ("trace: OK :parse "x (yy"trace: OK :parse "(λx. )"trace: OK :parse "( λx. ( λy. x ))"trace: OK :parse "( λx. λy. x) "trace: OK :parse "λx.λy.x"trace: OK :parse "x. one two three four five"trace: OK :parse "((x y) (λx. λy. y))"true
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\):
Renaming is a precise operation, with a carefully designed definition.
You'll want to find it before implementing it, either own your own, but
at least check your ideas with a paper.
Again, for the details, have a look at
Selinger's
notes (section 2.2),
and for more tests, see the final test file
lambda_test.nix.
#!/usr/bin/env -S nix-instantiate --evalrec {
# α-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;
} elseif 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;
};
}
#!/usr/bin/env -S nix-instantiate --evalwith builtins;
let ftests = (import../ftests.nix);
L = (import./parse.nix) // (import./rename.nix);
G = s: (L.parse s).expr;
tests = [
{
descr =''rename "z" y x'';
fun = L.rename;
args = [(G "z") "y""x"];
expected = (G "z");
}
{
descr =''rename "x" y x'';
fun = L.rename;
args = [(G "x") "y""x"];
expected = (G "y");
}
{
descr =''rename "(x y) (y z) " y x'';
fun = L.rename;
args = [(G "(x y) (y x z) ") "y""x"];
expected = (G "(y y) (y y z) ");
}
{
descr =''rename "λx. x z" y x'';
fun = L.rename;
args = [(G "λx. x z") "y""x"];
expected = (G "λy. y z");
}
{
descr =''rename "λx. x z" y y'';
fun = L.rename;
args = [(G "λx. x z") "y""y"];
expected = (G "λx. x z");
}
{
descr =''rename "λx. λy. y z foo bar" z x'';
fun = L.rename;
args = [(G "λx. λy. y z foo bar") "z""x"];
expected = (G "λz. λy. y z foo bar");
}
{
descr =''rename "λx. λy. y z foo bar" z x'';
fun = L.rename;
args = [(G "λx. λy. y z foo bar") "z""x"];
expected = (G "λz. λy. y z foo bar");
}
{
descr =''rename "λx. λy. y z foo bar" z x'';
fun = L.rename;
args = [(G "λx. λy. y z foo bar") "foo""y"];
expected = (G "λx. λfoo. foo z foo bar");
}
];
in ftests.run tests
trace: OK :rename "z" y x
trace: OK :rename "x" y x
trace: OK :rename "(x y) (y z) " y x
trace: OK :rename "λx. x z" y x
trace: OK :rename "λx. x z" y y
trace: OK :rename "λx. λy. y z foo bar" z x
trace: OK :rename "λx. λy. y z foo bar" z x
trace: OK :rename "λx. λy. y z foo bar" z x
true
Exercise: (β-substitution) Write a function substitute m n x,
which substitute the termx by the termy in the λ-term t,
for instance, noting \(M_{[N/x]}\) to replace \(x\) by \(N\) in \(M\):
As always, for the theoretical details, see
Selinger,
section 2.3.
#!/usr/bin/env -S nix-instantiate --evalwith builtins;
with (import./freeVars-allVars.nix);
with (import./rename.nix);
rec {
# 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);
# β-substitution, M[N/x] (substituing x for N in M) substitute = m: n: x:
if m.type =="var"thenif m.name == x then n else m
elseif m.type =="apply"then m // {
left = substitute m.left n x;
right = substitute m.right n x;
} elseif m.bound == x then m
elseif! (isFree n m.bound) then m // {
expr = substitute m.expr n x;
} elselet 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;
};
}
#!/usr/bin/env -S nix-instantiate --evalwith builtins;
let ftests = (import../ftests.nix);
L = (import./parse.nix) // (import./substitute.nix);
G = s: (L.parse s).expr;
tests = [
{
descr =''substitute: matching variable is substituted'';
fun = L.substitute;
args = [(G "x") (G "λx. λy. x y") "x"];
expected = (G "λx. λy. x y");
}
{
descr =''substitute: un-matching variable name'';
fun = L.substitute;
args = [(G "y") (G "λx. λy. x y") "x"];
expected = (G "y");
}
{
descr =''substitute: variable substituted in both parts of an apply'';
fun = L.substitute;
args = [(G "(x (x y))") (G "λx. λy. x y") "x"];
expected = (G "((λx. λy. x y) ((λx. λy. x y) y))");
}
{
descr =''substitute: bound variable not substituted'';
fun = L.substitute;
args = [(G "λx. λy. x y") (G "λx. λy. x y") "x"];
expected = (G "λx. λy. x y");
}
{
descr =''substitute: unbound, unused variable'';
fun = L.substitute;
args = [(G "λx. λz. x z") (G "λx. λy. x y") "z"];
expected = (G "λx. λz. x z");
}
{
descr =''substitute: replacing a free variable, no conflict'';
fun = L.substitute;
args = [(G "λx. λy. x z") (G "λx. λy. x y") "z"];
expected = (G "λx. λy. x (λx. λy. x y)");
}
{
descr =''substitute: replacing a free variable, renaming'';
fun = L.substitute;
args = [(G "λx. λy. x z y") (G "λx. λz. x y z") "z"];
expected = (G "λx. λx0. x (λx. λz. x y z) x0");
}
{
descr =''substitute: replacing a free variable, renaming (bis)'';
fun = L.substitute;
args = [(G "λx. λy. x (z x0) y") (G "λx. λz. x y z") "z"];
expected = (G "λx. λx1. x ((λx. λz. x y z) x0) x1");
}
{
descr =''substitute: Selinger's example'';
fun = L.substitute;
args = [(G "λx. y x") (G "λz. x z") "y"];
expected = (G "λx0. (λz. x z) x0");
}
# TODO: choose a better example. {
descr =''substitute: replacing bound variable by the variable to rename'';
fun = L.substitute;
args = [(G ''
(λf. n.
((λy.
(
(λn. x. y. (n (λz. y) x))
n
(λf. x. (f x)) y))
(λx0.
(n (f (λf. x. (n (λg. h. (h (g f))) (λu. x) (λu. u))) x0)))))
'') (G "f") "x0"];
expected = (G ''
(λx1. n.
((λy.
(
(λn. x. y. (n (λz. y) x))
n
(λx1. x. (x1 x)) y))
(λx0.
(n (x1 (λx1. x. (n (λg. h. (h (g x1))) (λu. x) (λu. u))) x0)))))
'');
}
{
descr =''substitute: don't re-use a name already used below'';
fun = L.substitute;
args = [
(G "(λn. x0. y. (n (λz. y) x0))")
(G "(λx0. (n (x1 (λx1. x0. (n (λg. h. (h (g x1))) (λu. x0) (λu. u))) x0)))")
"y" ];
expected = (G "(λx2. x0. y. (x2 (λz. y) x0))");
}
{
descr =''substitute: "complex" substitute'';
fun = L.substitute;
args = [(G ''
(λy.
(λp. λx. λy. p x y)
x
(λx. λy. x)
(
(λp. λx. λy. p x y)
y
(λx. λy. x)
(λx. λy. y)))'') (G "(λx. λy. x)") "x"];
expected = (G ''
(λy.
(λp. λx. λy. p x y)
(λx. λy. x)
(λx. λy. x)
(
(λp. λx. λy. p x y)
y
(λx. λy. x)
(λx. λy. y)))'');
}
];
in ftests.run tests
trace: OK :substitute: matching variable is substituted
trace: OK :substitute: un-matching variable name
trace: OK :substitute: variable substituted in both parts of an apply
trace: OK :substitute: bound variable not substituted
trace: OK :substitute: unbound, unused variable
trace: OK :substitute: replacing a free variable, no conflict
trace: OK :substitute: replacing a free variable, renaming
trace: OK :substitute: replacing a free variable, renaming (bis)trace: OK :substitute: Selinger's example
trace: OK :substitute: replacing bound variable by the variable to rename
trace: OK :substitute: don't re-use a name already used below
trace: OK :substitute: "complex" substitute
true
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.
For the theoretical details, see
Selinger,
section 2.5. Refer to the final test file
lambda_test.nix for more tests.
#!/usr/bin/env -S nix-instantiate --evalwith builtins;
with (import./substitute.nix);
rec {
reduce = m: /* trace(pretty m) */ (
if m.type =="lambda"then m // { expr = reduce m.expr; }
elseif m.type =="var"then m
elseif 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; inif n == m then n else eval n;
}
#!/usr/bin/env -S nix-instantiate --evalwith builtins;
let ftests = (import../ftests.nix);
L = (import./parse.nix) // (import./eval.nix) // (import./mks.nix) // (import./pretty.nix);
G = s: (L.parse s).expr;
P = m: L.pretty m;
S = P;
T = L.mkLambda "x" (L.mkLambda "y" (L.mkVar "x"));
F = L.mkLambda "x" (L.mkLambda "y" (L.mkVar "y"));
and = L.mkLambda "x" (L.mkLambda "y" (L.mkApply (L.mkApply (L.mkVar "x") (L.mkVar "y")) F));
ifelse = (G "(λp. λx. λy. p x y)");
xor = (G ''
(λx. λy.
(${S ifelse} x
(${S ifelse} y ${S F}${S T})
(${S ifelse} y ${S T}${S F})))
'');
zero = (G "(λf. λx. x)");
one = (G "(λf. λx. f x)");
two = (G "(λf. λx. f (f x))");
three = (G "(λf. λx. f (f (f x)))");
four = (G "(λf. λx. f (f (f (f x))))");
succ = (G "(λn. λf. λx. f (n f x))");
add = (G "(λn. λm. λf. λx. n f (m f x))");
mult = (G "(λn. λm. λf. n (m f))");
iszero = (G "(λn. λx. λy. n (λz.y) x)");
pred = (G "λn.λf.λx. n (λg.λh. h (g f)) (λu.x) (λu.u)");
# pred = (G "n.f.x. n (g.h. h (g f)) (u.x) (u.u)");/*
* Turing fixed point, recursion
*/ A = (G "(λx. λy. y (x x y))");
TFP = (G "((${S A}) (${S A}))");
Ffact = (G ''
λf.λn.
(${S ifelse}) (${S iszero} n)
(${S one})
(${S mult} n (f (${S pred} n)))
'');
fact = (G "(${S TFP}) (${S Ffact})");
tests = [
{
descr =''eval: variable'';
fun = L.eval;
args = (G "x");
expected = (G "x");
}
{
descr =''eval: unreductible apply'';
fun = L.eval;
args = (G "x y");
expected = (G "x y");
}
{
descr =''eval: unreductible applies'';
fun = L.eval;
args = (G "x y z");
expected = (G "x y z");
}
{
descr =''eval: function call, single arg'';
fun = L.eval;
args = (G "(λx. x y) z");
expected = (G "z y");
}
{
descr =''eval: let ... in ... -like (or T T)'';
fun = L.eval;
args = (G ''
(
(λ ifelse.
(λ F.
(λ T.
(λ or.
(
(or T) T
)
) (λx. (λy. (((ifelse x) T) (((ifelse y) T) F))))
) (λx. (λy. x))
) (λx. (λy. y))
) (λp. (λx. (λy. ((p x) y))))
)
'');
expected = T;
}
{
descr =''eval: xor T T == F (3)'';
fun = L.eval;
args = (G "((${S xor}${S T}) ${S T})");
expected = F;
}
{
descr =''eval: iszero three == F'';
fun = L.eval;
args = (G "${S iszero}${S three}");
expected = F;
}
{
descr =''eval: pred (pred three) == one'';
fun = L.eval;
args = (G "${S pred} (${S pred}${S three})");
expected = one;
}
{
descr =''eval: fact three == three * two * one = six'';
fun = L.eval;
args = (G "${S fact}${S three}");
expected = L.eval (G "${S mult}${S three}${S two}");
}
];
in ftests.run tests
trace: OK :eval: variable
trace: OK :eval: unreductible apply
trace: OK :eval: unreductible applies
trace: OK :eval: function call, single arg
trace: OK :eval: let ... in ... -like (or T T)trace: OK :eval: xor T T == F (3)trace: OK :eval: iszero three == F
trace: OK :eval: pred (pred three)== one
trace: OK :eval: fact three == three * two * one = six
true
#!/usr/bin/env -S nix-instantiate --evalwith 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
elseif 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
elseif m.type =="lambda"thenif inLambda then m.bound+"."+" "+(aux m.expr truefalse)
else"(λ"+m.bound+"."+" "+(aux m.expr truefalse)+")"elseif inApp then (aux m.left falsetrue)+" "+(aux m.right falsefalse)
else"("+(aux m.left falsetrue)+" "+(aux m.right falsefalse)+")" ; in aux m falsefalse;
freeVars = m:
if m.type =="var"then { ${m.name}=true; }
elseif 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; }
elseif 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"; }
elseif (peek1 s) =="("thenlet t = parseExpr (next1 s);
inif hasErr t then t
elseif (peek1 t) !=")"then t // { err ="expecting ')'"; }
else next1 t
elselet w = peekw s; inif 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;
inlet w = peekw t;
u = nextw t;
inif peek1 u =="."thenlet v = parseExpr (next1 u); inif hasErr v then v
else v // { expr = mkLambda w v.expr; }
elseif 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; inif hasErr t then t
elselet a =if acc == {} then t.expr else mkApply acc t.expr;
inif 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;
} elseif 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"thenif m.name == x then n else m
elseif m.type =="apply"then m // {
left = substitute m.left n x;
right = substitute m.right n x;
} elseif m.bound == x then m
elseif! (isFree n m.bound) then m // {
expr = substitute m.expr n x;
} elselet 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; }
elseif m.type =="var"then m
elseif 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; inif 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.
I think a good first step would be to add let ... in ...:
we've already saw that this can be considered syntactic sugar over basic
λ-calculus. Another "easy" step would be to bake the mathematical
expression parsers from the
previous article into the λ-calculus parser, and continue on to
evaluate mathematical expressions. This would brings us close to
PCF.
From there I think one can start working on lists and sets.
There are some other, more or less developed Nix interpreters
written in other languages: a bunch of them are listed
here. The
most advanced seems to be
HNix, written
in Haskell. All of them, including the original C++ interpreter
could be worth studying.
Comments
By email, at mathieu.bivert chez: