Мой перевод статьи Bartosz Milewski “Understanding F-Algebras” на schoolofhaskell.

Что такое алгебра? Говоря наивно, алебра – это такая штука, которая даёт нам возможность производить вычисления с числами и символами. Абстрактная алгебра представляет символы как элементы векторного пространства: они могут умножаться на скаляры и складываться друг с другом. Но что отделяет алгебры от линейных пространств, так это наличие векторного умножения: билинейного произведения векторов, рузультатом которого является другой вектор (против скалярного произведения, которое даёт скаляр). Комплексные числа, например, могут быть описаниы как 2-мерные векторы, чьи компоненты суть действительная и мнимая часть соответственно.

Однако, ничего не подведёт вас к следующему определению F-алгебры из пакета Control.Functor.Algebra для Haskell:

type Algebra f a = f a -> a

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

Существенность Алгебры⌗

Существует два по-настоящему существенных аспекта алгебры:

  1. Возможность формировать выражения и
  2. Возможность вычислять эти выражения

Существенность Выражения⌗

Стандартный способ генерации выражений – это использовать грамматики. Вот пример грамматики на Haskell:

data Expr = Const Int
          | Add Expr Expr
          | Mul Expr Expr

Как и большинство нетривиальных грамматик, грамматика выше определена рекурсивно. Вы можете думать об Expr как о самоподобном фрактале. Expr как тип содержит не только Const Int, но также Add и Mult, которые в свою очередь содержат другие Expr-ы, и т.д. Деревья, на всю глубину.

1. The fractal nature of an expression type

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

Поскольку мы имеем дело с типами, тои и определить нам надо функцию от типа, иначе известную как конструктор типа. Вот нерекурсивный прототип нашей грамматики (позже вы увидите, что за буквой F в ExprF скрывается функтор):

ExprF a = Const Int
        | Add a a
        | Mul a a

Наша фрактально-рекурсивная структура Expr может быть сгенерирована последовательным применением ExprF к сомому себе, как в ExprF (ExprF (ExprF a))), и т.д. Чем больше мы применяем, тем более глубокие деревья мы можем генерировать. После бесконечного числа итераций мы должны дойти до некоторой неподвижной точки, после которой последующие применения уже не будут иметь смысла. То есть применение ExprF ещё раз не изменит ничего – неподвижная точка не двигается под преобразованием ExprF. Это как добавление единицы к бесконечности: вы получаете назад бесконечность.

В Haskell мы можем выразить неподвижную точку конструктора типов f (т.е. функции от типа f – прим. перев.) как тип:

newtype Fix f = Fx (f (Fix f))

Если вы внимательно посмотрите на эту формулу, то увидите, что она отражает именно то, о чём я говорю: Fix f это тип, который получается применением f к самому себе. Это фикспоинт, неподвижная точка для f. (В литературе иногда можно встретить Fix под именем Mu, мю.)

Нам нужен лишь один универсальный рекурсивный тип, Fix, чтобы штамповать другие рукурсивные типы из (не рекурсивных) конструкторов типов.

Про конструктор значений (правая часть уравнения, против конструктора типа в левой, – прим. перев.) Fix можно заметить следующую штуку: об Fx можно думать как о функции, которая берёт аргумент типа f (Fix f) и производит Fix f:

Fx :: f (Fix f) -> Fix f

Мы используем эту функцию позже.

Теперь мы можем переопределить Expr как неподвижную точку функции ExprF:

type Expr = Fix ExprF

Вы можете задаться вопросом: существуют ли вообще какие-нибудь значения типа Fix ExprF? Населён ли данный тип? Это хороший вопрос, и ответ на него – да, потому что есть один конструктор ExprF, которые не зависит от a. Этот конструктор – Const Int. Мы можем “раскрутиться”, поскольку мы всегда можем создать лист дерева Expr, например так:

val :: Fix ExprF
val = Fx (Const 12)

После того, как мы получили данную возможность, мы можем создавать всё более и более сложные значения, используя два других констркутора ExprF:

testExpr = Fx $ (Fx $ (Fx $ Const 2) `Add` 
                (Fx $ Const 3)) `Mul` (Fx $ Const 4)

Сущность Вычисления⌗

Вычисление – это рецепт извлечения одного значения из некоторого выражения. Для того, чтобы вычислять рекурсивно определённые выражения, вычисление должно также производиться рекурсивно.

Повторимся, что рекурсия может быть обобщена – всё что нам надо это вычислительная стратегия для каждой toplevel-конструкции (сгенеренной, в частности, ExprF) и способ вычисления её (конструкции) детей. Давайте назовём такой нерекурсивный вычислитель (evaluator) именем alg, а рекурсивный (для вычисления детей) именем eval. Оба alg и eval возвращают значения одного и того-же типа a.

Для начала нам нужно уметь мапить (map) eval поверх детей выражения. Кто-то упомянул маппинг? Это значит, что нам нужен функтор!

Действительно, довольно легко убедить себя в том, что наш ExprF – это функтор:

instance Functor ExprF where
    fmap eval (Const i) = Const i
    fmap eval (left `Add` right) = (eval left) `Add` (eval right)
    fmap eval (left `Mul` right) = (eval left) `Mul` (eval right)

F-алгебра строится над функтором – над любым функтором. (Строго говоря, над эндофунктором: т.е. над функтором, отображающим данную категорию в саму себя – в наших примерах такой категорией предстаёт Hask – категория всех типов языка Haskell).

Теперь предположим, что мы знаем, как вычислять всех детей Add и Mul в Expr, получая на выходе значения некоторого типа a. Всё, что остаётся вычислить теперь – это (Add a a) и (Mul a a) в ExprF a. (Нам надо также уметь вычислить Const Int, но это уже не связано с рекурсией.)

Вот вам пример такого вычислителя, который порождает значения типа Int:

alg :: ExprF Int -> Int

alg (Const i)   = i
alg (x `Add` y) = x + y
alg (x `Mul` y) = x * y

(Заметьте, что мы вольны складывать и перемножать x и y, поскольку это обычные Int-ы)

Во что я сделал тут: я выбрал определённый тип, Int, в качестве цели моего вычисления. Такой тип называется типом-носителем данной алгебры. А затем определил функцию alg из образа Int (под действием отображения функтором ExprF) обратно в Int.

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

alg' :: ExprF String -> String

alg' (Const i)   = [chr (ord 'a' + i)]
alg' (x `Add` y) = x ++ y
alg' (x `Mul` y) = concat [[a, b] | a <- x, b <- y]

F-Algebras⌗

Мы теперь готовы определить F-алгебру в самых общих терминах. Сперва я использую язык теории категорий, а затем сразу же переведу определение на Haskell.

F-алгебра состоит из:

  1. эндофунктора F в категории C,
  2. объекта A в этой категории, и
  3. морфизма из F(A) в A.

F-алгебра в Haskell определяется функтором f, типом-носителем a и функцией из (f a) в a. (Соответствующая категория – Hask)

Аккурат сейчас определение, которым я начал этот пост, должно начать обретать смысл:

type Algebra f a = f a -> a

Для данного функтора f и типа-носителя a алгебра определяется указанием всего-лишь одной функции. Часто саму эту функцию называют алгеброй, отсюда и выбор имени alg в примерах выше.

Возвращаясь к нашему конкретному примеру: функтор это ExprF, тип-носитель это Int, а функция это alg:

-- Пример простой алгебры
type SimpleA = Algebra ExprF Int

alg :: SimpleA
alg (Const i)   = i
alg (x `Add` y) = x + y
alg (x `Mul` y) = x * y

Единственное, чего всё ещё не хватает, это определение функции eval, которая позаботиться о вычислении детей выражения. Выясняется, что эта функция может быть определена в очень общей форме. Чтобы сделать это, нам надо ознакомиться с понятием инициальной алгебры (initial algebra).

Инициальные Алгебры⌗

Существует много алгебр, основанных на данном функторе (я пока показал вам две). Но есть одна алгебра, которая рулит ими всеми – это инициальная алгебра. На самом деле, вы уже видели её части. Помните Fix, функцию от типа?

newtype Fix f = Fx (f (Fix f))

Для любого функтора f она определяет уникальный тип Fix f. Теперь мы “раскрутим” сами себя. Мы используем этот тип как носитель в определении другой алгебры. Выяснится, что эта алгебра окажется нашей инициальной алгеброй.

Для начала, вернёмся к нашему примеру и вместо Int или String используем (Fix ExprF) в качестве типа-носителя:

type ExprInitAlg = Algebra ExprF (Fix ExprF)

У нас есть функтор и тип-носитель. Для полного комплекта нам нужна функция со следующей сигнатурой:

ex_init_alg :: ExprF (Fix ExprF) -> Fix ExprF

Прикиньте, у нас уже есть функция такого типа. Это конструктор Fix:

ex_init_alg = Fx

(Замените f на ExprF в определении Fix, чтобы увидеть, как подходят сигнатуры)

Но стойте! Что вообще вычисляет этот “вычислитель?” Для аргумента (ExprF Expr) он выдаёт Expr. В частности, при данном

Add (Fx $ Const 2) (Fx $ Const 3)

он выдаст Expr:

Fx $ Add (Fx $ Const 2) (Fx $ Const 3)

Данный вычислитель ничего не редуцирует, как это делали другие наши вычислители. Он не вносит потери (is not lossy) в структуру. Он сохраняет всю информацию, поданную на вход. С другой стороны, все другие вычислители потенциально теряют некоторую часть информации. Они возвращают некий “summary”, некое резюме, дайджест информации, закодированной в данной структуре данных. В этом смысле алгебра, которую мы только что определили, обладает по меньшей мере такой-же “силой”, как и все другие мыслимые алгебры над данным функтором. Поэтому она и называется инициальной алгеброй.

Слово инциальный имеет особое значение в теории категорий. Инициальная алгебра имеет следующее свойство: существует (уникальный) гомоморфизм из неё в любую другую алгебру над тем же функтором.

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

На самом деле, гомоморфизм алгебр полностью описывается функцией, которая отображает один носитель в другой и при этом обладает определённым свойством. Поскольку носитель инициальной алгебры суть Fix f, нам нужна функция:

g :: Fix f -> a

где a это носитель для той другой алгебры. В той алгебре есть вычислитель alg с такой сигнатурой:

alg :: f a -> a

2. Гомоморфизм из инициальной алгебры в некоторую алгебру

То свойство, которым должна обладать g таково: не должно быть разницы, используем ли мы вычислитель инициальной алгебры и затем применим g, или же сначала применим g (с помощью fmap), а затем вычислитель той второй алгебрыб alg. Давайте проверим типы, чтобы убедить себя в осмысленности данного требования.

Первый вычислитель использует Fx чтобы добраться из f (Fix f) в Fix f. Потом g переносит Fix f в a.

Альтернативный путь использует gmap g чтобы замапить f (Fix f) в f a, за чем следует стрелка alg из f a в a. Заметьте, что это первый раз, когда мы воспользовались функториальными свойствами f. Они позволили нам втянуть (lift) функцию g в fmap g.

Ключевое наблюдение заключается в том, что Fx – это трансформация “без потерь” (loseless) и может быть легко обращена, инвертирована. Обратный элемент для Fx это unFix:

unFix :: Fix f -> f (Fix f)
unFix (Fx x) = x

После одного разворота стрелки Fx (это unFix) легко видеть, как прохождение по маршруту g суть то же самое, что и “окольный путь” через unFix, fmap g, и, следом, alg:

3. Определение катаморфизма

g = alg . (fmap g) . unFix

Мы можем использовать данное уравнение для рекурсивного определения g. Мы знаем, что данное определение сходится, поскольку применение g через fmap имеет дело с поддеревьями исходного дерева, а они строго меньше исходного дерева.

Мы можем обобщить вычисление ещё сильнее, “вынеся за скобки” зависимость от alg (положив g = cata alg):

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unFix

Результатом является очень общая функция, называемая катаморфизмом. Мы построили катаморфизм из алгебры чтобы доказать, что неподвижная точка функтора этой алгебры есть инициальная алгебра. Постойте, не создали ли мы только что рекурсивный вычислитель, который искали?

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

Взглянем снова на сигнатуру катаморфизма, добавив в неё (избыточные) скобки:

cata :: Functor f => (f a -> a) -> (Fix f -> a)

Штуковина берёт некоторую алгебру, то есть нерекурсивную функцию f a -> a, и возвращает функцию-вычислитель, (Fix f -> a). Этот вычислитель берёт выражение с типом Fix f и “вычисляет” (evaluates) его всё в тип a. Катаморфизм позволяет нам вычислять сколь угодно вложенные друг в друга выражения!

Давайте опробуем его с нашим простым функтором ExprF, который мы использовали для генерации вложенных выражений типа Fix ExprF.

Мы уже определили alg для него:

type SimpleA = Algebra ExprF Int

alg :: SimpleA
alg (Const i)   = i
alg (x `Add` y) = x + y
alg (x `Mul` y) = x * y

Итак, наш полностью завершённый вычислитель – это просто:

eval :: Fix ExprF -> Int
-- eval = cata alg = alg . fmap (cata alg) . unFix
eval = alg . fmap eval . unFix

Проанализурем его: для начала, unFix позволяет нам подсмотреть в top level входного выражения: это либо лист Const i, либо Add или Mul, дети которых снова суть полноправные выражения, пускай и одним уровнем выше к поверхности (shallow). Мы вычисляем детей, рекурсивно применяя к ним eval. На выходе получаем дерево единичной высоты, чьи листья теперь полностью вычислены в Int-ы. Это позволяет нам применить alg и получить результат.

Вы можете протестить это на простом выражении:

testExpr = Fx $ (Fx $ (Fx $ Const 2) `Add` 
                (Fx $ Const 3)) `Mul` (Fx $ Const 4)

{-# LANGUAGE DeriveFunctor #-}
data ExprF r = Const Int
             | Add r r
             | Mul r r
    deriving Functor

newtype Fix f = Fx (f (Fix f))
unFix :: Fix f -> f (Fix f)
unFix (Fx x) = x

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unFix

alg :: ExprF Int -> Int
alg (Const i)   = i
alg (x `Add` y) = x + y
alg (x `Mul` y) = x * y

eval :: Fix ExprF -> Int
eval = cata alg
-- show
testExpr = Fx $ 
             (Fx $ (Fx $ Const 2) `Add` (Fx $ Const 3)) `Mul` 
             (Fx $ Const 4)

main = print $ eval $ testExpr

foldr⌗

Обойти (traverse) и вычислить рекурсивную структуру данных? Не это ли делает foldr для списков?

Именно! Довольно просто создать алгебру для списков. Мы начинаем с функтора:

data ListF a b = Nil | Cons a b

instance Functor (ListF a) where
    fmap f Nil = Nil
    fmap f (Cons e x) = Cons e (f x)

Первый аргумент к ListF– это тип нашего элемента, второй – это тип, в который му будем осуществлять рекурсию.

Вот вам простая алгебра с типом-носителем Int:

algSum :: ListF Int Int -> Int
algSum Nil = 0
algSum (Cons e acc) = e + acc

Используя конструктор Fx, мы можем рекурсивно генерировать какие угодно списки:

lst :: Fix (ListF Int)
lst = Fx $ Cons 2 (Fx $ Cons 3 (Fx $ Cons 4 (Fx Nil)))

Наконец, мы можем вычислить наш список, используя наш универсальный катаморфизм:

cata algSum lst

Разумеется, мы может делать в точности то же с традиционным списками и foldr:

foldr (\e acc -> e + acc) 0 [2..4]

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

Вот полный пример со списками:

newtype Fix f = Fx (f (Fix f))

unFix :: Fix f -> f (Fix f)
unFix (Fx x) = x

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unFix
-- show
data ListF a b = Nil | Cons a b

instance Functor (ListF a) where
    fmap f Nil = Nil
    fmap f (Cons e x) = Cons e (f x)

algSum :: ListF Int Int -> Int
algSum Nil = 0
algSum (Cons e acc) = e + acc

lst :: Fix (ListF Int)
lst = Fx $ Cons 2 (Fx $ Cons 3 (Fx $ Cons 4 (Fx Nil)))

main = do
    print $ (cata algSum) lst
    print $ foldr (\e acc -> e + acc) 0 [2, 3, 4]

Выводы⌗

Вот главные поинты этого поста:

  1. Так-же как рекурсивные функции определяются неподвижными точками обычных функций, рекурсивные (вложенные) структуры данных определяются как неподвижные точки обычных конструкторов типов.
  2. Функторы суть интересные конструкторы типов, потому что они порождают вложенные структуры данных, которые поддерживают рекурсивное вычисление (обобщённая свёртка, generalized folding).
  3. Некоторая F-алгебра определяется функтором f, типом-носителем a и функцией из f a в a.
  4. Существует одна инициальная алгебра, которая отображается во все алгебры над данным функтором. Тип-носитель этой алгебры – это неподвижная точка этого функтора.
  5. Единственный маппинг между инициальной алгеброй и любой другой алгеброй над тем-же самым функтором генерируется катаморфизмом.
  6. Катаморфизм берёт простую алгебру и создаёт рекурсивный вычислитель для вложенной структуры данных (неподвижную точку данного функтора). Катаморфизм – это обобщение операции свёртки списков на любые другие рекурсивные структуры данных.

Благодарности⌗

Я благодарен Gabriel Gonzales за ревью этого поста. Габриэль сделал одно интересное наблюдение:

“В самом деле, даже в Haskell рекурсия не является полностью “first class”, поскольку компилятор ужасно оптимизирует рекурсивный код. Вот почему F-алгебры и F-коалгебры вездесущи в высокопроиводительных Haskell-библиотеках вроде vector, потому что они трансформируют рекурсивный код в нерекурсивный, а компилятор замечательно оптимизирует нерекурсивный код.”

Библиография⌗

Большинство примеров в моём посте были взяты из двух публикаций ниже:

  1. Fixing GADTs by Tim Philip Williams.
  2. Advanced Functional Programming, Tim Sheard’s course notes.
  3. Functional Programming with Bananas, Lenses, Envelopes, and Barbed Wire by Erik Meijer, Maarten Fokkinga, and Ross Paterson.
  4. Recursive types for free! by Philip Wadler
  5. Catamorphisms in Haskell Wiki

Примечания переводчика⌗

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