deniok: (Default)
[personal profile] 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]


Продолжение следует...
This account has disabled anonymous posting.
If you don't have an account you can create one now.
HTML doesn't work in the subject.
More info about formatting

Profile

deniok: (Default)
deniok

February 2022

S M T W T F S
  12345
6789101112
13141516171819
20212223 242526
2728     

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jun. 11th, 2025 12:38 pm
Powered by Dreamwidth Studios