Lambda Calculus is a universal model of computation proposed by Alonzo Church in the 1930's, and it is an incredibly small one at that. It consists of simple expressions constructed out of 3 things:

• variables
• lambda abstractions
• function applications

What are these? In friendly terms, a variable is just something that we don't know yet, and so we've given it a name instead. A lambda abstraction tells us how to replace a variable with it's value when we learn it. And a function application is the act of learning what a lambda abstraction's variable is.

How do we use this, say, to add two plus five? Well, it's easy! add five two, where add is a function taking two arguments.

Whereas Turing machines invoke clunky mechanisms, Church's calculus is a language, with a flexibility and flow not unlike that of the spoken language, and how each spoken word produces a sentence fragment that is awaiting the next word of the rest of the sentence.

This article isn't going to explain lambda calculus in depth, as it rather serves as a nice starting point for such explorations later. If you've been doing Haskell, you've been doing lambda calculus the whole time, anyway.

With that out of the way, let's get started! First off, we'll create a new cabal project file. You may prefer to use stack if you like. We're going to pull in a few libraries - containers for the usual suspects, parsec for parsing, and repline for interactive input - and set some extensions (nothing fancy, just FlexibleContexts, NoImplicitPrelude, and OverloadedStrings)

Let us define our expression data type. As you can see, an expression is made up of variables, lambda abstractions, and function applications.

The most important part is this part:

data Expr
    = Var Name
    | Lam Name Expr
    | App Expr Expr
                    

Our definition here is a lot less threatening than our earlier descriptions, don't you think? As you can see, an Expr is either a Var which is just a Name, a Lam which is a Name and another Expr, or a App which is two Exprs.

In addition to our data type, we've added a few convenience functions for encoding our expressions to strings, and for pretty printing them - it helps to be able to do something with what we're building.

So how do we go about actually using this data type? We could construct it manually, of course - we could define the identity function id = Lam "x" (Var "x"). But that is rather tedious. It is better to build a parser!

Having a parser serves a few purposes: first, it lets us use a better format for our lambda calculus code (\ x y . x is easier to read and write than Lam "x" (Lam "y" (Var "x"))) and secondly, it lets us write lambda calculus outside of Haskell, which comes in handy when we're building our interpreter later.

We will use the parsec library that we pulled in earlier. parsec is a parser-combinator library, which lets you use smaller parsers to build up a larger parser, and can result in parsers with similar shapes to the data type they are parsing. Since our Expr type is so small, it isn't hard to knock together a parser.

First, we build a parser for parsing Names, which is just captures an alphanumeric string. Then, a Var parser just wraps a constructor around a Name. Lam is a tad more complex, as it looks for one or more Names between a \ and a . followed by an Expr.

The parser for App is the harder bit to unravel. Naively, we could just say that an App is an Expr followed by a space and another Expr, and then use that to build our final parser with something like expr = var | lam | app, which looks rather like our data type. However, if we do it that way, our parser will loop infinitely, because to parse an App, we start by parsing an Expr, which could be an App that needs more parsing... Yikes! Rather than let this happen, we cut the loops, and handle App separately from Var and Lam. We do this by using chainl1 which lets us say that we have a series of Expr with App between them.

As you can see, our expression parser itself fits in just 14 lines - the rest is imports, and a few convenience functions for running our parser. Despite the small size, it parses parenthesis and spaces properly, and even handles multiple lambda arguments (so we can say \ x y z . ... instead of \ x . \ y . \ z . ...). Not bad at all.

With the parser out of the way, we should be able to run parse "\\ x y . x" and get Lam "x" (Lam "y" (Var "x")). (Note the double-slash - because it is a quoted haskell String that uses backslash to escape, we need to use double backslash with the first escaping the second.)

Neat! Now we can build expressions; that means it's time to evaluate them.

So far, we've had to do any evaluation manually, just as we had to do the building of expressions manually before we constructed our parser. We know that the evaluation of (\ x y . x) first second yields first, and that the evaluation of (\ x y . y) first second yields second. We're just going to implement this logic to do this automatically.

To start, we've added a few NameSupply definitions. We use this when we perform alpha conversion, which is what we do if we have a naming collision because we accidentally used the same variable name for two different things.

Then we have a bunch of stuff about FreeVars. A variable is either bound - that is, named in a lambda abstraction - or it is free, meaning it references. A lambda expression can only be evaluated if it contains no free vars, or equivalently, if we can provide the matching variables. So in the expression \ x y . x z, both x and y are bound (even though only x is used), while z is free. We can turn a free variable into a bound one by wrapping the full expression in a lambda abstraction with a matching name. This is where we might have naming collisions, because the free-variable-value's expression might contain variable names that are already in use in the full expression. All this FreeVars stuff helps us detect and ameliorate this.

Once we get to the eval function, it is rather small. It just recurses, beta reducing and calling itself until it stops. So what is beta reduction?

Beta reduction is where, if we have a function application with a lambda abstraction as the first of its two expressions, we can go ahead and give the lambda abstraction the second expression as its argument, substituting the expression for the matching variable in the expression. We use alpha conversion in the case of the earlier mentioned naming conflict. And so we have functions subst alpha and beta.

That's it! Really! We can test it out. A simple test of eval . parse $ "(\ x y . x) first second" should return Var first

If we take the church numerals 2 = \ s z . s (s z) and 3 = \ s z . s (s (s z)), and supply them as arguments to the function add = \ m n s z . m s (n s z), we get (\ m n s z . m s (n s z)) (\ s z . s (s z)) (\ s z . s (s (s z))) which when evaluated repeatedly to normal form yields \ s z . s (s (s (s (s z)))) which when provided one and zero as arguments, results in what is obviously five: one (one (one (one (one zero))))

Note: We'll take care of that normal form stuff in the future revision of this article. For now we'll allow this limitation in the name of a shorter article.

All together, ignoring whitespace, comments, and type hints, the evaluator is just shy of 50 lines of code, with the core of it being the 17 lines for eval subst alpha and beta.

Up to this point, we've been building our expression evaluator while using cabal repl / ghci to handle input and output. This is great for development, but to run our interpreter outside of cabal repl / ghci, we'll have to supply our own repl. Thankfully, this is not that difficult. We're going to first build our own standard READ-EVAL-PRINT-LOOP, just to show how, and then we'll quickly replace it with one using the repline package, which provides a nice shell experience with almost no work.