Когда состав катаморфизмов является катаморфизмом?
Со страницы 3 http://research.microsoft.com/en-us/um/people/emeijer/Papers/meijer94more.pdf:
в общем случае неверно, что катаморфизмы замкнуты по составу
При каких условиях катаморфизм превращается в катаморфизм? Более конкретно (при условии, что я правильно понял утверждение):
Предположим, у меня есть два базовых функтора F а также G и складывает для каждого: foldF :: (F a -> a) -> (μF -> a) а также foldG :: (G a -> a) -> (μG -> a),
Теперь предположим, что у меня есть две алгебры a :: F μG -> μG а также b :: G X -> X,
Когда состав (foldG b) . (foldF a) :: μF -> X катаморфизм?
Редактировать: у меня есть предположение, основанное на расширенном ответе dblhelix: outG . a :: F μG -> G μG должен быть компонентом в μG какой-то естественной трансформации η :: F a -> G a, Я не знаю, правильно ли это. (Правка 2: Как отмечает Кола, этого достаточно, но не обязательно.)
Редактировать 3: Рен Торнтон в Haskell-Cafe добавляет: "Если у вас есть правильный тип свойства дистрибутивности (как предполагает Кола), то все получится для конкретного случая. Но наличие правильного типа свойства дистрибутивности обычно равносильно тому, чтобы быть естественное преобразование в какую-то соответствующую категорию, так что это просто откладывает вопрос о том, всегда ли существует соответствующая связанная категория, и можем ли мы формализовать, что означает "надлежащим образом связанная".
4 ответа
When is the composition (fold2 g) . (fold1 f) :: μF1 -> A a catamorphism?
Когда существует F1-алгебра h :: F1 A -> A такой, что fold1 h = fold2 g . fold1 f,
Чтобы увидеть, что катаморфизмы в целом не являются замкнутыми по составу, рассмотрим следующие общие определения фиксированной точки, алгебры и катаморфизма на уровне типов:
newtype Fix f = In {out :: f (Fix f)}
type Algebra f a = f a -> a
cata :: Functor f => Algebra f a -> Fix f -> a
cata phi = phi . fmap (cata phi) . out
Для катаморфизмов, чтобы составить нам нужно
algcomp :: Algebra f (Fix g) -> Algebra g a -> Algebra f a
Теперь попробуйте написать эту функцию. Он принимает две функции в качестве аргументов (типов f (Fix g) -> Fix g а также g a -> a соответственно) и значение типа f a, и это должно произвести значение типа a, Как бы Вы это сделали? Чтобы получить значение типа a Ваша единственная надежда - применить функцию типа g a -> a, но тогда мы застряли: у нас нет средств, чтобы превратить значение типа f a в значение типа g aмы?
Я не уверен, имеет ли это какое-либо значение для ваших целей, но пример условия, при котором можно составить катаморфизм, - это если мы имеем морфизм от результата второго ката до фиксированной точки второго функтора:
algcomp' :: (Functor f, Functor g) =>
(a -> Fix g) -> Algebra f (Fix g) -> Algebra g a -> Algebra f a
algcomp' h phi phi' = cata phi' . phi . fmap h
(Отказ от ответственности: это выходит за рамки моей компетенции. Я считаю, что я прав (с оговорками, предоставленными в разных точках), но... Проверьте это сами.)
Катаморфизм может рассматриваться как функция, которая заменяет конструкторы типа данных другими функциями.
(В этом примере я буду использовать следующие типы данных:
data [a] = [] | a : [a]
data BinTree a = Leaf a | Branch (BinTree a) (BinTree a)
data Nat = Zero | Succ Nat
)
Например:
length :: [a] -> Nat
length = catamorphism
[] -> 0
(_:) -> (1+)
(К сожалению, catamorphism {..} Синтаксис недоступен в Haskell (я видел нечто подобное в Pola). Я хотел написать квазиквотер.)
Итак, что же length [1,2,3]?
length [1,2,3]
length (1 : 2 : 3 : [])
length (1: 2: 3: [])
1+ (1+ (1+ (0 )))
3
Тем не менее, по причинам, которые станут очевидными позже, было бы лучше определить его как тривиально эквивалентный:
length :: [a] -> Nat
length = catamorphism
[] -> Zero
(_:) -> Succ
Давайте рассмотрим еще несколько примеров катаморфизма:
map :: (a -> b) -> [a] -> b
map f = catamorphism
[] -> []
(a:) -> (f a :)
binTreeDepth :: Tree a -> Nat
binTreeDepth = catamorphism
Leaf _ -> 0
Branch -> \a b -> 1 + max a b
binTreeRightDepth :: Tree a -> Nat
binTreeRightDepth = catamorphism
Leaf _ -> 0
Branch -> \a b -> 1 + b
binTreeLeaves :: Tree a -> Nat
binTreeLeaves = catamorphism
Leaf _ -> 1
Branch -> (+)
double :: Nat -> Nat
double = catamorphism
Succ -> Succ . Succ
Zero -> Zero
Многие из них могут быть красиво составлены для формирования новых катаморфизмов. Например:
double . length . map f = catamorphism
[] -> Zero
(a:) -> Succ . Succ
double . binTreeRightDepth = catamorphism
Leaf a -> Zero
Branch -> \a b -> Succ (Succ b)
double . binTreeDepth тоже работает, но это почти чудо, в определенном смысле.
double . binTreeDepth = catamorphism
Leaf a -> Zero
Branch -> \a b -> Succ (Succ (max a b))
Это работает только потому, что double распределяет по max... Что является чистым совпадением. (То же самое относится и к double . binTreeLeaves.) Если мы заменили max с чем-то, что не так хорошо сочеталось с удвоением... Давайте определимся с новым другом (который не ладит с другими). Для бинарных операторов, которые double не распространять, мы будем использовать (*),
binTreeProdSize :: Tree a -> Nat
binTreeProdSize = catamorphism
Leaf _ -> 0
Branch -> \a b -> 1 + a*b
Попробуем установить достаточные условия для двух катаморфизмов двух составляющих. Понятно, что любой катаморфизм будет очень рад length, double а также map f потому что они дают свою структуру данных, не глядя на дочерние результаты. Например, в случае lengthможно просто заменить Succ а также Zero с тем, что вы хотите, и у вас есть новый катаморфизм.
- Если первый катаморфизм приводит к структуре данных, не смотря на то, что происходит с его дочерними элементами, два катаморфизма превратятся в катаморфизм.
Помимо этого, все становится более сложным. Давайте различать обычные аргументы конструктора и "рекурсивные аргументы" (которые мы будем отмечать знаком%). Так Leaf a не имеет рекурсивных аргументов, но Branch %a %b делает. Давайте используем термин "рекурсивная фиксированность" конструктора, чтобы ссылаться на количество рекурсивных аргументов, которые он имеет. (Я составил оба этих термина! Я понятия не имею, что такое правильная терминология, если она есть! Остерегайтесь использовать их в другом месте!)
Если первый катаморфизм отображает что-то в конструктор с нулевой рекурсивной фиксированностью, все хорошо!
a | b | cata(b.a)
===============================|=========================|================
F a %b %c .. -> Z | Z -> G a b .. | True
Если мы отобразим дочерние элементы непосредственно в новый конструктор, у нас тоже все хорошо.
a | b | cata(b.a)
===============================|=========================|=================
F a %b %c .. -> H %c %d .. | H %a %b -> G a b .. | True
Если мы отобразим в рекурсивную фиксированность один конструктор...
a | b | cata(b.a)
===============================|=========================|=================
F a %b %c .. -> A (f %b %c..) | A %a -> B (g %a) | Implied by g
| | distributes over f
Но это не так. Например, если есть g1g2 такой, что g (f a b..) = f (g1 a) (g2 b) .., это тоже работает.
Отсюда, правила, скорее всего, станут еще хуже.
Катаморфизмы разрушают структуру данных в значение результата. Таким образом, в общем случае, когда вы применяете катаморфизм, в результате получается что-то совершенно другое, и вы не можете применить к нему другой катаморфизм.
Например, функция, которая суммирует все элементы [Int] это катаморфизм, но результат Int, Там нет никакого способа, как применить другой катаморфизм на нем.
Однако некоторые специальные катаморфизмы создают результат того же типа, что и входные данные. Одним из таких примеров является map f (для некоторой заданной функции f). В то время как это разрушает первоначальную структуру, это также создает новый список как его результат. (На самом деле, map f может рассматриваться как как катаморфизм, так и анаморфизм.) Поэтому, если у вас есть такой класс специальных катаморфизмов, вы можете составить их.
Если мы рассмотрим семантическую эквивалентность, композиция двух катаморфизмов является катаморфизмом, когда первый является гиломорфизмом:
cata1 . hylo1 = cata2
Например (Haskell):
sum . map (^2) = foldl' (\x y -> x + y^2) 0