Бананы на розовых кустах

[lomeo]

Когда я только разбирался с бананами, линзами и т.д. задача описания катаморфизма для розы:

data Rose a = Rose a [Rose a]

вызывала у меня большое затруднение.


Мы с mibori очень пытались понять, как это сделать правильно. Я там напутал со страшной силой. Вчера я разбирался с разными бла-морфизмами и то, как их получить, основываясь на их ТК определениях (initial F-algebra в нашем случае) - и я вдруг прозрел.

Всё оказывается очень просто. Пусть роза - это initial R_A-algebra, которую мы назовём (μRA, in).

Во-первых, поскольку мы работаем с initial R_A-algebra, наш тип должен быть этим самым функтором R_A. С Rose так и есть:

instance Functor Rose where
    fmap f (Rose x xs) = Rose (f x) $ map f xs

Во-вторых, конструктор у розы всего один:

rose = in

поэтому нам нужна всего одна функция. Поскольку функтор R_A определяется так:

RA(X) = A × LX(Y)

где L_A - это функтор, относящийся к списку:

LA(X) = 1 + A × X

то получаем, что нам нужна функция

r : A × μLC -> C

μL_C - это carrier L_C-алгебры для списков.

Дальше. Катаморфизм есть уникальное решение (как следует из его universal property) следующего равенста:

(|φ|) . rose = r . (id × L(|φ|))

Самое сложное здесь - понять почему мы используем L_(|φ|). Я пока понимаю это интуитивно, подстановкой в типе функции r.

Ну, и всё! :-)

foldRose r (Rose x xs) = r x (map (foldRose r) xs)

Теперь я чувствую, что работа с ТК приносит плоды. Могу, например, параморфизм расписать для розы, хе-хе. А ведь я ещё в самом начале ;-)

Comments

жесть

[nealar.livejournal.com]

Читаю свои комменты в той дискуссии. Блин! Я правда был такой умный или это мне кто-то подсказывал? Вроде, щас я заметно тупее.

Re: жесть

[lomeo.livejournal.com]

Правда-правда... Я, например, твои посты про зависимые типы до сих пор не понимаю :-)
Кстати, 5-я часть, если она есть не потэгана.

Re: жесть

[nealar.livejournal.com]

Нету. Она, кажется, задумывалась как раз про это самое: тип W, любой индуктивный ADT изоморфен розовому дереву (или проще) и т.д.
А что ты конкретно в них не понимаешь? Хочу вопросов и придирок!! Я их собирался отполировать, чтобы нормальное объяснение получилось. Но никто не спрашивает и не критикует.

[lionet.livejournal.com]

foldRose r (Rose x xs) = r x (map (foldRose f) xs)

(foldRose f)?

[lomeo.livejournal.com]

Так точно, спасибо! Сейчас поправлю...

[kurilka.livejournal.com]

Ммм, 3 года войны с бананами...
А я только в том году почитал (правда не фиг чтоб понял), скокаж мне ещё мозг ломать (ибо про алгебры не понимаю ничего практически)...

[lomeo.livejournal.com]

По бананам могу порекомендовать замечательную статью Graham Hutton A tutorial on the universality and expressiveness of fold (http://www.cs.nott.ac.uk/~gmh/bib.html#fold). Там, правда, списки, но врубаешь в её мощь очень сильно.

[kurilka.livejournal.com]

В мощь статьи?
За ссылку сеньк.
Вопрос на засыпку - а "общих" статей по категорной семантике не встречал?
Просто посмотрел вот это - http://video.google.com/videoplay?docid=1878650318476022439 (в бравзере не смотрит, но мп4 сохраняет) и как-то заинтересовался.
Статья Даны Скотт (или как там его имя склоняется?) приведена, но блин в инете тока в списках литературы она встречается :(

[lomeo.livejournal.com]

Да ёпрст

Я читаю всё, что попадётся, как только вижу рядом слова category и haskell :-)

Например, профессора Varmo Vene (http://www.cs.ut.ee/~varmo/) и его собутыльника Tarmo Uustalu (http://cs.ioc.ee/~tarmo). С комонадами тоже, кажется, у них познакомился. У них вообще много, что можно взять как паттерн ФП и использовать.

[kurilka.livejournal.com]

Вармо-то у меня в ссылках числится, только у него чего-то там всё по мне слишком "жёсткое" (или я не прав?)
А у Тармо что интересного посоветуешь?

[lomeo.livejournal.com]

У Тармо я какие то презентации смотрел, сейчас не вспомню. Из не слишком жёсткого не могу ничего посоветовать :-( У меня только вчера скачок был очередной в понимании. Читаю Вене "Categorical programming with inductive and coinductive types". Если не категорное, то по морфизмам много чего есть, только большей частью там списки рассматриваются. А програмист-прагматик хочет более общих решений. В Хаскель вон даже пакет есть Control.Recursive называется. Сейчас может пост успею перед сном написать.

[kurilka.livejournal.com]

Categorical programming скачан давненько :)
Только вот категории я добить до чего-то сносного пока ещё не могу, разбираю пределы сейчас.
А пост почитаем обязательно.

[palm-mute.livejournal.com]

Роза у тебя какая-то незнакомая. Мне казалось, что розовое дерево выглядит так:

data RoseTree a = RoseTree a [RoseTree a]

И соответствующий функтор должен выглядеть так:

data RoseTreeF a r = Rose a [r]

instance Functor (RoseTreeF a) where
    fmap f (Rose a rs) = Rose a (map f rs)

Во всяком случае, у Марка Джонса (http://web.cecs.pdx.edu/~mpj/pubs/springschool95.pdf) розы такие.
Хотя я в ТК с бананами ничего не понимаю, и скорее всего, совершенно не понял, о чем ты.
з.ы. мне казалось, что наиболее просто получить fold - это заменить в структуре данных каждый конструктор на функцию с соответствующими типами аргументов.
убегает, вжав голову в плечи

[lomeo.livejournal.com]

Блин! Это она и есть и разбирал я её, быстро писал, ёлки. Сейчас поправлю.

[lomeo.livejournal.com]

Насчёт ЗЫ - да, конечно. Только вот как заменить тип аргумента [Rose a]?
Или возьми верёвку data Rope a b = Nil | Twist b (Rope b a)

[palm-mute.livejournal.com]

Я процесс перехода от рекурсивного типа к фикспойнту функтора представляю себе на пальцах, без категорий (не узрел свет ТК, о чем сожалею, но что поделаешь):
берем рекурсивный конструктор типа, добавляем в конец списка аргументов новую переменную r, каждый рекурсивный "вызов" этого конструктора заменяем на r.
Что делать в случае Rope - не знаю. Было бы очень интересно взглянуть.

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

[lomeo.livejournal.com]

На словах не очень понял, можно пример?

Я пока не знаю, что делать с data Foo t a = Foo (t (Foo a))

[palm-mute.livejournal.com]

>Я пока не знаю, что делать с data Foo t a = Foo (t (Foo a))
Я тоже не знаю, у меня эта строчка не компилируется.
Ноя в принципе не знаю, каким образом делаются "банановые" преобразования надо nested datatypes и похожими патологическими случаями. Я умею готовить только простые рекурсивные типы (списки, деревья, выражения), так что вряд ли я тебе что-то новое скажу.

[lomeo.livejournal.com]

блин, ты что там всё компилишь? :-)
data Foo t a = Foo (t (Foo t a))

Да, nested datatypes я так и не понял :-(

[palm-mute.livejournal.com]

> блин, ты что там всё компилишь? :-)
А что делать? Если не компилится в голове, надо проверить на железяке.

Думаю, нерекурсивный функтор получается примерно так:

data FooF t a r = FooF (t r) -- заменили все вхождения Foo t a на r

instance (Functor t) => Functor (FooF t a) where
    fmap f (FooF tr) = FooF (fmap f tr)

[lomeo.livejournal.com]

Да, спасибо, но у тебя функтор по r получился, а нам a нужно. А то ты легко от рекурсивности типа уйдёшь. Будет у тебя FooF "x" легко.

Надо

data Foo t a = Foo (t (Foo a))

instance (Functor t) => Functor (Foo t) where
  fmap f (Foo x) = Foo $ fmap (fmap f) x

ну и тогда дальше просто

foldFoo :: (Functor t) => (t b -> b) -> Foo t a -> b
foldFoo f (Foo x) = f (fmap (foldFoo d) x)

Ну и из ТК получается тоже точно так же. Спасибо, что направил на путь истиный :-)

[lomeo.livejournal.com]

Ёлки data Foo t a = Foo (t (Foo t a)) конечно!
А то компилироваться не будет ;-) Надо бы проверять перед постом...

[palm-mute.livejournal.com]

> Спасибо, что направил на путь истиный :-)
ЭЭ. Не за что, я сам не понял, куда я тебя направил :).

>но у тебя функтор по r получился, а нам a нужно
ничего не понимаю. зачем нам a нужно?
data types a-la-carte как раз получаются из функторов по r.
На примере списков, как у Марка Джонса:

data ListF a r = Nil | Cons a r

instance Functor (ListF a) where
    fmap f Nil = Nil
    fmap f (Cons a r) = Cons a (f r)

data Fix f = In { out :: f (Fix f) }

type List a = Fix (ListF a)

fold f = f . fmap (fold f) . out 

sumList = fold f
    where f Nil = 0
          f (Cons x xs) = x + xs

test =  sumList $ In $ Cons 3 $ In $ Cons 2 $ In $ Cons 1 $ In Nil -- sum [3,2,1] = 6

[lomeo.livejournal.com]

А, я просто не понял, что ты его в Fix оборачивать будешь. А так

type Foo t a = Fix (FooF t a)

получаем те же яйца, что и в рекурсивном типе.

[deni-ok.livejournal.com]

>Или возьми верёвку data Rope a b = Nil | Twist b (Rope b a)

В конце бананов написано, что если взять Fix уровня типов с кайндом ((*->*)->(*->*))->(*->*) вместо обыденного (*->*)->* и немного потрахаться, то будет счастье.

Сам не пробовал.

[lomeo.livejournal.com]

Да, мне хочется категорный подход увидеть.