Current mood:	geeky
Current music:	muse
Entry tags:	book, functional programming, plt

SPJ "The implementation of functional programming languages"
Сегодня, просматривая свою коллекцию книжек и paper-ов по функциональному программированию, решил посмотреть, что там пишет Simon L. Peyton Jones в своей книге "The implementation of functional programming languages". И был приятно удивлён - как же классно он пишет! Хотел всего лишь прочесть вступление и зачитался! :) Меньше чем за 30 первых страниц книги получаем чёткое, сжатое, понятное и хорошо иллюстрированное описание таких тем:

• синтаксис лямбда-исчисления (в дальнейшем ЛИ)


• карринг


• операционная семантика ЛИ


• бета-редукция, альфа- и эта-преобразования и что они значат


• порядок редукции, его оптимальность


• нормальный порядок редукции


• теоремы Чёрча-Россера


• пример выражения, у которого нет нормальной формы


• как выражать рекурсивные функции в ЛИ


• Y-комбинатор


• денотационная семантика ЛИ, отличие денотационной семантики от операционной


• bottom _|_


• строгость и ленивость функций

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

В качестве анонса попробую написать свой вольный пересказ/перевод вступления к книге.

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

А теперь подробнее.

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

1. Преобразование программы из функционального языка высокого уровня в промежуточный язык, базирующийся на ЛИ.
2. Имплементация промежуточного языка.

После описанного в начале поста обзора классического лямбда-исчисления вводится некое надмножество ЛИ (enriched lambda calculus), которое облегчает трансляцию в него языков высокого уровня.
Оставшиеся главы первой части книги раскрывают такие аспекты преобразования в промежуточный код:

• трансляция простых программ на Miranda (который является примером языка высокого уровня в книге и в некотором роде одним из прообразов Haskell)


• сопоставление по образцу (pattern matching), его формальная семантика


• эффективная трансляция pattern matching выражений (эта глава, как и некоторые последующие, написана Филипом Вадлером)


• преобразование обогащённого лямбда-исчисления в обычное


• list comprehensions


• проверка типов, полиморфизм


• реализация type-checker-а

Вторая часть.
Вторая и третья части книги посвящены имплементации лямбда-исчисления с помощью техники редукция графов (graph reduction).
Кратко суть этой техники можно описать на примере выполнения простой программы

 f x = (x + 3) * (x - 1) 

Предположим, нам нужно посчитать f 2:

 f 2 = (2 + 3) * (2 - 1) 

Это выражение можно представить в виде дерева:

     *
    / \
   +   -
  / \ / \
 2  3 2  1

применяя последовательно сложение и вычитание (в любом порядке), мы получим такое (редуцированное) дерево:

     *
    / \
   5   1

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

Проведя вышеописанный процесс, можно сделать следующие наблюдения:

1. Выполнение функциональной программы состоит в вычислении выражений.
2. Естественным представлением функциональной программы является дерево (или более обще - граф)
3. Вычисление происходит посредством выполнения последовательных простых шагов называемых редукциями. Каждая редукция представляет собой простое локальное изменение в графе - редукцию графа.
4. Редукции могут проводиться в различном порядке, а также параллельно, поскольку часто они не влияют не взаимодействуют друг с другом.
5. Вычисление считается завершённым, если не осталось выражений, которые могут быть редуцированы.

Техника редукции графов представляет модель выполнения функциональной программы, разительно отличающуюся от модели выполнения в императивных языках.
Эта техника последовательно рассматривается во второй части книги, которая рассказывает о таких темах:

• представление программы в виде графа


• порядок редукций


• собственно проведение редукций


• суперкомбинаторы


• полная ленивость


• SK - комбинаторы (техника альтернативная суперкомбинаторам)


• сборка мусора

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

• концепция и описание G-машины


• различные оптимизации её работы


• анализ строгости


• оценка сложности функциональных программ


• параллельные реализации редукции графов

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