Lambda Calculus: The Engine Underneath

A calculus with nothing in it but functions

In 1936, Alonzo Church was trying to formalize what it means for something to be “effectively computable” — decades before any electronic computer existed to compute anything. His answer, the lambda calculus, is almost shocking in how little it contains. There are no numbers, no booleans, no lists, no built-in arithmetic. There is exactly one kind of thing — the function — and exactly three rules for building and manipulating them.

That’s it. And it turns out to be exactly as powerful as a Turing machine: anything one can compute, the other can too. Haskell is, in a very real sense, the lambda calculus with pockets sewn in — the same three rules underneath, plus types, syntax, and a standard library layered on top for convenience.

The three pieces

A term in the lambda calculus is built from just three things:

1. Variables — x, y, z, …
2. Abstraction — λx. e, a function that takes an argument called x and returns the expression e
3. Application — e1 e2, applying the function e1 to the argument e2

Translate this directly into Haskell and nothing is lost:

-- λx. x + 1        becomes:
\x -> x + 1

-- λx. λy. x + y    becomes (a function returning a function):
\x -> \y -> x + y

That second example is worth sitting with. λx. λy. x + y is a function of one argument, x, that returns another function, which itself takes y and returns x + y. There is no such thing as a genuinely two-argument function in the lambda calculus — only functions that return functions. Haskell’s \x y -> x + y and multi-argument type signatures like (->) :: a -> b -> c are sugar over exactly this: currying, named after Haskell Curry, is built into the calculus at its foundation, not bolted on as a Haskell-specific feature.

The one computation rule: beta reduction

The lambda calculus has exactly one rule for actually computing anything: beta reduction. When a function meets its argument, you substitute the argument for every free occurrence of the bound variable in the body.

That single substitution rule, applied over and over, is the entire computational engine — not just of the lambda calculus, but underneath every let, every function call, every pattern match Haskell ever performs. When GHC evaluates (\x -> x + 1) 5, it is doing beta reduction, full stop.

Building data out of nothing but functions

Since the calculus has no built-in booleans or numbers, an early and genuinely beautiful discovery was that you don’t need them — you can encode data as functions that behave the right way when applied. This is called Church encoding.

-- Booleans: TRUE picks its first argument, FALSE picks its second
true'  = \t -> \f -> t
false' = \t -> \f -> f

-- "if" is just application: no special syntax needed at all
if' = \b -> \t -> \f -> b t f

if' true' "yes" "no"   -- reduces, by substitution alone, to "yes"

true' and false' aren’t labeled as booleans anywhere — they’re just functions that happen to select one of two arguments. if' doesn’t need to “look inside” a boolean and branch on it; it just applies the boolean to the two branches and lets beta reduction do the choosing. The entire behaviour of if falls straight out of function application, with nothing extra added.

Numbers work the same way. A Church numeral for $n$ is a function that applies whatever it’s given, $n$ times:

zero'  = \f -> \x -> x                    -- apply f, zero times
one'   = \f -> \x -> f x                  -- apply f, once
two'   = \f -> \x -> f (f x)              -- apply f, twice
succ'  = \n -> \f -> \x -> f (n f x)      -- one more application than n

two' (+1) 0 reduces, by nothing but substitution, to (+1) ((+1) 0) = 2 — the numeral genuinely computes its own value, out of raw function application, with no numbers involved in its own definition.

Recursion without a name: the Y combinator

There’s a puzzle hiding in all of this: the lambda calculus has no let rec, no way for a function to refer to itself by name — every term is anonymous. So how do you write something like factorial, which obviously needs to call itself?

The startling answer is a fixed-point combinator — a function that, given any function f, produces f’s fixed point: a value x such that f x = x. The classic one is the Y combinator:

-- Y = λf. (λx. f (x x)) (λx. f (x x))
y' f = (\x -> f (x x)) (\x -> f (x x))

Applying Y to a function f produces a value that, when unfolded by beta reduction, keeps handing f a copy of “the rest of the computation” to call whenever it needs to recurse — self-reference achieved with nothing but application and substitution, no naming required at all.

From untyped to Haskell

The system above — the untyped lambda calculus — is what Church actually wrote down, and it’s powerful enough that y' above typechecks in no sensible type system at all (try giving \x -> x x a type: x would need to be both a and a -> b simultaneously). Haskell is built on the simply-typed lambda calculus instead, which adds exactly the discipline Chapter 3 described: every term gets a type, decided before anything runs, at the cost of ruling out a few things — like the bare Y combinator — that the untyped calculus permitted.

That tradeoff — a little less raw power, in exchange for the guarantee that well-typed programs can’t go wrong in certain ways — is the Curry–Howard correspondence from Chapter 3 in its native habitat: type systems and logic turn out to be the same mathematics, viewed from two directions, and the lambda calculus is the shared root both grew from.