Curry's Y combinator

We have already built quite a lot on top of λ-terms — data and branching — yet loops are clearly missing. And in their classical form they will not appear at all: instead we get recursion. That is, we need to cook up a term that would spin any function forever. Finiteness we secure through branching, but that comes later.

The Earth's axis stays fixed while the planet itself rotates around it. The equation of the axis is the key characteristic of the rotation, and it is worth being able to derive it. With terms the analogy is the same, only we are after not an axis but a point that is fixed relative to a term. There is a theorem (the fixed-point theorem); I will state it loosely: every λ-term $F$ has a fixed point — a term $X$ for which

Such a point is not hard to build explicitly. Take $X$ $\equiv (\lambda x.\,F\,(x\,x))\,(\lambda x.\,F\,(x\,x))$; its single redex reduces in one β-step:

So $X$ $\to_\beta F\,X$, and in particular $F\,X$ $=_\beta X$.

The term $X$ can be written as $(\lambda f.\,(\lambda x.\,f\,(x\,x))\,(\lambda x.\,f\,(x\,x)))\,F$. We need to tear the fixed point out of the equation and spin the function directly with Curry’s combinator; the combinator is written as:

Substituting $X$ $= \mathrm{Y}\,F$ into the theorem, we get the fixed-point identity — the working form of recursion:

Identity (1.25) is precisely an equality, not a reduction: no chain of direct β-steps takes $\mathrm{Y}\,F$ to $F\,(\mathrm{Y}\,F)$. Indeed, the single redex gives $\mathrm{Y}\,F$ $\to_\beta A$ $\equiv (\lambda x.\,F\,(x\,x))\,(\lambda x.\,F\,(x\,x))$ — this is the familiar $X$ from the proof of the theorem. From there the chain runs through $F\,(A)$, $F\,(F\,(A))$ and so on, and the term $F\,(\mathrm{Y}\,F)$ never appears in it: inside $A$ the combinator $\mathrm{Y}$ no longer occurs. Meanwhile $F\,(\mathrm{Y}\,F)$ itself reduces to $F\,(A)$ in a single step:

The two sides of the identity are equal only because they converge to the common reduct $F\,(A)$; to obtain exactly $F\,(\mathrm{Y}\,F)$ from $\mathrm{Y}\,F$ one would have to step against the arrow (a conversion).

Let us try this on the classic example — the factorial. The recursive step is given by a template with an extra parameter $f$ (the future recursive call):

The fixed point of this template is exactly the factorial. With Curry's combinator the unfolding goes through β-equality:

This scheme is native to lazy languages (call-by-name/call-by-need). In Haskell the fixed-point combinator is built in — $\mathtt{fix}$ from $\mathtt{Data.Function}$ — and it unfolds exactly as in (1.25), on demand:

fix :: (a -> a) -> a
fix f = let x = f x in x   -- the knot is tied by a lazy let: x refers to itself

fac :: Integer -> Integer
fac = fix (\f n -> if n == 0 then 1 else n * f (n - 1))

For all its usefulness in Haskell, Curry's combinator has two problems — and Haskell sidesteps both. The first is the type system: the self-application $x\,x$ does not typecheck in Hindley–Milner, because it sends type inference into a loop. So the fixed point is defined with a recursive $\mathtt{let}$ (as in $\mathtt{fix}$ above) or the self-application is hidden behind a newtype. What this system is and why it works this way is the subject of a separate section further on.

The second is the evaluation order: in a strict (call-by-value) language the definition $\mathtt{let\;x = f\;x}$ would loop forever — to obtain $x$ the runtime immediately evaluates $f\;x$, for which it again needs $x$, and so on without end, never reaching any useful work. Haskell is saved by laziness: $x$ is unfolded only when its value is actually demanded, so the same definition works without looping.