Коалгебры и анаморфизмы
Dec. 30th, 2007 06:31 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
Предыдущие посты этой серии:
1. Типы как неподвижные точки функторов
2. Алгебры и катаморфизмы
Краткое содержание предыдущих серий
С помощью аналога fix для типов:
Введя понятие f-алгебры как функции phi :: f a -> a для заданных функтора f и типа a, мы пришли к нотации катаморфизма:
А можно ли наоборот?
Попробуем решить обратную задачу - не свертки рекурсивного типа данных в значение, а "развертывания" такого типа на основе значения. В классическом Хаскелле этим занимается
Анаморфизмы и коалгебры
Мы строили катаморфизмы на основе изоморфизма In :: f (Rec f) -> Rec f (f-инварианта), при этом следующее преобразование было тождественным:
Заменим теперь каждое вхождение out :: Rec f -> f (Rec f) на произвольную функцию psi :: a -> f a. Получим нотацию анаморфизма:
Пример: тип Nat
Для рекурсивного типа
Смотрим в GHCi:
Саму по себе работу анаморфизма можно увидеть, расписав пошаговые редукции вызова функции ana, например:
Пример-упражнение: тип Bin
Можно смонтировать рекурсивный тип данных для двоичного представления натуральных чисел:
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.
no subject
Date: 2007-12-30 10:50 pm (UTC)http://www.londonhug.net/2007/12/11/video-design-patterns-as-higher-order-datatype-generic-programs/
no subject
Date: 2007-12-30 11:29 pm (UTC)Собственно вся эта серия началась с того, что я наткнулся на статью того же Jeremy Gibbons:
http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/parametric.pdf
И решил, что в бананах для меня не должно оставаться тёмных мест :)
В частности, почему важен именно Bifunctor (Difunctor в терминологии Meijer-Hutton).
ЗЫ: Будем (в деле HUG) держать равнение на Лондон :)
no subject
Date: 2007-12-31 09:06 pm (UTC)no subject
Date: 2008-01-15 06:24 am (UTC)А по поводу fmap это fix для типов получается или я что-то путаю?
И ещё выходит что катаморфизм делает из рекурсивного типа нерекурсивный, а анаморфизм наоборот? Или есть какая-то ещё важная особенность которую я упускаю?
no subject
Date: 2008-01-16 08:26 pm (UTC)Типа того.
В ТК функтор T ставит в соответствие каждой стрелке f : c -> c' стрелку T f : T c -> T c'. В Хаскелле это делает
который имеется для функтора f.
Ну и аксиомы для функторов ТК выполняются
>fmap это fix для типов получается или я что-то путаю?
Не, fix для функторов - это Rec
Подсовывая сюда (вместо f) нерекурсивные инстансы функтора, получаем рекурсивные типы.
>...катаморфизм делает из рекурсивного типа нерекурсивный, а анаморфизм наоборот?
Да, катаморфизм обобщает паттерн рекурсии fold, а анаморфизм unfold.
no subject
Date: 2008-01-16 08:35 pm (UTC)no subject
Date: 2008-01-16 08:43 pm (UTC)Иначе все полиморфные типы всегда будут под forall.
no subject
Date: 2008-01-16 08:58 pm (UTC)fmap :: (c -> c') -> (f c -> f c')
не совсем понятно что есть f c, откуда видимо "вылезает" ограничение на f...
Или f c - это типа инстанс типа классов (не знаю как это правильно формулируется), поэтому надо иметь его определённым, т.к. мы не можем оперировать произвольными типами классов?
no subject
Date: 2008-01-16 09:15 pm (UTC)no subject
Date: 2008-01-16 09:20 pm (UTC)no subject
Date: 2008-01-16 09:27 pm (UTC)no subject
Date: 2008-01-16 09:31 pm (UTC)Коли полезли в эту тему: а кайнд параметризуемый кайндом в реальности вещь используемая?
no subject
Date: 2008-01-16 09:44 pm (UTC)no subject
Date: 2008-01-16 09:53 pm (UTC)А, дошло, вложенности там на уровне кайндов не выходит, т.к. есть уже вложенность на уровне типов. Есть лишь число параметров кайнда.
Или снова вру? :)
Кстати я правильно понимаю, что типы классов единственный вариант создания кайндов в хаскеле?
no subject
Date: 2008-01-16 10:02 pm (UTC)Имеем:
kind'ом обладают конструкторы типов.
no subject
Date: 2008-01-16 10:07 pm (UTC)Ну да, точно, конструкторы, классы ониж по сути группируют функции, туплю.
no subject
Date: 2008-01-16 09:24 pm (UTC)Ну ты как-то скептически выражаешься ;)
Способ ограничить параметрический полиморфизм, когда он избыточен. В моей презентации по free theorems как раз о Eq и теореме для nubBy, которая всё равно имеет контекст (x = y) = (f x = f y), так что переход к nub + ограниченный квантор не вносит никакой дополнительной сложности/сущности.
no subject
Date: 2008-01-16 09:30 pm (UTC)no subject
Date: 2008-01-16 10:05 pm (UTC)no subject
Date: 2008-01-16 10:05 pm (UTC)no subject
Date: 2008-01-20 11:49 am (UTC)Ну, в CoQ есть описание
довольно большой части ТК.
Конечно, не всё сможет
вывестись автоматически, но и
в Хаскелевой системе типов
компилятор не всегда закончит работу.
;)
no subject
Date: 2008-01-20 12:06 pm (UTC)no subject
Date: 2008-01-20 12:59 pm (UTC)но там делается упор на конструктивную математику.
Есть Extraction Language для Ocaml, Haskell, Scheme
и какой-то его (CoQ) внутренний язык Toplevel.
Программирование выглядит типа того,
что формулируешь спецификацию, потом
детализируешь её, некоторые куски
дописываешь сам, потом к спецификации
добавляешь упрощающие доказательство мелочи,
и после некоторых мучений получаешь программу,
которая гарантированно соответствует спецификации.
Вообще, мучения на практике возникают, в основном,
только при доказательстве всяческих (не)равенств,
во многом остальном выглядит похожим на Epigram.
Вроде бы, чего-то в Epigram2 в делают с
(не)равенствами в их Observational Type System.
Сложность доказательства зависит, главным образом,
от сложности поставленных условий.
Например, бывает просто упорядочивающая перестановка,
а бывает ещё и с дополнительными условиями, например,
видел статью, где в CoQ описывалась пирамидальная сортировка.
Можно сформулировать задачи минимизации, только оно
далеко не все их них сможет разрешить самостоятельно.
Конечно, это не похоже на языки общего назначения, но могло бы
быть таким, при условии полной автоматизации доказательств.
Так что, ИМХО, не многое отделяет proof assistant'ы
от языков программирования общего назначения.
no subject
Date: 2008-01-20 02:14 pm (UTC)no subject
Date: 2008-01-23 04:02 pm (UTC)"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
no subject
Date: 2008-01-23 04:15 pm (UTC)no subject
Date: 2008-01-23 05:58 pm (UTC)Ох, сколько я уже Сергею обещал ...
"Долгов" у меня много накопилось :-)
Сейчас вот по работе мне надо всякую фигню ;-)
Для полного счастия надо разобраться,
что такое Second Generation Wavelet, и (главное)
как реализовывать его на неравномерной сетке.
С первого взгляда всё кажется простым и понятным,
но обнаруживаются всякие тонкости.
Можно это и не раскапывать, но тогда будет,
как у всех, просто-напросто, куча нудной и простой работы.
Я же выбираю "всякую фигню", хоть оно и не касается
всяких там интересностей по логике и теории вычислений :-)
no subject
Date: 2008-01-23 05:59 pm (UTC)На свою голову (и/или задницу).
no subject
Date: 2008-01-23 06:01 pm (UTC)no subject
Date: 2008-01-23 07:05 pm (UTC)Generic Programming: Advanced Lectures (Lecture Notes in Computer Science)
Date: 2008-02-13 08:55 am (UTC)http://www.pdfchm.com/book/generic-programming-advanced-lectures-lecture-notes-in-computer-science--9745/
Re: Generic Programming: Advanced Lectures (Lecture Notes in Computer Science)
Date: 2008-02-13 03:47 pm (UTC)