Время от времени я делаю попытки штурмовать функциональное программирование. Не то что бы оно мне нужно, но меня больше интересует, почему я не могу его понять. Что там, в голове, этому мешает?
Если долго биться лбом о стену, то на лбу вырастет мозоль. Но и стена в какой-то момент даст маленькую трещину. Кажется, этот момент настал.
Я подходил к вопросу немного не с той стороны. Потому что в основе ФП лежит
Лямбда-исчисление
И смысл его очень прост.
Ля́мбда-исчисле́ние (λ-исчисление) — формальная система, разработанная американским математиком Алонзо Чёрчем для формализации и анализа понятия вычислимости.
Понимаете, это не какое-то там программирование, не какие-то там модные названия. Это просто система описания вычислений, которая намеренно доведена до абсолютной абстракции и абсолютного минимализма, чтобы ничего вообще не мешало и не отвлекало от чистейшего вычислительного смысла. Машину Тьюринга знаете? Так вот это машина Тьюринга, только описанная с помощью функций. С её помощью можно построить любую программу.
Это не значит, что она удобна или вообще подходит для программирования. Совсем наоборот. Функциональные языки, заимствуя из неё концепции, всё же имеют дополнительные расширения, которые делают их более комфортными. Но чтобы разобраться в функциональном программировании, корни его надо искать именно в лямбда-исчислении.
Лямбда
Можно вздохнуть свободно – название "лямбда" не имеет никакого особенного смысла. С тем же успехом это могли быть сигма, альфа и что угодно. Лямбда это просто обозначение абстрактной функции, которое оказалось вот таким. В обычном программировании мы написали бы просто function.
Всё есть функция
Подобно тому как в JavaScript всё есть объект, в лямбда-исчислении всё есть функция. Вообще всё.
Синтаксис записи функции такой:
λx.M
Вот сейчас будет совсем легко. Но это последний раз, когда легко.
- λ это собственно лямбда, то есть функция
- x это аргумент функции
- M это тело функции
Выражение λx.M транслируется в привычное программистское
function(x) { M }
И мы (во всяком случае, я) счастливы, что хотя бы это понятно.
В примерах любят показывать функцию тождественности, которая возвращает свой же аргумент:
λx.x
Это эквивалент такого кода:
function(x) { return x }
Или в традиционной математической записи:
f(x) = x
Это тривиально, но сделать что-то более сложное будет уже непросто.
Мягко говоря.
Кодирование Чёрча
Самое большое потрясение вызывает то, что даже литералы, такие как 1, 2, 3, 'A', 'B', 'C' и т.д., не существуют в лямбда-исчислении. Единственный примитивный тип это функция, и чтобы записать число 5, мы должны представить его через функции. Это называется кодированием Чёрча, которое существует для чисел, для логических значений, для пар значений и т.д.
Здесь требуется долгая остановка и внимательное изучение принципов. Если это займёт неделю, значит неделю, спешить не надо.
Сразу откажитесь от понятия "хранение данных", сотрите его из сознания. Его просто нет, как нет и "данных". Есть только функции. Как закодировать число 5, не имея числа 5?
В кодировании Чёрча число N кодируется как функция, применённая к аргументу N раз.
Смотрите, мы определяем несуществующее в данной системе число N через применение функции N раз, где N это всё-таки число. Какой-то замкнутый круг.
Но давайте по порядку.
Число 0
λf.λx.x
Если вы ещё не привыкли, это λf.M, где M = λx.x, также можно записать λf.(λx.x)
Разбираем:
Есть λf – функция λ с аргументом f, а тело этой (которая λf) функции – λx.x. Перепишем традиционно:
function(f) { λx.x }
Теперь разберём тело функции λf. Оно в свою очередь содержит функцию тождественности λx.x, возвращающую свой аргумент x. Перепишем и его:
function(f) {
function(x) { return x }
}
Дальше будем писать без return, т.к. тело любой функции, будучи вычислено, всегда является возвращаемым значением (кcтати, так можно писать в Rust):
function(f) {
function(x) { x }
}
Теперь, чтобы передать аргумент x традиционным способом, переделаем внешнюю функцию под два аргумента f, x:
function(f, x) {
function(x) { x }
}
И далее, чисто ради упрощения, так как функцию тождественности можно заменить её аргументом, перепишем так:
function(f, x) { x }
В результате мы получили какую-то ерунду. Где здесь 0?
Обратим внимание, что в функцию передаётся аргумент-функция f, которая нигде не используется. По правилам кодирования Чёрча, число N это функция f, применённая N раз к аргументу x. Но здесь функция f не применялась к аргументу x ни разу – то есть ноль раз.
Таким образом, мы закодировали ноль в каком-то странном, но логически доказуемом виде, а физически его нигде нет. Это взрывает мозг.
Подобно тому как мы можем объяснить электроны через электромагнитные поля, но не можем объяснить природу самих полей, здесь мы также объясняем число 0 через то, что само по себе необъяснимо.
Количество здесь – это не данные, это процесс. Данные мы получаем, когда трактуем применение функций. Они рождаются только во взаимодействии с чем-то. Функцию λf.λx.x мы трактуем как 0.
Сейчас это знание практически бесполезно, но давайте дальше.
Число 1
λf.λx.f x
Функция, описывающая 0, немного изменилась. Я больше не буду переписывать её в традиционном виде, так как пора привыкать к оригинальной записи.
Для ясности можно записать так:
λf.(λx.(f x))
Есть функция λf с аргументом-функцией f. Тело этой (которая λf) функции содержит функцию λx с аргументом x и телом f x.
В теле функции λx мы применяем функцию f к аргументу x, это записывается как f x. Визуально можно представить, будто поток аргументов справа от функции движется в функцию:
f <-- x
Как видим, функция f на этот раз используется и применяется один раз. Значит, аналогичным странным образом мы закодировали число 1.
Число 5
Далее мы можем использовать шорткаты / определения / макросы для кодировок Чёрча, чтобы снизить избыточность кода. Вот так:
0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
и т.д.
То есть запись вида add 1 2 позволит нам не писать, но подразумевать:
add (λf.λx.f x) (λf.λx.f (f x))
Как видим, в кодировке числа 2 функция f применяется к x два раза:
f (f x)
Сначала к x применяется f, затем к результату применяется ещё раз f.
f <-- (f <-- x)
В данном случае скобки важны, так как определяют, что должно вычисляться первым. Без скобок мы получим такую запись:
f f x
И это будет означать: применить f к f, а затем результат применить к x:
(f <-- f) <-- x
Следуя шаблону, мы теперь можем записать представление числа 5, применив функцию f пять раз:
5 = λf.λx.f (f (f (f (f x))))
Аналогичным образом можно закодировать любое число, например триллион. Но для этого придётся написать, как функция применяется триллион раз. Серьёзно. Другого пути нет.
Именно поэтому лямбда-исчисление не подходит для решения практических задач. Но оно доказывает, что любую задачу можно решить с единственным типом "функция".
Таинственная f
Итак, чисто концептуально мы (надеюсь) поняли, что число N в кодировке Чёрча это функция f, применённая N раз к аргументу x.
Вроде бы звучит нормально, но что это за функция f? Откуда она берётся и что делает?
Исходя из определения кодировки Чёрча, это ведь вообще любая функция, да и аргумент x тоже любой! Суть не в функции, а в том, что она должна примениться N раз.
Это действительно так. В лямбда-исчислении нет концепции числа, а есть лишь процесс применения функции, описанный как синтаксическая структура.
Поэтому функция f в данном случае остаётся абстрактной. Мы её не знаем, но нам и не нужно её знать, потом что нам нужна только структура f (f (f ...(f x))). Запись этой структуры и есть наша трактовка числа. Более того, f и должна оставаться абстрактной, чтобы такая структура могла существовать, но про это я попытаюсь рассказать во второй части.
Однако же числа сами по себе нас редко интересуют. Нас больше интереcуют операции с числами, например сложение 1 + 2. А для этого нужны:
- Кодировка Чёрча для числа 1: λf.λx.f x
- Кодировка Чёрча для числа 2: λf.λx.f (f x)
- Функция сложения: ???
И в результате должна получиться кодировка числа 3: λf.λx.f (f (f x))
Для начала отметим, что операции "+" у нас нет. Есть функция сложения, её можно условно назвать и "+", и "add", но сложение двух чисел будет выглядеть не как 1 + 2, а как + 1 2 или add 1 2.
(add <--1) <--2
Здесь мы применяем функцию add к аргументу 1, а затем результат (это будет какая-то другая функция) применяем к аргументу 2.
Напишем... ха-ха, напишем, хорошая шутка, просто погуглим функцию add m n. Она должны складывать числа m и n:
add = λm.λn.λf.λx.m f (n f x)
Спокойно, всё не так страшно!
В обычной программе мы могли бы сделать функцию двух аргументов, вроде
function add(m, n)
Но в лямбда-исчислении функция может принимать только один аргумент. Поэтому add это функция одного аргумента m, а её тело я отодвину подальше для наглядности:
λm. -----> λn.λf.λx.m f (n f x)
Теперь можно видеть, что тело λm это в свою очередь функция одного аргумента n:
λn. -----> λf.λx.m f (n f x)
То есть функция add не принимает два аргумента, но принимает один и возвращает функцию λn, которая содержит первый и принимает второй.
Полный разбор сделаем ниже, а пока нужно понять, что такое
Бета-редукция
Обозначение "бета" опять же не имеет каких-то скрытых смыслов и выбрано произвольно. Оно нужно только для того, чтобы отличать эту конкретную бета-редукцию от остальных типов редукции.
Смысл бета-редукции успокаивающе прост: мы берём аргумент функции и подставляем его в тело функции, в те места, где он указан. После этого нам уже не нужна внешняя оболочка функции, которая принимает аргумент – он уже принят, и тело функции мы можем рассматривать самостоятельно. Произошла редукция, будто бы выражение сбросило с себя внешний слой.
λm.λn.λf.λx.m f (n f x) 1 2 <--- указываем аргументы m = 1, n = 2
подставляем 1 вместо m в тело функции λm и сбрасываем внешний слой λm:
λn.λf.λx.1 f (n f x)
в результате мы получили другую функцию λn c аргументом n, которая готова принять следующий аргумент.
λn.λf.λx.1 f (n f x) 2 <--- оставшийся аргумент n = 2
подставляем 2 вместо n в тело функции λn и сбрасываем внешний слой λn:
λf.λx.1 f (2 f x)
Больше аргументов нет.
Теперь раскроем кодировки 1 и 2, пометив для них аргументы f и x как g, y и h, z:
λf.λx.(λg.λy.g y) f (λh.λz.h(h z) f x)
Делаем бета-редукцию для (λg.λy.g y) f, подставляя фактический аргумент f в качестве ожидаемого функцией аргумента g:
λf.λx.λy.f y (λh.λz.h(h z) f x)
Делаем вторую бета-редукцию для λh.λz.h(h z) f, подставляя фактический аргумент f в качестве ожидаемого функцией h:
λf.λx.λy.f y (λz.f(f z)) x
Делаем третью бета-редукцию для (λz.f(f z)) x, подставляя фактический аргумент x в качестве ожидаемого функцией z:
λf.λx.λy.f y (f(f x))
Делаем четвёртую бета-редукцию для λy.f y (f(f(x)), подставляя фактический аргумент (f(f(x)) в качестве ожидаемого функцией y:
λf.λx.f(f(f x))
И... мы получили представление Чёрча для числа 3: функция f применена к аргументу x три раза.
Мы сложили 1 и 2 неизвестным науке способом!
Возвращаясь к нулю. Попробуем сложить 0 и 1. Вот промежуточная форма с подстановкой 0 и 1:
λf.λx.0 f (1 f x)
Раскроем 0 и 1:
λf.λx.(λg.λy.y) f ((λh.λz.h z) f x)
Выполним редукции:
λf.λx.(λy.y) ((λz.f z) x)
λf.λx.(λy.y) (f x)
λf.λx.f x
И мы получили кодировку 1 (функция f применяется к x ровно один раз). Всё правильно, 0 + 1 = 1. Таким образом, кодировка 0 действительно работает как 0.
На этом пока всё. Продолжать пока рано, нагрузка на мозг слишком высока. Этот материал нужно перечитывать, привлекая ресурсы поиска и требуя объяснений от DeepSeek (кстати он хорош), пока не образуется навык беглого чтения лямбда-выражений и понимания их преобразования.
Далее можно будет разобраться с более сложными понятиями.