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

[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

[lomeo.livejournal.com]

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