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]


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

Date: 2007-12-13 10:03 pm (UTC)
From: [identity profile] dtim.livejournal.com
"Катаморфизмы под катом" - это алгебраически здорово! :)

Date: 2007-12-14 07:11 am (UTC)
From: [identity profile] deni-ok.livejournal.com
В следующих сериях ждите параморфизмы под паром и хиломорфизмы под Хилем :))

Date: 2007-12-14 10:08 am (UTC)
From: [identity profile] dtim.livejournal.com
А что с анаморфизмами делать?

Date: 2007-12-14 10:45 am (UTC)

Date: 2007-12-14 06:59 am (UTC)
From: [identity profile] kurilka.livejournal.com
Ммм, а почто тэгом общим не объеденены обе записи?

Date: 2007-12-14 07:06 am (UTC)
From: [identity profile] deni-ok.livejournal.com
Сейчас поправлю, будет тэг "bananas in space".

Date: 2007-12-14 07:06 am (UTC)
From: [identity profile] kurilka.livejournal.com
Спасибо

Date: 2007-12-14 11:52 am (UTC)
From: [identity profile] antilamer.livejournal.com
Как раз сегодня читал эту статью. Сломался на словах "ковариантный" и "контравариантный"; не расскажешь, что они там означают?

Date: 2007-12-14 12:25 pm (UTC)
From: [identity profile] deni-ok.livejournal.com
(->) имеет kind *->*->* а для функторов требуется *->*. Надо связать один из, тогда есть две возможности (ко- и контрвариантная)

instance типаFunctor (a->)

vs.

instance типаFunctor (->b)

Как-то так.

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 Jul. 13th, 2025 12:35 pm
Powered by Dreamwidth Studios