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

[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

[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)

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