Nearly a century ago, Alonzo Church invented the simple, elegant, and yet elusive lambda calculus. Along with Alan Turing, he then proved the ChurchTuring thesis: that anything computable with a Turing machine can also be computed in the lambda calculus. However, nearly as soon as we had digital computers, we started inventing programming languages, and with them a vast treasure of features, beautiful and terrible, many of which seem very hard to relate to the fundamental nature of computability, let alone the lambda calculus specifically.
While it’s true that anything which can be computed, period, can be computed in the lambda calculus, you might not want to: it’s austere, to say the least, and was not designed with modern sensibilities regarding readability in mind. We developed all those languages and features for a reason! Still, Church demonstrated not just that it was possible to compute anything computable with the lambda calculus, but also how one might do so.
In this series, we’ll examine some ways to express common programming language features using the minimalistic tools of the lambda calculus. We begin with perhaps the most ubiquitous type: booleans.
λ is blind
The lambda calculus’s austerity is extreme: you don’t even have booleans. All you have are:
Lambda abstractions;
Applications; and
Variables.
We’ll now review these in some detail; feel free to skip this section if you’re already familiar with the lambda calculus.
Lambda abstractions
Lambda abstractions (“lambdas,” “abstractions,” and “functions” will also be used interchangeably) introduce a function of a single variable.
Abstractions are written λ x . y
, for variable x
and expression y
, where x
is now available as a bound variable in the body, and any enclosing definition of x
is shadowed (i.e. λ x . λ x . x
= λ x . λ y . y
≠ λ x . λ y . x
). (We shall assume strictly lexical scoping for the time being.)
In Haskell, we would write \ x > y
instead; in JavaScript, function (x) { return y }
or (x) => y
.
Applications
Applications (“function application” and “function call” will be used interchangeably) apply the result of the expression on the left to the expression on the right.
Applications are written as x y
, for expressions x and y, and leftassociated, i.e. a b c
= (a b) c
≠ a (b c)
. Function application binds tighter than lambda abstraction, i.e. λ x . λ y . y x
= λ x . λ y . (y x)
≠ λ x . (λ y . y) x
.
The syntax is the same in Haskell; in JavaScript, we would write x(y)
or a(b, c)
. Note however that since lambda calculus functions are all singleargument functions, a more direct (though less idiomatic) equivalent for the latter would be a(b)(c)
.
Variables
Variables introduced by enclosing lambdas.
Variable are written as more or less arbitrary names, typically alphanumeric (e.g. x
or y0
or thing
); however, we will feel free to include nonalphanumeric characters in names as we see fit, since the paucity of syntax means there’s little risk of ambiguity.
Since the only available variables are those bound by enclosing lambdas, we can also infer that there are no let
bindings for local variables, and no globals of any sort; the lambda calculus doesn’t come with a standard library.
Summary
In quasiBNF, the grammar for the lambda calculus is extremely minimal:
And finally, this table gives a sidebyside comparison of the syntax of the lambda calculus with the corresponding syntax in Haskell & JavaScript:
Lambda calculus  Haskell  JavaScript  

Abstraction 
λ x . y

\ x > y

(x) => y

Application 
f x

f x

f(x)

Variable 
x

x

x

Unconditional λ
Lambdas are the only way to introduce values—they’re the only “literal” syntax in the language. We can therefore infer that the only kinds of runtime values must be closures. In an interpreter for the lambda calculus, closures might consist of the name of the introduced variable, the body of the lambda, & a map relating the names and values of any variables it closed over when constructed (again, we assume strict lexical scoping). There are no bits, bytes, words, pointers, or objects in the language’s semantics; only this runtime representation of lambdas.
Likewise, lambdas are also the only way to introduce variables—there’s no standard library, builtins, primitives, prelude, or global environment to provide common definitions. We’re truly baking the apple pie from scratch.
All of this raises the question: how do you do anything when you don’t even have true
and false
? Lambdas and variables don’t do, they merely are, so that leaves application. When all you have is application, everything looks like a lambda abstraction, so we’ll represent booleans using lambdas.
Of course, it’s not just booleans we’re after; true
and false
aren’t much use without and
, or
, not
, if
, and all the rest. To be useful, our representation of booleans should therefore suffice to define these, as well. But how do you define if
without using if
? In a lazy language like Haskell, we might define if
as a function something like so:
if_ :: Bool > a > a > a
= if cond then then_ else else_ if_ cond then_ else_
In a strict language like JavaScript, we’d instead take functions for the alternatives:
function if_(cond, then_, else_) {
if (cond) {
then_();
else {
} else_();
} }
Both these definitions use the language’s native booleans and if
syntax (a tactic for implementing embedded DSLs known as “metacircularity”), and thus aren’t viable in the lambda calculus. However, they do give us a hint: in both cases we have a function taking a condition, consequence, and alternative, and using the first to select one of the latter two. In the lambda calculus, we might start by writing:
if = λ cond then else . ?
(Note: there aren’t any keywords in the lambda calculus, so there’s nothing stopping me from naming variables things like if
, a fact which I will take free advantage of.)
We’ve introduced a definition for if
, as a function of three parameters; now what do we do with them? The lambda calculus’s stark palette makes it easy to enumerate all the things we can do with some variable a
:
Ignore it, whether by simply not mentioning it at all (as in
λ a . λ b . b
), or by shadowing it with another lambda which binds the same name (as inλ a . λ a . a
).Mention it, whether on its own in the body of a lambda (as in
λ a . a
orλ a . λ b . a
), somewhere within either side of an application (as inλ a . λ b . a b
orλ a . λ b . b a
), or some combination of both (as inλ a . (λ b . a) a
).
We could for example simply return then
or else
:
if = λ cond then else . then
if = λ cond then else . else
But in that case the conditional isn’t conditional at all—the value in no way depends on cond
. Clearly the body must make use of all three variables if we want it to behave like the if
s we know and love from other languages.
Taking a step back for a moment, let’s examine the roles of if
’s arguments. then
and else
are passive; we only want to use or evaluate one or the other depending on the value of cond
. cond
, then, is the key: it takes the active role.
Thus, in the same way that our if_
functions in Haskell & JavaScript employed those language’s features to implement, we’re going to define if cond then else
as the application of the condition to the other two parameters:
if = λ cond then else . cond then else
This feels strangely like cheating: surely we’ve only moved the problem around. Now instead of if
making the decision about which argument to return, we’ve deferred it to cond
. But if
and cond
aren’t the same, semantically; if
takes a boolean and two other arguments and returns one of the latter, while cond
is a boolean—albeit evidently a boolean represented as a function. Let’s make that precise by writing down if
’s type:
if : Bool > a > a > a
Notwithstanding our use of the yettobedefined name Bool
for the type of the condition, this is the same type as we gave if_
in Haskell; that’s a good sign that we’re on the right track! It takes a Bool
and two arguments of type a
, and it must return one of those because that’s the only way for it to come up with the a
that it returns. But what is Bool
?
Working backwards from the type and definition of if
, we see that cond
is applied to two arguments, and therefore must be a function of two parameters. Further, these are both of type a
, and the value it returns must also be of type a
for if
’s type to hold. Thus, we can define the type Bool
like so:
Bool = ∀ a . a > a > a
If a given Bool
is a function of two arguments of arbitrary type, returning the same type, it must therefore select one of its arguments to return. There are only two distinguishable inhabitants of Bool
, true
and false
, so we can therefore deduce that since if
defers the selection of the result to the Bool
, for true
and false
to actually differ they must make opposite selections. In other words, true
must return the then
parameter, while false
must return the else
one:
true, false : Bool
true = λ then else . then
false = λ then else . else
We didn’t move the problem around after all; we solved it. What we noticed was a deeper insight: this encoding of booleans makes if
redundant, since if we can apply if
to a Bool
and two arguments, we could equally apply the Bool
to those arguments directly.
It’s frequently convenient to conflate booleans with bits, their minimal representation, but in truth they’re not the same at all. Practically, some programming languages define booleans as a byte in memory, perhaps clamping its values to 0 and 1; others define them as instances of some boolean class, or constructors of an algebraic datatype. Some provide no formal relationship between true
and false
at all, save for a common interface—duck typing.
Mathematically, booleans are the values in propositional logic; the upper and lower bounds of a lattice; the zero and one of a semiring; the members of the set with cardinality 2; and many other things in many different contexts.
Operationally, booleans represent choice, and this is a pattern that we’ll see repeated: encoding a datatype with lambdas means representing the datatype as functions supporting all of its operations. All operations on booleans can be defined by selecting between two alternatives, which is precisely what our encoding does.
We can demonstrate this by defining some other operations on booleans, e.g. logical operators, using the encoding we’ve built thus far.
not
takes a single Bool
and returns another:
not : Bool > Bool
not = λ x . ?
As when defining if
, all we can do with a Bool
is branch on it:
not = λ x . if x ? ?
But which arguments should we pass if we wish to return a Bool
with the opposite value? Recall the definition of Bool
from above:
Bool = ∀ a . a > a > a
To return a Bool
, therefore, each argument must likewise be a Bool
. The first argument will be selected if x
is true
, the second if x
is false
, so if we want the opposite value from x
we can simply apply it to the opposite values in either position:
not = λ x . if x false true
not x
will therefore return false
if x
is true
, and true
if x
is false
; equationally:
not true = false
not false = true
Which is precisely the meaning we intended not
to have.
or
and and
are closely related to one another, so we’ll define them simultaneously. Both take two Bool
s and return a Bool
:
or, and : Bool > Bool > Bool
or = λ x y . ?
and = λ x y . ?
As with not
, all we can do with Bool
s is branch:
or = λ x y . if x ? ?
and = λ x y . if x ? ?
For or
, if x
is true
, we can return true
immediately (“shortcircuiting”). For and
, it’s the opposite:
or = λ x y . if x true ?
and = λ x y . if x ? false
If x
is false
, or
needs to test whether y
is true
; likewise, if x
is true
, and
needs to test whether y
is also true
. Once more, all we can do with Bool
s is branch:
or = λ x y . if x true (if y ? ?)
and = λ x y . if x (if y ? ?) false
And since we must return a Bool
, we can use true
and false
:
or = λ x y . if x true (if y true false)
and = λ x y . if x (if y true false) false
Pleasantly, if y true false
(and likewise y true false
) is operationally equivalent to y
. Using that equivalence, we can simplify these definitions, leaving us with:
or = λ x y . if x true y
and = λ x y . if x y false
Conclusion
In this post, we’ve explored defining a ubiquitous programming language feature—booleans—using nothing more than the spartan trappings of the lambda calculus. We’ve emerged with a language which can express not merely functions and their applications, but also fundamental metaphysical concepts such as truth.
In the next post, we’ll look at lambdaencodings of beauty: ML/Haskellstyle algebraic datatypes.