Когда в состав катаморфизмов входит катаморфизм?

Ответ 1

Когда состав (сгиб 2 г). (fold1 f) :: μF1 → А катаморфизм?

Когда существует F1 -algebra h :: F1 A → A такой, что fold1 h = fold2 g. fold1 f 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 и ga → a соответственно) и значение типа fa, и ему необходимо получить значение типа a. Как бы Вы это сделали? Чтобы получить значение типа a ваша единственная надежда - применить функцию типа ga → a, но тогда мы застряли: у нас нет средств для преобразования значения типа fa в значение типа ga, не так ли?

Я не уверен, имеет ли это какое-либо значение для ваших целей, но пример условия, при котором можно составить катаморфизм, - это если мы имеем морфизм от результата второго ката до фиксированной точки второго функтора:

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

Ответ 2

(Отказ от ответственности: это выходит за рамки моей компетенции. Я считаю, что я прав (с предостережениями, предоставленными в разных точках), но... убедитесь сами.)

Катаморфизм можно рассматривать как функцию, заменяющую конструкторы типа данных другими функциями.

(В этом примере я буду использовать следующие типы данных:

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

Но это не так. Например, если существуют g1 g2 такие, что g (f a b..) = f (g1 a) (g2 b) .., это также работает.

Отсюда, как я ожидаю, правила будут просто беспорядочными.

Ответ 3

Катаморфизмы деконструируют структуру данных в значение результата. Таким образом, в целом, когда вы применяете катаморфизм, результат - это нечто совершенно иное, и вы не можете применить к нему еще один катаморфизм.

Например, функция, суммирующая все элементы [Int], является катаморфизмом, но результат Int. Нет способа применить к нему еще один катаморфизм.

Однако некоторые специальные катаморфизмы создают результат того же типа, что и вход. Одним из таких примеров является map f (для некоторой заданной функции f). Хотя он деконструирует исходную структуру, он также создает новый список в качестве результата. (Фактически, map f можно рассматривать как как катаморфизм, так и как anamorphism.) Итак, если у вас есть такой класс специальных катаморфизмов, вы можете составить их.

Ответ 4

Если мы рассматриваем семантическую эквивалентность, то состав двух катаморфизмов является катаморфизмом, когда первый является хиломорфизмом:

cata1 . hylo1 = cata2

Например (Haskell):

sum . map (^2) = foldl' (\x y -> x + y^2) 0