Типичный любитель ?-исчисления.

Однажды, бороздя просторы интернета, я наткнулся на новость о лиспоподобном, встраиваемом языке программирования Shen. Раньше у них на главной странице висел пример кода на Лиспе. В примере авторы описывают абстрактную коллекцию и функции работы с ними.

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

С лямбда исчислением я был знаком очень поверхностно, так как почти всегда статьи об этом разделе математики состоят полностью из формул, которые никак не попробовать на практике не представляется возможным. Поэтому пришла идея разобраться с ним на практике, и возможно привлечь на темную сторону силы адептов машины Тьюринга ООП.

Если вас не пугает Lisp, много лямбд и y-combinator (не тот, который с новостями),

Вступление

Статья не претендует на полноту охвата материала или на замену SICP. Я не являюсь математиком, и тем более не являюсь знатоком лямбда-исчисления. Единственное на что она претендует – это на линейность изложения. В тексте поставлена задача познакомить читателей с функциями как first-class citizens и сделать это в максимально интересной для лямбда-исчисления форме. В процессе написания кода, я попытаюсь объяснить то, что происходить понятным простым инженерам языком.

Сегодня сильно прослеживается тенденция заимствования концепций из функционального программирования императивными языками (даже в С++ после 30 лет комитет пошёл на такой авантюрный поступок. И да, Java8), поэтому есть надежда, что кому-то эта статья пригодиться. Естественно, если на Хабре найдутся любители лямбда-исчисления, которые меня смогут поправить, добавляйте комментарии.

Итак, «почему был выбрал Лисп» – спросите вы. Причин этому несколько. Первая – это то, что все примеры в статьях о функциональном программировании пишутся на Haskell'е. Вторая – это уже упомянутая книга: Structure and Interpretation of Computer Programs, которая является одной из самых любимых мною книжек и которую я рекомендовал прочитать всем, кто этого еще не сделал. Третья, потому что Лисп – это для настоящих хакеров.


Старая добрая шутка

На Хабре есть несколько статей о лямбда исчислении. Например здесь и здесь. Некоторые из них раскрывают теорию шире, чем это попытаюсь сделать я, поэтому я бы советовал прочитать хотя бы одну их них для понимая того, чем мы будем заниматься. Я не буду приводить здесь всю теорию, дабы не усложнять статью. Для написания наших абстракций, нам будет достаточно статей на Википедии (все настоящие программисты так пишут программы). Англоязычные статьи шире раскрывают тему, поэтому можно использовать статьи об Lambda Calculus и более развернутую статью с описанием кодирования типов Church Encoding.

Также нам надо знать язык программирования LISP. Но не переживайте, если Вы его не знаете, потому что весь синтаксис у него состоит из скобок, мы его быстро выучим. Все что нам надо это знать как лямбда термы записываются в Лиспе и, немного позже, для сокращения записи, несколько функций. Достаточно знать, что в Лиспе, что бы выполнить функцию, нужно заключить ее вызов в скобки, в которых первым аргументом будет имя функции, а за ним будут идти параметры (очень похоже на польскую нотацию). То есть для нахождения суммы нужно писать (+ 2 3), для слияния строк (string-append «Hello» «world!»). Так же стоит сказать, что существует несметное количество диалектов Лиспа. Мы будем использовать Racket из-за удобной среды разработки, но почти весь код будет работать с большинством диалектов (возможно нужно будет использовать другие функции для манипуляции строк и т.п.). Все ссылки на скачивание и инструкции по установке Вы сможете найти на сайте языка.

?-исчисление

Если Вы последовали моему совету прочитали о лямбда исчислении, вы уже знаете что в нем есть три правила для терма:

• переменная x, в Лиспе записывается точно так же, с помощью имени переменной;
• лямбда абстракция (?x.t), может быть записана как обычная функция, известная нам из всех языков программирования: (define (fun x) t); или как безымянная лямбда (lambda (x) t).
• аппликация (t s), это обычный вызов функции, в Racket'е так и записывается (t s).

Итак, с помощью объявления функции и ее вызова, мы попробуем написать систему типов и поможет нам в этом кодирование Чёрча (у Вас должна быть открыта вкладка с Википедией, где о ней написано). Как написал автор англоязычной статьи, это кодирование позволяет представить типы данных и операторы в терминах лямбда-исчисления. Мы это и проверим.

Небольшой недостаток того, что был выбран Лисп в том, что функция всегда требует предоставить ей все аргументы, а не каррирует, как делает например Haskell или ML. Поэтому нам нужно будет явно использовать lisp-лямбды, или использовать функцию curry. Я постараюсь рассказать об этом по мере потребности.

Также в Racket уже зарезервированы некоторые нужные нам имена, поэтому все наши функции будет писать писать с заглавной буквы.
Запускаем среду разработки DrRacket и поехали.

Булевые значения

Начнем мы из Булевых значений, они же True и False. По-началу их реализация может показаться немного странной – в лямбда исчислении все выглядит странно. В дальнейшем мы убедимся, что это работает.

Булевый тип данных для представляет ценность для нас только в том случае, если мы сможем их отличать друг от друга. Это можно сделать с помощью оператора (функции) If. На Википедии уже описан это тип (там все типы описаны), и мы, используя Лисп, перенесем их в редактор.

(define (True a b) a)
(define (False a b) b)
(define (If c a b) (c a b)) 

Используя интерактивный интерпретатор Racket (расположен снизу в нашей IDE), мы можем проверить работоспособность нашей булевой логики. Типы представляют собой функции, которые принимают два аргумента и возвращают или первый (в случае True), или второй (False). Оператор If просто вызывает их с нужными ветками:

> (If True "first" "second")
"first"
> (If False "first" "second")
"second" 

Но это еще не все. Мы привыкли проверять несколько условий одновременно. Поэтому нужно расширить нашу булевую логику и ввести операторы (снова подсматриваем в Википедию). Функции не сложные. Пишем:

(define (And p q) (p q p))
(define (Or p q) (p p q))
(define (Not p) (p False True))

Тут все просто: And функция в случае успешного прохождения первого условия, проверяет второе; Or в случае успешной проверки возвращает себя, в случае неуспешной проверяет второе значение; Not меняет предикаты местами. Обязательно проверяем:

> (If (And True False) "first" "second")
"second"
> (If (And True True) "first" "second")
"first"
> (If (Or False True) "first" "second")
"first"
> (If (Or False False) "first" "second")
"second"
> (If (Or False (Not False)) "first" "second")
"first"

Все, можно считать себя знатоками лямбда исчисления. Но мы на этом не остановимся. Тут стоит отметить, что я буду использовать привычные нам типы для простоты. Дальше, когда у нас будет достаточно своих типов, мы будем оперировать с ними. Пока будем использовать строки и числа для иллюстрации.

Натуральные числа

Натуральные числа – это числа, которые используются для счета. Мы с вами используем арабские цифры и десятичную систему счисления. Но на самом деле натуральные числа сами по себе являются очень интересной абстракцией и часто приводятся как пример использования алгебраических типов данных.

Для представления чисел мы реализуем так называемые Church numerals (цифры Чёрча). Числом в такой кодировке является функция, которая принимает текущее значение и функцию роста. Например в случае с обычной арифметикой это могут быть 3 и +1. В конечном итоге, применив к начальному значению функцию роста N раз, получим натуральное число, которое его представляет. Я не хочу использовать для описания обычную арифметику. Дальше покажу почему.

Мы уже достаточно подковались в техническом плане. Пора приступить к реализации. Для иллюстрации будем использовать привычные для нас представления натуральных чисел: арабские цифры и строки. Для чисел функцией роста будет функция, которая складывает число с единицей (PlusOne), для строк – функция конкатенации с другой строкой, где в роли другой строки у нас будут палочки "|", как в школе (Concat):

(define (Nil f x) x)
(define (One f x) (f x))
(define (Two f x) (f (f x)))

(define (PlusOne x) (+ 1 x))
(define (Concat x) (string-append x "|"))

Тут становится понятно, почему я преднамеренно уклонялся от использования цифр при описании натуральных чисел. Это потому, что цифры Чёрча являются самодостаточными значениями. Если вы попробуете в интерпретаторе ввести 'Two', вы увидите, что интерпретатор возвращает лямбду #<procedure:Two>. Но, если вы не хотите определять руками все множество натуральных чисел, но хотите получить визуальное представление натурального числа, нужно ему передать в параметрах функцию увеличения значения и начальное значение. Доказательством для этого служит наш интерпретатор:

> Two
#<procedure:Two>
> (Two Concat "")
"||"
> (Two PlusOne 0)
2

Мы объявили 3 натуральных числа, в которых выполнение функции вложены друг в друга. Но было бы неплохо использовать например число 99, что бы определить 100, а не писать сто вложенных вызовов функций. В этом случае нам спешат на помощь функции следующего и предыдущего элементов. Реализовываем функции и сразу же перепишем наши числа:

(define (Succ n f x) (f (n f x)))
(define (Pred n f x) ((n (lambda (g) (lambda (h) (h (g f)))) (lambda (u) x)) (lambda (u) u)))

(define (Null f x) x)
(define (One f x) (Succ Null f x)) 
(define (Two f x) (Succ One f x))
(define (Three f x) (Succ Two f x))
(define (Four f x) (Succ Three f x))
(define (Five f x) (Succ Four f x)) 

Функция увеличения числа довольно проста, а вот уменьшения – сложнее. Для следующего по порядку числа мы просто оборачиваем исходное еще одним вызовом функции. Для взятия предшественника используется функция, которая пропускает первое применение функции роста в цепочке применения функции f.

Очевидно, что в лямбда-исчислении должны существовать арифметические операции с натуральными числами, иначе это были бы не числа совсем. Смотрим страницу Википедии и переписываем:

(define (Plus m n) (lambda (f x) (m f (n f x))))
(define (Minus m n) (lambda (f x) ((n (lambda (t) (lambda (r s) (Pred t r s))) m) f x)))
(define (MinusC m n) (lambda (f x) ((n (lambda (t) (curry Pred t)) m) f x)))
(define (Mul m n) (lambda (f x) (m (lambda (y) (n f y)) x)))
(define (IsZero n) (n (lambda (x) False) True))
(define (Eq m n) (IsZero (Minus m n)))

Plus применяет функцию сначала n раз, потом еще m. Minus применяет функцию предыдущего элемента к уменьшаемому числу (можно использовать каррирование, что бы получить более читаемую запись: MinusC). Функция умножения m раз повторяет n применений функции. Проверка на нуль: как известно IsZero возвращает свой аргумент не применяя функции, значит получим True, а все числа больше игнорируют свой аргумент и возвращают False. Проверка на равенство делает вычитание и проверяет на ноль (поскольку у нас нету отрицательных чисел, нужно в другую сторону тоже проверять). Деление и возведение в степень тоже есть, но мы их реализовывать не будем. Они есть на странице, попробуйте написать сами. Теперь с помощью операций мы можем определить числа побольше: десятки и сотни:

(define (Ten f x) (Mul Five Two))
(define (Hundred f x) (Mul Ten Ten))

И нарисуем сто палочек:

> (Hundred Concat "")
"||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||"
> ((Plus Two (Mul Four Ten)) PlusOne 0)
42
> (IsZero Null)
#<procedure:True>
> (IsZero Two)
#<procedure:False>
> (Eq Two Two)
#<procedure:True>
> (Eq Two One)
#<procedure:False>

Пара

Продолжим парой значений. В лямбда-исчислении пара – это функция, которая замыкает два аргумента и «ждет» функцию, которую потом может применить к этим значениями. Очевидными кандидатами на такие функции есть взятие первого или второго элемента:

(define (Pair a b) (lambda (f) (f a b)))
(define (First p) (p (lambda (a b) a)))
(define (Second p) (p (lambda (a b) b)))

Функции доступа к элементу принимают пару и «скармливают» им лямбду, которая возвращает соответственно первый или второй аргумент. Проверяем:

> (First (Pair "first" "second"))
"first"
> (Second (Pair "first" "second"))
"second" 

С помощью пары мы можем реализовать много абстракций: например списки и кортежи.

Списки

Списки – самая часто используемая и часто изучаемая коллекция в функциональном программировании. В уже упомянутой книжке SICP, списки рассмотрены очень подробно. Собственно сам «LISP» расшифровывается как List Processing Language. Поэтому к ним мы подойдем со всей ответственностью и энтузиазмом. В интернете часто можно наткнуться на описание списков в стиле лямбда-исчисления.

Собственно, список – это не что иное как пара значений (пары у нас уже есть): головной элемент и хвост, он же продолжение списка. На Википедии описаны 3 способа кодирования списков:

• с использование пары как элемента. Это позволяет хранить первым элементом пары индикатор того, что список пустой. Это вариант хорош тем, что функция с элементами очень простая – в зависимости от индикатора пустоты можно исполнять первую или вторую функцию;
• с использование одного элемента, а в пустом списке хранить false. В этом случает представление списка имеет более короткую записи, но работа немного сложнее, чем в первом случае;
• определять список с помощью функции правой свертки. Нам он не подходит, потому что сложный.

Мы выберем первый вариант, так он является наиболее наглядным. Для вывода элементов списка используем Лисп-функцию 'display', которая выводит свой аргумент в терминал. Дополнительно определим функцию вывода для чисел и палочек. Напомню, что каждый элемент списка у нас является еще одно парой, где первый элемент True если список пустой и False если содержит значимый элемент. Переписываем:

(define (NatToNumber m) (display (m PlusOne 0)))
(define (NatToString m) (display (m Concat "")))
; ...
(define (Nil) (Pair True True))
(define (IsNil) First)
(define (Cons h t) (Pair False (Pair h t)))
(define (Head l) (First (Second l)))
(define (Tail l) (Second (Second l)))

(define (ProcessList l f) ((If (IsNil l) (lambda ()(void)) (lambda ()(f (Head l))))))
(define (ConsZeroList n) (n (lambda (l) (Cons Null l)) (Nil)))
(define (ConsRangeList n) (Second (n 
                                  (lambda (p) (Pair (Minus (First p) One) (Cons (First p) (Second p))))
                                  (Pair n (Nil)))))

Пока мы не умеем итерироваться по списку, потому что не знаем как сделать рекурсию. Поэтому все что нам остается – вручную перебирать элементы и работать с ними. Функция ProcessList применяет к текущему головному элементу переданную функцию-аргумент, или не делает ничего, если список пустой. Тут стоит заметить, что в лямбда-исчислении используется normal order. Это означает, что функции сначала оборачивают свои аргументы, а потом исполняются. В Лиспе же используется applicative order – аргументы функции вычисляются до того, как быть переданным. В теле функции ProcessList при проверке с If мы не хотим выполнять обе ветки одновременно, поэтому придется передавать в ветки исполнения лямбды и вызывать ту, которая возвращается после проверки. ConsZeroList создает список из нулей требуемый длинны, а ConsRangeList создает список из последовательности чисел. Они основаны на многократном применении натуральным числом функции над элементом. Проверяем в интерпретаторе:

> (define L1 (Cons One (Cons Two (Cons Three (Nil)))))
> (ProcessList L1 NatToNumber)
1
> (ProcessList (Tail (Tail L1)) NatToNumber)
3
> (ProcessList (Tail (Tail (Tail L1))) NatToNumber)
>

Y-combinator

Итак, мы достигли апогея нашей статьи. Для того, что бы обрабатывать весь список, нам нужно итерироваться по нему. В данный момент мы не знаем как это сделать. А это можно сделать используя Y-combinator, он же Fixed-point combinator, он же комбинатор неподвижной точки. Что бы понять, почему он так называется, нужно читать много текста. Нам достаточно знать то, что если ему передать функцию, первым аргументом функции он передаст саму же себя. С помощью этого мы сможем рекурсивно выполнять операции на объектами (например списками).

Y-комбинатор очень хорошо объяснен в статье Майка Венье. В Википедии есть точное определение комбинатора. В вышеупомянутой статье есть код на Лиспе. Нам нужна функция для applicative order. Просто переписываем. Там же подсмотрим функцию вычисления факториала, которую мы можем переписать под наши натуральные числа:

(define (Y f) ((lambda (x) (x x)) (lambda (x) (f (lambda (y) ((x x) y))))))

(define (Fac n)
  ((Y 
    (lambda (f)
      (lambda (m)
        ((If (Eq m Null) (lambda () One)
          (lambda () (Mul m (f (Minus m One))))))))) n))

Проверим результат. Факториал десяти, в следствии того, что наша функция создает почти 4 миллиона лямбд, а потом их выполняет, вычисляется довольно долго:

> (NatToNumber (Fac Five))
120
> (NatToNumber (Fac Ten))
3628800

Теперь возьмемся за списки. С помощью Y-комбинатора, реализуем всеми любимую троицу функций для обработки списков: Map, Filter, Reduce; и функцию для вывода:

;Lists
(define (PrintList l)
  (display "[")
  ((Y 
    (lambda (r)
      (lambda (m)
        ((If (IsNil m)
          void
          (lambda () 
            (NatToNumber (Head m))
            (display ", ")
            (r (Tail m)))))))) l)
  (display "]"))

(define (Map l f)
  ((Y 
    (lambda (r)
      (lambda (m)
        ((If (IsNil m)
          Nil
          (lambda () (Cons (f (Head m)) (r (Tail m))))))))) l))

(define (Filter l f)
  ((Y 
    (lambda (r)
      (lambda (m)
        ((If (IsNil m) Nil
          (lambda ()
            ((If (f (Head m))
              (lambda () (Cons (Head m) (r (Tail m) f)))
              (lambda () (r (Tail m) f)))))))))) l))

(define (Reduce l f z)
  ((Y 
    (lambda (r)
      (lambda (m)
        ((If (IsNil m) z
          (lambda () (f (Head m) (r (Tail m) f z)))))))) l))

Реализация этих функций описана во многих статья, поэтому я о них не буду много рассказывать. Лучше применим их на практике:

> (PrintList (ConsRangeList Ten))
[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, ]
> (PrintList (Map (ConsRangeList Ten) (lambda (x) (Plus x One))))
[2, 3, 4, 5, 6, 7, 8, 9, 10, 11, ]
> (PrintList (ConsZeroList Ten))
[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ]
> (PrintList (Map (ConsZeroList Ten) (lambda (x) (Plus x Hundred))))
[100, 100, 100, 100, 100, 100, 100, 100, 100, 100, ]
> (PrintList (Filter (ConsRangeList Ten) (lambda (x) (Not (Eq x Five)))))
[1, 2, 3, 4, 6, 7, 8, 9, 10, ]
> (NatToNumber (Reduce (ConsRangeList Ten) (lambda (x y) (Plus x y)) Null))
55
> (NatToNumber (Reduce (ConsZeroList Ten) (lambda (x y) (Plus x y)) Null))
0

Эпилог

Вот так, используя одни только функции мы смогли реализовать все, что нужно обычному функциональщику для программирования. Надеюсь что материал понравился. Лямбда исчисление заслуживает того, что бы хотя бы с ним ознакомиться. Вот уже 30 лет функциональным языкам пророчат убийство ООП и императивных языков. Но сегодня все больше создается мультипарадигменных языком программирования. Возможно поэтому Хаскелль так и не стал широко распространенным.

Тем не менее, математическая красота заложенная в лямбда исчисление еще много десятилетий будет привлекать программистов всех специальностей.

Весь код можно посмотреть/скачать на гитхабе.

UPD: В комментариях mapron вспомнил похожую публикацию с кодом на Javascript.