deniok: (Default)
deniok ([personal profile] deniok) wrote2007-12-30 06:31 pm

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

Предыдущие посты этой серии:
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.

[identity profile] deni-ok.livejournal.com 2008-01-20 12:06 pm (UTC)(link)
CoQ почти не смотрел. Это ведь скорее система для доказательств, а не PL общего назначения, нес па?

[identity profile] nivanych.livejournal.com 2008-01-20 12:59 pm (UTC)(link)
Да, скорее, это система для доказательств,
но там делается упор на конструктивную математику.
Есть Extraction Language для Ocaml, Haskell, Scheme
и какой-то его (CoQ) внутренний язык Toplevel.

Программирование выглядит типа того,
что формулируешь спецификацию, потом
детализируешь её, некоторые куски
дописываешь сам, потом к спецификации
добавляешь упрощающие доказательство мелочи,
и после некоторых мучений получаешь программу,
которая гарантированно соответствует спецификации.
Вообще, мучения на практике возникают, в основном,
только при доказательстве всяческих (не)равенств,
во многом остальном выглядит похожим на Epigram.
Вроде бы, чего-то в Epigram2 в делают с
(не)равенствами в их Observational Type System.

Сложность доказательства зависит, главным образом,
от сложности поставленных условий.
Например, бывает просто упорядочивающая перестановка,
а бывает ещё и с дополнительными условиями, например,
видел статью, где в CoQ описывалась пирамидальная сортировка.
Можно сформулировать задачи минимизации, только оно
далеко не все их них сможет разрешить самостоятельно.

Конечно, это не похоже на языки общего назначения, но могло бы
быть таким, при условии полной автоматизации доказательств.
Так что, ИМХО, не многое отделяет proof assistant'ы
от языков программирования общего назначения.

[identity profile] deni-ok.livejournal.com 2008-01-20 02:14 pm (UTC)(link)
Спасибо, обязательно окунусь ;) Но чуть позже.