Давайте теперь реализуем какую-нибудь сложную структуру данных, например, список. Список, конечно, односвязный. Пусть мы хотим, чтобы list хранил в себе список из чисел 1, 2, 3. Тогда эту переменную мы определим таким образом, что выражение list f 0 будет равно f 1 (f 2 (f 3 0)). Говоря в терминах императивных языков программирования, list принимает два аргумента: функцию объединения и какой-то параметр, который мы назовем аккумулятором, а затем проходит по списку справа налево и объединяет очередной элемент с аккумулятором. Иначе говоря, производит правую свертку. Чем-то похож на цикл for с конца.
Список из трех элементов 1, 2, 3, например, реализуется так:
list123 := \f. \acc. f 1 (f 2 (f 3 acc))
Пустой список выглядит так (он, кстати, совпадает с false и zero, удивительное дело):
nil := \f. \acc. acc
Список из одного элемента конструируется так:
singleton := \x. \f. \acc. f x acc
Добавление элемента h в начало списка t (сокращения от слов head и tail). Никого же не смущает функция, принимающая четыре аргумента, да?
cons := \h. \t. \f. \acc. f h (t f acc)
Конкатенация (склеивание) списков:
concat := \alist. \blist. \f. \acc. alist f (blist f acc)
Забавно, но конкатенация списков также умеет складывать числа.
Проверка списка на пустоту похожа на проверку числа на нуль:
isnul := \list. list (\x. \acc. false) true
Подсчет длины списка:
length := \list. list (\x. \acc. succ acc) 0
Или, если применить η-преобразование:
length := \list. list (\x. succ) 0
Получение первого элемента списка (false, если список пустой):
head := \list. list (\x. \acc. x) false
Кстати, заметили опять знакомые выражения? head =b pair true false, даже удивительно.
Получение первого элемента списка со значением по умолчанию в случае пустого списка:
headdef := \def. \list. list (\x. \acc. x) def
А еще headdef =b pair true, если вы хотите кого-нибудь запутать.
Научимся теперь расслаивать список на пару (head, tail), то есть пару из первого элемента списка и списка без первого элемента (хвоста списка). Пожалуй, самое сложное из того, что нам приходилось создавать на текущий момент.
Первое, что приходит в голову — попробовать написать что-то наподобие:
split := \list. list (\x. \acc. pair x acc) (...)
То есть втупую на каждом шаге создавать пару из головы и хвоста.
Но всплывает две проблемы. Первая — acc не является списком. Это результат функции split от хвоста списка. То есть пара.
Чтобы превратить split от списка обратно в список, мы можем использовать cons:
unsplit := \splitres. cons (first splitres) (second splitres)
Так как пара вызывает переданную ей функцию от своих первого и второго элемента, это можно упростить до:
unsplit := \splitres. splitres cons
Наконец, новая версия split:
split := \list. list (\x. \acc. pair x (unsplit acc)) (...)
У нас осталась другая проблема. Не очень понятно, что должно быть на месте ..., чтобы все работало.
Но вот что должен выдать split от списка из одного элемента мы точно знаем, так что давайте попробуем вычислить split (singleton E):
singleton E -> \f. \acc. f E acc split (singleton E) -> -> (singleton E) (\x. \acc. pair x (unsplit acc)) (...) -> -> (\x. \acc. pair x (unsplit acc)) E (...) -> -> pair E (unsplit (...))
А должно быть pair E nil, то есть unsplit (...) -> (...) cons -> nil. Так что пусть ... принимает один аргумент и всегда возвращает nil.
split := \list. list (\x. \acc. pair x (unsplit acc)) (\x. nil)
Значит, теперь у нас split (singleton E) -> pair E nil, что нам и нужно, а дальше функция редукции \x. \acc. pair x (unsplit acc) будет работать как ожидалось.
Можно провести аналогию с таким циклом:
acc = \x. nil
for x in reversed list:
tail = acc cons
acc = pair x tail
return acc
Ну и, конечно, теперь можно реализовать функцию tail, которая возвращает список без своего первого элемента:
tail := \list. second (split list)
Интересно, кстати, что все же произойдет, если split запустить от пустого списка? Для пустого списка split nil -> \x. nil по определению, но что будет, если это выражение интерпретировать как пару?
first (\x. nil) -> (\x. nil) (\a. \b. a) -> nil second (\x. nil) -> (\x. nil) (\a. \b. b) -> nil
Ожидаемо, tail nil -> nil. Не очень ожидаемо, что first (split nil) -> nil. Но тут стоит благодарить случай за то, что nil и false кодируются одинаково, и first (split nil) =b nil =b false =b head nil, так что какая-то консистентность сохранилась.