Коалгебры и анаморфизмы

[deniok]

Предыдущие посты этой серии:
1. Типы как неподвижные точки функторов
2. Алгебры и катаморфизмы



Краткое содержание предыдущих серий

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

data Rec f = In (f (Rec f))

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

Введя понятие f-алгебры как функции phi :: f a -> a для заданных функтора f и типа a, мы пришли к нотации катаморфизма:

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

Мы увидели, что задавая разные f-алгебры (phi :: f a -> a), мы можем универсально описывать стратегии свертывания произвольных алгебраических структур:

foldFunctor :: Functor f => Rec f -> a
foldFunctor = cata phi

А можно ли наоборот?

Попробуем решить обратную задачу - не свертки рекурсивного типа данных в значение, а "развертывания" такого типа на основе значения. В классическом Хаскелле этим занимается

unfoldr :: (b -> Maybe (a, b)) -> b -> [a]

из Data.List. Конечно в этом случае целевым функтором является список. Очевидно, что искомый тип нашего "развёртывателя":

unfoldFunctor :: Functor f => a -> Rec f

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

Мы строили катаморфизмы на основе изоморфизма In :: f (Rec f) -> Rec f (f-инварианта), при этом следующее преобразование было тождественным:

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

Зададим теперь тождественное преобразование рекурсивной структуры

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

базирующиеся на основе изоморфизма, обратного к изоморфизму In

out :: Rec f -> f (Rec f)
out (In x) = x

Покажем что copy' = id на примере выражения In (S (In (S (In Z)))) типа Nat:

copy'               (In (S (In (S (In Z)))))   ~> по def copy'
In (fmap copy' (out (In (S (In (S (In Z))))))  ~> по def out
In (fmap copy'          (S (In (S (In Z))))    ~> по def fmap
In (S (copy'               (In (S (In Z)))))   ~> по def copy'
In (S (In (fmap copy' (out (In (S (In Z))))))) ~> по def out
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'(out  (In Z))))))) ~> по def out
In (S (In (S (In (fmap copy'          Z)))))   ~> по def fmap
In (S (In (S (In (Z)))))

Заменим теперь каждое вхождение out :: Rec f -> f (Rec f) на произвольную функцию psi :: a -> f a. Получим нотацию анаморфизма:

ana :: Functor f => (a -> f a) -> a -> Rec f
ana psi x = In (fmap (ana psi) (psi x))

Функцию psi :: a -> f a называют f-коалгеброй - она описывает способ получения функтора f a на основе значений типа a.


Пример: тип Nat

Для рекурсивного типа

data N c = Z | S c 

instance Functor N where
  fmap g  Z    = Z
  fmap g (S x) = S (g x)

type Nat = Rec N

мы имели N-алгебру

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

и катаморфизм, задающий преобразование

natToInt :: Nat -> Int
natToInt = cata phi_N

Дуальная к этой алгебре N-коалгебра

psi_N :: Int -> N Int
psi_N 0 = Z
psi_N n = S (n-1)

задает анаморфизм

intToNat :: Int -> Nat
intToNat = ana psi_N

выполняющий обратное преобразование.
Смотрим в GHCi:

*Bis> intToNat 42
(In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S 
(In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S 
(In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S 
(In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S (In (S 
(In (S (In (S (In (Z)))))))))))))))))))
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
*Bis> natToInt (intToNat 42)
42

Саму по себе работу анаморфизма можно увидеть, расписав пошаговые редукции вызова функции ana, например:

ana                                  psi_N 2       ~> по def ana
In (               fmap (ana psi_N) (psi_N 2))     ~> по def psi_N
In (               fmap (ana psi_N)     (S 1))     ~> по def fmap
In (S (                  ana psi_N         1))     ~> по def ana
In (S (In (        fmap (ana psi_N) (psi_N 1))))   ~> по def psi_N
In (S (In (        fmap (ana psi_N)     (S 0))))   ~> по def fmap
In (S (In (S (           ana psi_N         0))))   ~> по def ana
In (S (In (S (In ( fmap (ana psi_N) (psi_N 0)))))) ~> по def psi_N
In (S (In (S (In ( fmap (ana psi_N) Z)))))         ~> по def fmap
In (S (In (S (In (Z)))))

Пример-упражнение: тип Bin

Можно смонтировать рекурсивный тип данных для двоичного представления натуральных чисел:

data Bin = Empty | Zero Bin | One Bin

При таком определении двоичные числа читаются справа налево

                Empty   = 0
            One Empty   = 1
      Zero (One Empty)  = 2
      One  (One Empty)  = 3
Zero (Zero (One Empty)) = 4
и т.д.

УПРАЖНЕНИЕ: Запишите тип Bin как неподвижную точку функтора B. Реализуйте B-алгебру, задающую катаморфизм, преобразующий этот тип в тип Int. Реализуйте B-коалгебру, задающую анаморфизм, генерирующий двоичное Bin-представление на основе переданного числа типа Int.

Comments

[nivanych.livejournal.com]

И обозвали они это -
"Constructive Category Theory".

Ещё советую почитать работу Hagino.
"T-algebras are also used in domain theory,
but while domain theory needs some primitive
data types, like products, to start with,
we do not need any.
Products, coproducts and exponentiations
are defined exactly like in category theory
using adjunctions. F,G-dialgebras also enable us
to define natural number object, object for
finite lists and other familiar data types in programming.
Futhermore, their symmetry allows us to have the dual
of the natural number object and the object
for infinite lists (or lazy lists).
We also introduce a functional programming language
in a categorical style. It has no primitive data types
nor primitive control structures. Data types are declared
using F,G-dialgebras and each data type is associated
with its own control structure. For example, natural numbers
are associated with primitive recursion.
A specification language to describe categories is also included.
It is used to give a formal semantics to F,G-dialgebras
as well as to give a basis to the categorical
programming language we introduce."

Не хватает только развитого полиморфизма,
ну и Зависимых Типов, но надо обратить внимание,
что год публикации - 1987.
Страничка Tatsuya Hagino -
http://www.tom.sfc.keio.ac.jp/~hagino/
Ссылка на книжку (там же) -
http://www.tom.sfc.keio.ac.jp/~hagino/thesis.pdf

[deni-ok.livejournal.com]

Написал бы обзор (или хотя бы обзорчик). Потом бы в диссертацию вставил ;)

[nivanych.livejournal.com]

Обязательно будет ...
Ох, сколько я уже Сергею обещал ...
"Долгов" у меня много накопилось :-)

Сейчас вот по работе мне надо всякую фигню ;-)
Для полного счастия надо разобраться,
что такое Second Generation Wavelet, и (главное)
как реализовывать его на неравномерной сетке.
С первого взгляда всё кажется простым и понятным,
но обнаруживаются всякие тонкости.
Можно это и не раскапывать, но тогда будет,
как у всех, просто-напросто, куча нудной и простой работы.
Я же выбираю "всякую фигню", хоть оно и не касается
всяких там интересностей по логике и теории вычислений :-)

[nivanych.livejournal.com]

Многие бы сказали, что сам себе ищу трудностей.
На свою голову (и/или задницу).

[deni-ok.livejournal.com]

Ну тут так: либо ты их ищешь и побеждаешь, либо наоборот они тебя ;)

[nivanych.livejournal.com]

Пока ничья ;-)