Текст:Эрик Мейер:ФП при помощи бананов, линз, конвертов и колючей проволоки

Мы разработали исчисление для ленивого функционального программирования, которое основано на операторах рекурсии, связанных с определениями типов данных. Для этих операторов мы вывели несколько алгебраических законов, которые полезны в деле трансформации программ. Мы покажем, что все функции из статьи Бёрда (Bird) и Уодлера (Wadler) «Введение в функциональное программирование» могут быть выражены через эти операторы.

Введение

В ряду многих стилей и методологий разработки программ стиль «Squiggol», по нашему мнению, заслуживает внимания со стороны сообщества функционального программирования. Общая цель Squiggol'а заключается в вычислении программ по их спецификациям таким же образом, как математик вычисляет решение дифференциальных уравнений или использует арифметику для решения числовых задач.

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

Эта философия похожа на методологию структурного программирования для императивного программирования. Использование оператора goto запрещено в целях поддержки структурированности потока управления при помощи таких примитивов, как условные выражения и циклы, которые заменяют фиксированные применения оператора goto, что позволяет программам быть выполнимыми и даже элегантными. Для функционального программирования подобный вопрос заключается в выборе схемы рекурсии в качестве базиса для исчисления программ. Мы предложим несколько операторов рекурсии, которые естественно ассоциируются с определениями алгебраических типов данных. Далее доказывается некоторое количество общих теорем об этих операторах, что далее используется для трансформации программ и доказательства корректности этого процесса.

Бёрд (Bird) и Меертенс (Meertens) [4, 18] идентифицировали некоторые правила для нескольких определённых типов данных (наиболее известные — конечные списки), которые они потом использовали для вычисления решения для нескольких проблем программирования. При помощи внедрения исчисления в теорию категорий работу Бёрда и Меертенса можно обобщить для произвольных, индуктивно определённых алгебраических типов данных [17, 12]. Некоторое время назад рабочая группа Бэкхауза (Backhouse) [1] расширила исчисление на родственные системы взглядов, достигнув тем самым покрытия недетерминизма.

Независимо Патерсон (Paterson) [21] разработал исчисление для функциональных программ, схожее по содержанию, но очень отличающееся по форме (как многие австралийские живтоные) с работами, указанными ранее. Но на самом деле, если кто-нибудь «проберётся» через синтаксические различия, он увидит, что правила, выведенные Патерсоном, являются теми же и иногда более общими, нежели те, что используются адептами Squiggol'а.

Эта работа предлагает расширение теории в контексте ленивого функционального программирования, т. е. для нас нас тип является ω-cpo, и мы рассматриваем только непрерывные отображения между типами (другими словами, мы работаем с категорией CPO). Работа с категорией SET, как сделали, для примера, Малькольм (Malcolm) [17] и Хагино (Hagino) [14], обозначает, что конечные типы данных (определённые в виде начальных алгебр) и бесконечные типы данных (определённые как терминальные коалгебры) составляют два различных «мира». В этом случае невозможно определить по индукции такие функции (катаморфизмы), которые были бы применимы и для конечных типов, и для бесконечных, а потому произвольно рекурсивные определения недопустимы. Работа в категории CPO позволяет заключить, что носители начальных алгебр и терминальных коалгебр совпадают, и что в этом случае единый тип данных можно использовать и для конечных, и для бесконечных структур. Цена, которую необходимо заплатить за такое удобство, заключается в том, что и функции, и значения становятся неизбежными.

Тип «список»

Мы проиллюстрируем шаблоны рекурсии на примере специфического типа данных, называемого «списком» (основанном на префиксации). Таким образом, определения в этом разделе являются конкретизацией тех общих определений, которые будут даны в четвёртом разделе. Современные языки программирования позволяют определить списки над элементами типа $A$ примерно следующим образом:

$A* ::= Nil | Cons (A || A*)$

Рекурсивная структура этого определения применяется в тех случаях, когда создаются функции с типом $A* \rightarrow B$, разрушающие список; такие функции называются катаморфизмами (от греческого предлога κατα, обозначающего «вниз», как в слове «катастрофа»). Анаморфизмами называются функции с типом $B \rightarrow A*$ (от греческого предлога ανα, обозначающего «наверх», как в слове «анаболизм»), такие функции генерируют список $A*$ из начального значения типа $B$. Функции типа $A \rightarrow B$, дерево вызовов для которых похоже на сами списки, называются хиломорфизмами (из философии Аристотеля, где слово υλοσ обозначает «пыль» или «материя»).

Катаморфизмы

Пусть $b \in B$ и $\oplus \in A||B \rightarrow B$, в этом случае катаморфизм для списка есть функция $h \in A* \rightarrow B$ следующего вида:

• $h Nil = b$
• $h (Cons (a, as)) = a \oplus (h as)$

В нотации Бёрда и Уодлера [5] эта функция будет записана как $h = foldr b (\oplus)$. Мы записываем катаморфизмы при помощи заключения соответствующих компонентов в т. н. бабановые скобки:

$h = (|b, \oplus|)$

Алгебраические типы данных

Схемы рекурсии

Параметризованные типы