Алгебры и катаморфизмы
Dec. 13th, 2007 11:16 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
Продолжаю вести конспект Bananas in Space (начало здесь).
Краткое содержание первой серии
С помощью аналога fix для типов:
Нотация катаморфизма
Рассмотрим функцию
Алгебры
Для данных функтора f и типа a функция phi :: f a -> a известна как f-алгебра.
Если в примере с функтором N задать функцию phi, заменяющую Z на 0, а S на succ, то получим N-алгебру типа N Int -> Int
Алгебры для Expr и List
Построим ещё алгебры для примеров из прошлой серии.
Если в примере с функтором E задать функцию phi, заменяющую Num на id, а Add на (+),то получим E-алгебру типа E Int -> Int:
УПРАЖНЕНИЕ: задайте другие E-алгебры, порождающие запись арифметических выражений в префиксной и инфиксной строковой формах.
Если в примере с функтором L a задать функцию phi, заменяющую Nil на [], а Cons на (:), то получим (L a)-алгебру типа L a [a] -> [a]
УПРАЖНЕНИЕ: Придумайте и реализуйте другие (L a)-алгебры.
Бонус-трек: "Эвалютор" на стеке
Зададим для Expr E-алгебру типа E ([Int] -> [Int]) -> [Int] -> [Int]
Продолжение следует...
Краткое содержание первой серии
С помощью аналога 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]
Продолжение следует...