Пары, списки и структуры данных из одних лямбд
Есть один вопрос, который убивает доверие к лямбда-исчислению быстрее всего: «ладно, числа и булевы вы кое-как выкрутили, но данные-то где хранить?» Программист привык, что структура данных — это кусок памяти: массив лежит подряд, у объекта есть поля, у узла списка есть указатель на следующий. А в лямбда-исчислении нет ни памяти, ни полей, ни указателей. Только функции.
Разгадка выглядит как фокус, но после неё уже не развидеть:
Структура данных — это функция, которая знает, что в ней лежит, и отдаёт это тому, кто попросит.
Не коробка, из которой достают. А привратник, который сам вручает. Вы приходите к паре и говорите: «вот функция, примени её к обоим моим полям». Пара применяет — и вы получаете то, что хотели. Хотите первое поле — передайте функцию, которая берёт два аргумента и возвращает первый. Всё.
Если это звучит абстрактно — посмотрите на JavaScript, вы это уже писали:
const point = (f) => f(3, 4); // "пара" (3, 4)
point((x, y) => x); // 3 — взяли первое поле
point((x, y) => y); // 4 — взяли второе
point((x, y) => Math.hypot(x, y)); // 5 — а можно сразу вычислить по обоим
Ни одного массива, ни одного объекта. Данные закодированы в замыкании. Ровно этим мы и займёмся, только строго и до конца — от пары до полноценного списка с head, tail, map и filter.
Пара Чёрча
Формально пара определяется так:
PAIR = λa. λb. λf. f a b
FST = λp. p (λa. λb. a)
SND = λp. p (λa. λb. b)
Читаем вслух. PAIR берёт два значения a и b и возвращает функцию, которая ждёт селектор f и применяет его к a и b. Селектор решает, что вернуть.
Теперь главное наблюдение. Селекторы λa.λb. a и λa.λb. b — это ровно TRUE и FALSE из статьи про булевы значения. Мы не придумываем новые кирпичи, мы переиспользуем старые:
FST = λp. p TRUE
SND = λp. p FALSE
Вот та же мысль картинкой:
Полная раскрутка: FST (PAIR M N)
Никаких «очевидно, получаем». Считаем каждый шаг. Пусть M и N — произвольные термы.
Сначала соберём саму пару. Аппликация левоассоциативна, так что PAIR M N — это (PAIR M) N:
PAIR M N
= ((λa. λb. λf. f a b) M) N
шаг 1 — бета: подставляем M вместо a
→ (λb. λf. f M b) N
шаг 2 — бета: подставляем N вместо b
→ λf. f M N
Промежуточный итог: пара (M, N) — это терм λf. f M N. Она нормальная форма, дальше не редуцируется — сидит и ждёт селектор.
Теперь берём первое поле:
FST (λf. f M N)
= (λp. p TRUE) (λf. f M N)
шаг 3 — бета: подставляем пару вместо p
→ (λf. f M N) TRUE
шаг 4 — бета: подставляем TRUE вместо f
→ TRUE M N
шаг 5 — разворачиваем TRUE
= ((λa. λb. a) M) N
шаг 6 — бета: подставляем M вместо a
→ (λb. M) N
шаг 7 — бета: подставляем N вместо b, но b в теле не встречается
→ M
Семь шагов — и мы получили M. Обратите внимание на шаг 7: N просто выбрасывается. Второе поле никуда не «удаляется из памяти» — оно перестаёт быть достижимым, потому что связанная переменная b не входит в тело. Это и есть весь механизм выбора.
Симметрично SND (PAIR M N) даст N — отличие только в шаге 6, где FALSE = λa.λb. b игнорирует первый аргумент.
То же самое кодом
// Пара Чёрча один в один: аргументы каррированы, как в лямбда-исчислении
const PAIR = a => b => f => f(a)(b);
const TRUE = a => b => a;
const FALSE = a => b => b;
const FST = p => p(TRUE);
const SND = p => p(FALSE);
const p = PAIR("лево")("право");
console.log(FST(p)); // "лево"
console.log(SND(p)); // "право"
# То же на Python. Обратите внимание: каррирование обязательно —
# в лямбда-исчислении функция всегда одноаргументная.
PAIR = lambda a: lambda b: lambda f: f(a)(b)
TRUE = lambda a: lambda b: a
FALSE = lambda a: lambda b: b
FST = lambda p: p(TRUE)
SND = lambda p: p(FALSE)
p = PAIR("лево")("право")
print(FST(p)) # лево
print(SND(p)) # право
Скопируйте и запустите. Это не иллюстрация «по мотивам» — это буквально тот же терм, записанный синтаксисом вашего языка.
Производные операции
Раз пара — обычный терм, над ней можно строить что угодно.
SWAP = λp. PAIR (SND p) (FST p)
CURRY = λf. λa. λb. f (PAIR a b) -- функция от пары → каррированная
UNCURRY = λf. λp. f (FST p) (SND p) -- каррированная → функция от пары
Раскрутим SWAP (PAIR M N) целиком:
SWAP (λf. f M N)
= (λp. PAIR (SND p) (FST p)) (λf. f M N)
шаг 1 — бета
→ PAIR (SND (λf. f M N)) (FST (λf. f M N))
шаг 2 — считаем SND (уже разбирали выше, 5 шагов)
→ PAIR N (FST (λf. f M N))
шаг 3 — считаем FST
→ PAIR N M
шаг 4-5 — сворачиваем PAIR
→ λf. f N M
Получили пару с переставленными полями. Никакого мутирования — на выходе новый терм, старый нетронут. Иммутабельность здесь не дисциплина и не соглашение: изменять просто нечего, в языке нет присваивания.
Кортежи, тройки и записи
Пара — не предел. Тройка строится в лоб, по той же схеме:
TRIPLE = λa. λb. λc. λf. f a b c
T1 = λt. t (λa. λb. λc. a)
T2 = λt. t (λa. λb. λc. b)
T3 = λt. t (λa. λb. λc. c)
Или вложением пар: PAIR a (PAIR b c), тогда b достаётся как FST (SND t), а c — как SND (SND t). Оба варианта рабочие; прямой n-местный вариант эффективнее (один шаг вместо цепочки), вложенный — универсальнее, потому что не требует нового определения под каждую арность.
Обобщение очевидно: запись с n полями — это функция, принимающая n-местный селектор. Именно так устроены записи в лямбда-исчислении, и именно так выглядит паттерн «объект без класса» в функциональных языках:
// "Объект" User без единого поля — только замыкание
const User = name => age => role => selector => selector(name)(age)(role);
const u = User("Аня")(31)("admin");
const getName = u => u(n => a => r => n);
const getRole = u => u(n => a => r => r);
// а можно спроецировать сразу во что угодно, не доставая поля по одному:
const describe = u => u(n => a => r => `${n}, ${a}, роль: ${r}`);
console.log(getName(u)); // Аня
console.log(describe(u)); // Аня, 31, роль: admin
Это ровно то, что в ООП называют паттерном Visitor: структура не отдаёт свои внутренности наружу, а принимает посетителя и сама решает, что ему показать. Разница только в том, что здесь Visitor — не интерфейс с методами, а одна функция. Про сам паттерн подробно — в треке по паттернам проектирования, а про функциональный стиль вообще — в функциональном программировании.
Зачем это нужно: PRED через пару
Пара — не украшение. Она решает задачу, которая без неё выглядит безнадёжной.
Вспомним числа Чёрча: число n — это «применить функцию n раз», n f x = f (f (... (f x))). Прибавить единицу легко: обернуть ещё одним применением. А вот отнять единицу — как? У числа нет обратного хода, вы не можете «развернуть» применение функции.
Стивен Клини нашёл трюк (по легенде — сидя в кресле у стоматолога). Идея: если нельзя идти назад, будем тащить за собой предыдущее значение. Заведём пару (предыдущее, текущее) и будем сдвигать её вперёд:
ZZ = PAIR ZERO ZERO
SS = λp. PAIR (SND p) (SUCC (SND p))
PRED = λn. FST (n SS ZZ)
SS берёт пару (a, b) и возвращает (b, b+1). Применили n раз к (0, 0) — получили (n-1, n). Берём первое поле.
Раскрутим PRED THREE до конца. Обозначим числа Чёрча c0, c1, c2, c3.
PRED c3
= (λn. FST (n SS ZZ)) c3
шаг 1 — бета
→ FST (c3 SS ZZ)
шаг 2 — разворачиваем c3 = λf.λx. f (f (f x))
= FST (((λf. λx. f (f (f x))) SS) ZZ)
шаг 3 — бета: f := SS
→ FST ((λx. SS (SS (SS x))) ZZ)
шаг 4 — бета: x := ZZ
→ FST (SS (SS (SS ZZ)))
Теперь считаем изнутри. ZZ = PAIR c0 c0 = λf. f c0 c0.
шаг 5 — SS ZZ
= (λp. PAIR (SND p) (SUCC (SND p))) (PAIR c0 c0)
→ PAIR (SND (PAIR c0 c0)) (SUCC (SND (PAIR c0 c0)))
→ PAIR c0 (SUCC c0)
= PAIR c0 c1
шаг 6 — SS (PAIR c0 c1)
→ PAIR (SND (PAIR c0 c1)) (SUCC (SND (PAIR c0 c1)))
→ PAIR c1 (SUCC c1)
= PAIR c1 c2
шаг 7 — SS (PAIR c1 c2)
→ PAIR c2 (SUCC c2)
= PAIR c2 c3
шаг 8 — FST (PAIR c2 c3)
→ c2
PRED 3 = 2. И заодно PRED 0 = FST (0 SS ZZ) = FST ZZ = 0 — ноль остаётся нулём, вычитание на натуральных числах обрезается снизу.
# PRED целиком на Python — можно запустить и проверить
ZERO = lambda f: lambda x: x
SUCC = lambda n: lambda f: lambda x: f(n(f)(x))
ZZ = PAIR(ZERO)(ZERO)
SS = lambda p: PAIR(SND(p))(SUCC(SND(p)))
PRED = lambda n: FST(n(SS)(ZZ))
def to_int(n):
"""Вытаскиваем питоновское число из числа Чёрча: считаем применения."""
return n(lambda k: k + 1)(0)
three = SUCC(SUCC(SUCC(ZERO)))
print(to_int(PRED(three))) # 2
print(to_int(PRED(ZERO))) # 0
Цена вопроса: PRED n требует O(n) шагов и на каждом шаге строит новую пару. Вычесть единицу дороже, чем прибавить — асимметрия, которой в обычных числах нет. Это плата за кодирование «число = количество применений».
Списки: два способа
С парой в руках список строится минимум двумя разными способами. Оба используются в реальных языках, и разница между ними — не academic trivia, а вопрос сложности операций.
из лямбд)) Через пары NIL = PAIR TRUE TRUE CONS кладёт флаг + данные HEAD и TAIL за O(1) нужен явный флаг пустоты Свёрткой (Church) список = свой reduceRight MAP, SUM, LENGTH тривиальны TAIL дорогой — O(n) рекурсия не нужна Scott encoding список = свой pattern match HEAD и TAIL за O(1) обход требует Y-комбинатор
Способ 1: вложенные пары с флагом
Самый прямолинейный перенос связного списка из C. Узел — это пара (голова, хвост), а пустой список надо как-то отличить. Добавляем флаг:
NIL = PAIR TRUE TRUE
CONS = λh. λt. PAIR FALSE (PAIR h t)
ISNIL = FST
HEAD = λl. FST (SND l)
TAIL = λl. SND (SND l)
Первое поле — «пустой ли я». У NIL там TRUE, у любого узла — FALSE. Второе поле у узла — пара из головы и хвоста; у NIL оно мусорное (TRUE), и трогать его нельзя.
Раскрутим HEAD (CONS M NIL):
CONS M NIL
= (λh. λt. PAIR FALSE (PAIR h t)) M NIL
шаг 1 — бета: h := M
→ (λt. PAIR FALSE (PAIR M t)) NIL
шаг 2 — бета: t := NIL
→ PAIR FALSE (PAIR M NIL)
HEAD (PAIR FALSE (PAIR M NIL))
= (λl. FST (SND l)) (PAIR FALSE (PAIR M NIL))
шаг 3 — бета
→ FST (SND (PAIR FALSE (PAIR M NIL)))
шаг 4 — SND берёт второе поле
→ FST (PAIR M NIL)
шаг 5 — FST берёт первое поле
→ M
HEAD и TAIL здесь — константное число шагов, независимо от длины списка. Это важное свойство, и второй способ его теряет.
const NIL = PAIR(TRUE)(TRUE);
const CONS = h => t => PAIR(FALSE)(PAIR(h)(t));
const ISNIL = FST;
const HEAD = l => FST(SND(l));
const TAIL = l => SND(SND(l));
// Список [1, 2, 3]
const xs = CONS(1)(CONS(2)(CONS(3)(NIL)));
console.log(HEAD(xs)); // 1
console.log(HEAD(TAIL(xs))); // 2
console.log(ISNIL(xs)(":пусто")(":не пусто")); // :не пусто
console.log(ISNIL(NIL)(":пусто")(":не пусто")); // :пусто
Способ 2: список — это его собственная свёртка
Второй способ красивее и на практике полезнее. Идея: раз единственное, что мы делаем со списком, — это обходим его, пусть список сам себя обходит.
NIL = λc. λn. n
CONS = λh. λt. λc. λn. c h (t c n)
Список принимает две вещи: c — что делать с каждым элементом, n — что вернуть на пустом списке. Это в точности сигнатура reduceRight / foldr.
Соберём [1, 2, 3] руками, шаг за шагом. Начинаем с конца.
CONS 3 NIL
= (λh. λt. λc. λn. c h (t c n)) 3 NIL
шаг 1 — бета: h := 3
→ (λt. λc. λn. c 3 (t c n)) NIL
шаг 2 — бета: t := NIL
→ λc. λn. c 3 (NIL c n)
шаг 3 — считаем NIL c n = (λc. λn. n) c n → (λn. n) n → n
→ λc. λn. c 3 n
Теперь надстраиваем двойку:
CONS 2 (λc. λn. c 3 n)
шаг 4 — бета: h := 2
→ (λt. λc. λn. c 2 (t c n)) (λc. λn. c 3 n)
шаг 5 — бета: t := (λc. λn. c 3 n)
→ λc. λn. c 2 ((λc. λn. c 3 n) c n)
шаг 6 — редуцируем внутреннюю аппликацию (два бета-шага)
→ λc. λn. c 2 (c 3 n)
И единицу:
CONS 1 (λc. λn. c 2 (c 3 n))
шаг 7-9 — те же три шага
→ λc. λn. c 1 (c 2 (c 3 n))
Итог: список [1,2,3] — это терм λc. λn. c 1 (c 2 (c 3 n)). Структура списка полностью растворилась в структуре вложенных вызовов.
Теперь любая операция — это просто подстановка подходящих c и n:
SUM = λl. l PLUS ZERO
LENGTH = λl. l (λh. λacc. SUCC acc) ZERO
ISNIL = λl. l (λh. λacc. FALSE) TRUE
HEAD = λl. l (λh. λacc. h) NIL
MAP = λg. λl. λc. λn. l (λh. λacc. c (g h) acc) n
APPEND = λl1. λl2. λc. λn. l1 c (l2 c n)
Раскрутим LENGTH на списке [a, b], то есть на терме λc. λn. c a (c b n). Обозначим шаг STEP = λh. λacc. SUCC acc:
LENGTH (λc. λn. c a (c b n))
= (λl. l STEP ZERO) (λc. λn. c a (c b n))
шаг 1 — бета
→ (λc. λn. c a (c b n)) STEP ZERO
шаг 2 — бета: c := STEP
→ (λn. STEP a (STEP b n)) ZERO
шаг 3 — бета: n := ZERO
→ STEP a (STEP b ZERO)
шаг 4 — STEP a X = (λh. λacc. SUCC acc) a X → (λacc. SUCC acc) X → SUCC X
→ SUCC (STEP b ZERO)
шаг 5 — то же для внутреннего
→ SUCC (SUCC ZERO)
= c2
Длина 2. Заметьте: h в STEP не используется вообще — нам всё равно, что за элементы, важно только их количество. Формальный аппарат сам выкинул лишнее.
Отдельно стоит проследить APPEND. Почему λc. λn. l1 c (l2 c n) действительно склеивает списки? Потому что l2 c n — это результат свёртки второго списка, и он подставляется на место n в свёртке первого. Начальное значение первой свёртки становится всем вторым списком. Красиво и в один терм.
NIL = lambda c: lambda n: n
CONS = lambda h: lambda t: lambda c: lambda n: c(h)(t(c)(n))
xs = CONS(1)(CONS(2)(CONS(3)(NIL)))
# Подставляем обычные питоновские функции вместо c и n
print(xs(lambda h: lambda acc: h + acc)(0)) # 6 — сумма
print(xs(lambda h: lambda acc: acc + 1)(0)) # 3 — длина
print(xs(lambda h: lambda acc: [h] + acc)([])) # [1, 2, 3] — материализация
print(xs(lambda h: lambda acc: max(h, acc))(0)) # 3 — максимум
MAP = lambda g: lambda l: lambda c: lambda n: l(lambda h: lambda acc: c(g(h))(acc))(n)
doubled = MAP(lambda x: x * 2)(xs)
print(doubled(lambda h: lambda acc: [h] + acc)([])) # [2, 4, 6]
const NIL = c => n => n;
const CONS = h => t => c => n => c(h)(t(c)(n));
const xs = CONS(1)(CONS(2)(CONS(3)(NIL)));
const toArray = l => l(h => acc => [h, ...acc])([]);
console.log(xs(h => acc => h + acc)(0)); // 6
console.log(toArray(xs)); // [1, 2, 3]
const MAP = g => l => c => n => l(h => acc => c(g(h))(acc))(n);
const FILTER = p => l => c => n => l(h => acc => (p(h) ? c(h)(acc) : acc))(n);
console.log(toArray(MAP(x => x * 10)(xs))); // [10, 20, 30]
console.log(toArray(FILTER(x => x % 2 === 1)(xs))); // [1, 3]
Обратите внимание на FILTER: он не «удаляет» элементы, он просто не вызывает c для тех, кто не прошёл проверку — и элемент бесследно исчезает из результирующей свёртки. Ни массивов, ни сдвигов, ни новой памяти в явном виде.
Больное место: TAIL при свёрточном кодировании
У этого способа есть цена. HEAD берётся легко (первый вызов c побеждает и возвращает h), а вот TAIL — нет. Свёртка идёт от конца к началу, и когда мы доходим до головы, «хвост» как отдельный объект уже не существует — он растворён в накопленном значении.
Приходится применить ровно тот же трюк, что и в PRED: тащить пару (хвост, весь список).
TAIL = λl. FST (l (λh. λp. PAIR (SND p) (CONS h (SND p))) (PAIR NIL NIL))
Проверим на [a, b], обозначив шаг TS = λh. λp. PAIR (SND p) (CONS h (SND p)):
шаг 1 — свёртка разворачивается в
FST (TS a (TS b (PAIR NIL NIL)))
шаг 2 — внутренний вызов: p := PAIR NIL NIL, SND p = NIL
TS b (PAIR NIL NIL)
→ PAIR NIL (CONS b NIL)
= PAIR NIL [b]
шаг 3 — внешний вызов: p := PAIR NIL [b], SND p = [b]
TS a (PAIR NIL [b])
→ PAIR [b] (CONS a [b])
= PAIR [b] [a, b]
шаг 4 — FST
→ [b]
Работает, но каждый TAIL — это полный обход, O(n). Если писать рекурсивный алгоритм через HEAD/TAIL, получите квадратичную сложность там, где ожидали линейную. Отсюда практический вывод: выбор кодирования диктует профиль сложности, и это не абстракция — ровно та же дилемма всплывает при выборе между foldr-based API и явными cons-ячейками в настоящих языках.
Способ 3: Scott encoding, он же pattern matching
Есть третий вариант, который в современных обсуждениях встречается чаще всего, потому что он прямо соответствует сопоставлению с образцом:
NIL = λonCons. λonNil. onNil
CONS = λh. λt. λonCons. λonNil. onCons h t
Разница с предыдущим — крошечная, но принципиальная: CONS передаёт onCons сырой хвост t, а не результат свёртки t c n. Список не обходит сам себя, он только сообщает, какой у него конструктор, и отдаёт содержимое.
ISNIL = λl. l (λh. λt. FALSE) TRUE
HEAD = λl. l (λh. λt. h) NIL
TAIL = λl. l (λh. λt. t) NIL
Все три — константное время. Взамен теряется бесплатный обход: LENGTH и SUM уже не выражаются подстановкой, для них нужна настоящая рекурсия, а рекурсии без имён у нас пока нет. Как её получить — тема следующей статьи про Y-комбинатор.
// Scott encoding — это switch по конструктору, записанный как вызов
const NIL_S = onCons => onNil => onNil;
const CONS_S = h => t => onCons => onNil => onCons(h)(t);
const match = (list, { cons, nil }) => list(h => t => cons(h, t))(nil);
const ys = CONS_S(1)(CONS_S(2)(NIL_S));
const describe = l => match(l, {
cons: (h, t) => `голова ${h}, дальше ещё что-то`,
nil: "пусто",
});
console.log(describe(ys)); // голова 1, дальше ещё что-то
console.log(describe(NIL_S)); // пусто
Если вы писали на Elixir, Haskell, Rust или Scala — узнаёте case. Scott encoding и есть pattern matching, только вместо синтаксиса компилятора его делает сама структура данных. В треке по Elixir сопоставление с образцом — базовый инструмент; полезно знать, что под ним лежит.
Сравнение трёх кодирований
Короткое правило. Нужно читать структуру (взять хвост, разобрать по конструкторам) — Scott. Нужно свернуть в значение (сумма, длина, отображение) — Church. Пары с флагом — учебный промежуточный вариант, который хорош тем, что не требует ничего, кроме уже разобранной пары.
Типичные ошибки
Забыли каррирование. В Python и JS соблазнительно написать lambda a, b: ... вместо lambda a: lambda b: .... Это уже не лямбда-исчисление: в нём каждая функция ровно одноаргументная, а «функция двух аргументов» — это функция, возвращающая функцию. Смешивать нельзя — код перестанет стыковаться с чужими комбинаторами.
Взяли HEAD у NIL. В чистом лямбда-исчислении это не падает с исключением, а возвращает мусор — какой-то терм, который вы туда положили заглушкой. Проверка ISNIL — целиком на совести вызывающего. Это, кстати, точная модель того, почему нетипизированные языки требуют дисциплины: система типов, которая запретила бы такое, появится только в статье про типизированное лямбда-исчисление.
Захват имён при подстановке. Определяя свои комбинаторы, легко случайно связать свободную переменную. В CONS = λh. λt. λc. λn. c h (t c n) имена c и n выбраны так, чтобы не пересекаться с типичными аргументами; если бы вместо c стояло h, всё сломалось бы. Механику разбирали в статье про подстановку — здесь она перестаёт быть теорией.
Ленивость против энергичности. FILTER в JS выше работает не потому, что мы умные, а потому что мы явно написали тернарник, который не вызывает c. В энергичном языке аргументы вычисляются до вызова, и наивный перенос терма может зациклиться там, где в лямбда-исчислении с нормальным порядком всё сходится. Это тема статьи про стратегии вычисления.
Экспоненциальный размер. Церковные списки из десяти элементов — это терм в сотни узлов. Кодирование Чёрча — доказательство выразительности, а не рекомендация по производительности. Настоящие компиляторы функциональных языков используют нативные структуры; лямбда-исчисление объясняет, почему это возможно делать одними функциями, а не почему это нужно.
Где это встречается в реальном коде
Кодирование данных функциями — не музейный экспонат.
Continuation-passing style. Любая функция вида getUser(id, callback) — это Scott encoding результата: вместо возврата значения функция вызывает переданный обработчик. Промисы, Result/Either через .match({ ok, err }), обработка ошибок в стиле «передай два колбэка» — всё оттуда.
Sum types в языках без sum types. В JavaScript нет алгебраических типов, но пишут так:
// Either, закодированный по Скотту — ни одного объекта, только замыкания
const Left = e => ({ match: ({ left }) => left(e) });
const Right = v => ({ match: ({ right }) => right(v) });
const parse = s => {
const n = Number(s);
return Number.isNaN(n) ? Left(`не число: ${s}`) : Right(n);
};
const show = r => r.match({
left: e => `ошибка: ${e}`,
right: v => `значение: ${v * 2}`,
});
console.log(show(parse("21"))); // значение: 42
console.log(show(parse("abc"))); // ошибка: не число: abc
Обёртка в объект — косметика; сердцевина здесь ровно λv. λonLeft. λonRight. onRight v.
Свёртки как универсальный API. То, что список — это свой foldr, в Haskell дошло до уровня библиотеки: класс Foldable описывает любую структуру, которую можно свернуть, и через него выражаются length, sum, elem, toList. Церковное кодирование — это ровно определение «структура ЕСТЬ своя свёртка».
Тактика в компиляторах. Приём с парой из PRED — по сути амортизация: чтобы получить предыдущее состояние, тащим его рядом с текущим. Тот же шаблон встречается в потоковой обработке (скользящее окно) и в reducer-архитектурах фронтенда, где состояние всегда прошлое-плюс-новое.
Упражнения
Сведите к нормальной форме, показывая каждый шаг. Ответы ниже — но сначала карандашом.
SND (PAIR (PAIR A B) C)FST (SWAP (PAIR M N))HEAD (TAIL (CONS A (CONS B NIL)))— для кодирования ScottLENGTH (APPEND [A] [B, C])— для церковного кодирования, где[A] = λc.λn. c A n- Напишите комбинатор
SECOND-OR-DEFAULT, который у пары(a, b)возвращаетb, а если получилNIL(в кодировании через пары с флагом) — возвращает заданное значение по умолчанию.
Ответы
1.
SND (PAIR (PAIR A B) C)
= (λp. p FALSE) ((λa.λb.λf. f a b) (PAIR A B) C)
→ (λp. p FALSE) (λf. f (PAIR A B) C) [две беты внутри]
→ (λf. f (PAIR A B) C) FALSE
→ FALSE (PAIR A B) C
= ((λa.λb. b) (PAIR A B)) C
→ (λb. b) C
→ C
2. SWAP (PAIR M N) → PAIR N M = λf. f N M (разобрано в тексте, 5 шагов). Дальше:
FST (λf. f N M)
→ (λf. f N M) TRUE
→ TRUE N M
→ (λb. N) M
→ N
Итого FST (SWAP p) = SND p — свойство, которое можно доказать в общем виде, а не проверять на примерах.
3. Для Scott encoding:
CONS A (CONS B NIL)
= λonC. λonN. onC A (CONS B NIL)
TAIL (λonC. λonN. onC A (CONS B NIL))
= (λl. l (λh.λt. t) NIL) (...)
→ (λonC. λonN. onC A (CONS B NIL)) (λh.λt. t) NIL
→ (λonN. (λh.λt. t) A (CONS B NIL)) NIL
→ (λh.λt. t) A (CONS B NIL)
→ (λt. t) (CONS B NIL)
→ CONS B NIL
HEAD (CONS B NIL)
= (λl. l (λh.λt. h) NIL) (λonC. λonN. onC B NIL)
→ (λonC. λonN. onC B NIL) (λh.λt. h) NIL
→ (λh.λt. h) B NIL
→ (λt. B) NIL
→ B
4. APPEND [A] [B,C] = λc.λn. c A (c B (c C n)) — трёхэлементный список. Свёртка со STEP = λh.λacc. SUCC acc и нулём даёт SUCC (SUCC (SUCC ZERO)) = c3. Длина 3, что и ожидалось: APPEND не перестраивает узлы, он подставляет вторую свёртку на место начального значения первой.
5.
SECOND-OR-DEFAULT = λl. λd. (ISNIL l) d (SND (SND l))
Здесь ISNIL l — булево значение Чёрча, то есть само работает как if: применённое к двум веткам, выбирает нужную. Важная тонкость: в энергичном языке ветка SND (SND l) вычислится до выбора и на NIL даст мусор, а при нормальном порядке редукции — нет. На JS/Python это лечится оборачиванием веток в thunk-функции:
const SECOND_OR_DEFAULT = l => d =>
ISNIL(l)(() => d)(() => SND(SND(l)))(); // ветки — функции, вызываем после выбора
Мини-итог
- Структура данных в лямбда-исчислении — это функция, которая принимает потребителя своего содержимого и сама решает, что ему передать.
- Пара
λa.λb.λf. f a bплюс селекторыTRUE/FALSEдают кортеж; из кортежей строятся записи, объекты, деревья. - Пара нужна не для красоты: без неё не выражается
PRED, а значит и вычитание, иTAILпри церковном кодировании. - Списки кодируются тремя способами. Church (свёртка) — данные без рекурсии, но дорогой
TAIL. Scott — константный доступ, но обход требует рекурсии. Пары с флагом — учебный компромисс. - Всё это переносится в JS и Python один в один каррированными стрелочными функциями — и всплывает в продакшн-коде как CPS, Visitor,
Either.matchиFoldable.
Обратите внимание на паттерн, который повторяется по всему треку: у нас снова нет ничего нового, мы только по-разному складываем три конструкции из статьи про синтаксис. Единственное, чего до сих пор нет, — способа заставить функцию вызвать саму себя. Без него не написать SUM для Scott-списков, не написать факториал, не написать вообще ни одного цикла.
Источники
- Benjamin C. Pierce, «Types and Programming Languages», глава 5 — каноничный разбор кодирования Чёрча, включая пары и
PRED: https://www.cis.upenn.edu/~bcpierce/tapl/ - Henk Barendregt, «The Lambda Calculus: Its Syntax and Semantics» — исчерпывающий справочник по свойствам термов
- Church encoding и Scott encoding, сравнение представлений: https://en.wikipedia.org/wiki/Church_encoding и https://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding
- Haskell
Foldable— «структура как своя свёртка» в виде рабочей библиотеки: https://hackage.haskell.org/package/base/docs/Data-Foldable.html - Раймонд Смаллян, «To Mock a Mockingbird» — комбинаторная логика в виде головоломок, отличная тренировка на раскрутку редукций
Что дальше
Мы построили данные, но пока не умеем их обходить в общем случае: любая рекурсивная функция требует имени, чтобы позвать саму себя, а в лямбда-исчислении имён у функций нет. Разгадка — комбинатор неподвижной точки, один из самых красивых объектов во всей информатике.
