Алгебры и катаморфизмы

[deniok]

Продолжаю вести конспект Bananas in Space (начало здесь).

Краткое содержание первой серии

С помощью аналога fix для типов:

-- конструктор типа
data Rec f = In (f (Rec f))
-- тип конструктора данных
In :: f (Rec f) -> Rec f

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

-- классическая запись рекурсивного типа
data Nat = Z | S Nat

как неподвижные точки функторов

-- добавляем параметр под рекурсию ...
data N c = Z | S c
-- ... делаем функтором ...
instance Functor N where
  fmap g  Z    = Z
  fmap g (S x) = S (g x)
-- ... и получаем альтернативную запись рекурсивного типа Nat
type Nat = Rec N

(Говоря про любые рекурсивные типы, я пока оставляю за скобками экспоненциальные, то есть со стрелками внутри конструктора данных.)


Нотация катаморфизма

Рассмотрим функцию

copy :: Functor f => Rec f -> Rec f
copy (In x) = In (fmap copy x)

Эта функция на самом деле является id. Она проезжает по рекурсивной структуре, заменяя конструктор In на него же. Действительно, на примере выражения In (S (In (S (In Z)))) типа Nat:

copy      (In (S (In (S (In Z))))) ~> по def copy
In (fmap copy (S (In (S (In Z))))) ~> по def fmap
In (S (copy      (In (S (In Z))))) ~> по def copy
In (S (In (fmap copy (S (In Z))))) ~> по def fmap
In (S (In (S (copy      (In Z))))) ~> по def copy
In (S (In (S (In (fmap copy Z))))) ~> по def fmap
In (S (In (S (In (Z)))))

Напишем обобщение copy, которое заменяет In :: f (Rec f) -> Rec f не на себя же, а на произвольную phi :: f a -> a. Получим катаморфизм

cata :: Functor f => (f a -> a) -> Rec f -> a
cata phi (In x) = phi (fmap (cata phi) x)

Для иллюстрации работы cata применим cata phi к In (S (In (S (In Z)))). В правой части определения cata выражение fmap (cata phi) протаскивает (cata phi) через конструктор S, оставляя после себя phi на месте, где стоял In:

cata phi           (In (S (In (S (In Z))))) ~> по def cata
phi (fmap (cata phi)   (S (In (S (In Z))))) ~> по def fmap
phi (S (cata phi          (In (S (In Z))))) ~> по def cata
phi (S (phi (fmap (cata phi)  (S (In Z))))) ~> по def fmap
phi (S (phi (S (cata phi         (In Z))))) ~> по def cata
phi (S (phi (S (phi (fmap (cata phi) Z))))) ~> по def fmap
phi (S (phi (S (phi (Z)))))

Итак видно, что

cata phi (In (S (In (S (In Z))))) = phi (S (phi (S (phi Z))))

то есть cata - это обобщение свёртки списков foldr для произвольного функтора!

Алгебры

Для данных функтора f и типа a функция phi :: f a -> a известна как f-алгебра.

Если в примере с функтором N задать функцию phi, заменяющую Z на 0, а S на succ, то получим N-алгебру типа N Int -> Int

phi_N :: N Int -> Int
phi_N Z     = 0
phi_N (S n) = succ n

Применяя cata к этой алгебре, получим стандартный преобразователь

natToInt :: Nat -> Int -- алиас для Rec N -> Int
natToInt = cata phi_N

Проверяем в GHCi:

*Bis> natToInt (In Z)
0
*Bis> natToInt (In (S (In Z)))
1
*Bis> natToInt (In (S (In (S (In Z)))))
2

При разворачивании определения cata и fmap уйдут и получим естественное рекурсивное

natToInt' :: Nat -> Int
natToInt' (In x) = case x of
                        Z   -> 0
                        S n -> succ (natToInt' n)

Алгебры для Expr и List

Построим ещё алгебры для примеров из прошлой серии.

Если в примере с функтором E задать функцию phi, заменяющую Num на id, а Add на (+),то получим E-алгебру типа E Int -> Int:

phi_E :: E Int -> Int
phi_E (Num n)    = id n
phi_E (Add e e') = e + e'

Применяя cata к этой алгебре, получим стандартный "эвалютор" арифметики

eval :: Expr -> Int -- алиас для Rec E -> Int
eval = cata phi_E

Проверяем в GHCi:

*Bis> eval (In (Num 3))
3
*Bis> eval (In (Add (In (Num 3)) (In (Num 5))))
8
*Bis> eval (In (Add (In (Add (In (Num 3)) (In (Num 5)))) (In (Num 7))))
15

УПРАЖНЕНИЕ: задайте другие E-алгебры, порождающие запись арифметических выражений в префиксной и инфиксной строковой формах.

Если в примере с функтором L a задать функцию phi, заменяющую Nil на [], а Cons на (:), то получим (L a)-алгебру типа L a [a] -> [a]

phi_L :: L a [a] -> [a]
phi_L Nil         = []
phi_L (Cons e es) = e : es

Применяя cata к этой алгебре, получим стандартный преобразователь

listify :: List a -> [a] -- алиас для Rec (L a) -> [a]
listify = cata phi_L

Проверяем в GHCi:

*Bis> listify (In Nil)
[]
*Bis> listify (In (Cons 'i' (In Nil)))
"i"
*Bis> listify (In (Cons 'h' (In (Cons 'i' (In Nil)))))
"hi"

УПРАЖНЕНИЕ: Придумайте и реализуйте другие (L a)-алгебры.

Бонус-трек: "Эвалютор" на стеке

Зададим для Expr E-алгебру типа E ([Int] -> [Int]) -> [Int] -> [Int]

phi_E' :: E ([Int] -> [Int]) -> [Int] -> [Int]
phi_E' (Num n)    = push n
phi_E' (Add e e') = add . e' . e
-- катаморфизм
eval' :: Rec E -> ([Int] -> [Int])
eval' = cata phi_E'
--сервисные функции над стеком, реализованным через список
push a as = a : as
add (a : b : cs) = (b + a) : cs

Проверяем в GHCi:

*Bis> eval' (In (Add (In (Add (In (Num 3)) (In (Num 5)))) (In (Num 7)))) []
[15]

Продолжение следует...