Комбинатор Карри

Мы уже многое построили на базе λ-термов, а именно: данные, ветвление, но вот явно не хватает циклов. Которых в своём классическом понимании и не будет вообще. Заместо этого будет рекурсия. То есть надо придумать такой терм, который бы крутил любую функцию бесконечно. Конечность мы обеспечим за счёт ветвления, но это будет потом.

Ось Земли является неподвижной, в то время как сама планета вращается вокруг этой оси. Уравнение оси — важнейшая характеристика вращения, и его хорошо бы уметь выводить. В случае с термами аналогия такая же, только мы ищем не ось, а точку, которая неподвижна относительно терма. Есть такая теорема (о неподвижной точке), сформулирую произвольно: у любого λ-терма $F$ есть неподвижная точка — терм $X$, для которого

Такую точку нетрудно построить явно. Возьмём $X \equiv (\lambda x.\,F\,(x\,x))\,(\lambda x.\,F\,(x\,x))$; единственный редекс сводится одной β-редукцией:

Итак, $X \to_\beta F\,X$, в частности $F\,X =_\beta X$.

Терм $X$ можно представить как $(\lambda f.\,(\lambda x.\,f\,(x\,x))\,(\lambda x.\,f\,(x\,x)))\,F$. Нам надо вырвать неподвижную точку из уравнения, а функцию крутить непосредственно комбинатором Карри, который обозначается так:

Подставив $X = \mathrm{Y}\,F$ в теорему, получаем тождество неподвижной точки — рабочую форму рекурсии:

Тождество (1.25) — именно равенство, а не редукция: никакая цепочка прямых β-шагов не приведёт $\mathrm{Y}\,F$ к $F\,(\mathrm{Y}\,F)$. В самом деле, единственный редекс даёт $\mathrm{Y}\,F \to_\beta A \equiv (\lambda x.\,F\,(x\,x))\,(\lambda x.\,F\,(x\,x))$ — это знакомый нам $X$ из доказательства теоремы. Дальше цепочка идёт через $F\,(A)$, $F\,(F\,(A))$ и так далее, и терма $F\,(\mathrm{Y}\,F)$ в ней нет: внутри $A$ комбинатор $\mathrm{Y}$ уже не встречается. Зато $F\,(\mathrm{Y}\,F)$ сам за один шаг редуцируется в $F\,(A)$:

Стороны тождества равны лишь потому, что сходятся к общему редукту $F\,(A)$, а чтобы из $\mathrm{Y}\,F$ получить именно $F\,(\mathrm{Y}\,F)$, пришлось бы шагнуть против стрелки (конверсия).

Опробуем это на классическом примере — факториале. Рекурсивный шаг задаём шаблоном с дополнительным параметром $f$ (будущим рекурсивным вызовом):

Неподвижная точка этого шаблона и есть факториал. С комбинатором Карри развёртка идёт через β-равенство:

Эта схема — родная для ленивых языков (call-by-name/call-by-need). В Haskell комбинатор неподвижной точки встроен — $\mathtt{fix}$ из $\mathtt{Data.Function}$, и развёртка идёт ровно как в (1.25), по мере надобности:

fix :: (a -> a) -> a
fix f = let x = f x in x   -- узел завязан ленивым let: x ссылается сам на себя

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

У комбинатора Карри, при всей его применимости в Haskell, есть две проблемы — и Haskell обе обходит. Первая — система типов: самоаппликация $x\,x$ в системе Хиндли — Милнера не типизируется, потому что приводит к зацикливанию вывода типов. Поэтому неподвижную точку задают рекурсивным $\mathtt{let}$ (как в $\mathtt{fix}$ выше) или прячут самоаппликацию за newtype. Что это за система и почему она так устроена — тема отдельного раздела дальше.

Вторая — энергичный порядок вычислений: в строгом (call-by-value) языке определение $\mathtt{let\;x = f\;x}$ крутилось бы вечно — чтобы получить $x$, среда сразу вычисляет $f\;x$, для этого снова $x$, и так без конца, не добираясь до полезной работы. Haskell спасает ленью: $x$ раскрывается лишь тогда, когда его значение действительно понадобится, поэтому та же запись работает без зацикливания.