Есть ли у каждого типа уникальный катаморфизм?

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

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

Например, я просто составил этот глупый тип, без реальной концепции того, что его структура "означает", и вывел для него катаморфизм. Я не вижу другого способа, которым я мог бы определить общую цель для этого типа:

data X a b f = A Int b
             | B
             | C (f a) (X a b f)
             | D a

xCata :: (Int -> b -> r)
      -> r
      -> (f a -> r -> r)
      -> (a -> r)
      -> X a b f
      -> r
xCata a b c d v = case v of
  A i x -> a i x
  B -> b
  C f x -> c f (xCata a b c d x)
  D x -> d x

Мой вопрос в том, имеет ли каждый тип уникальный катаморфизм (до переупорядочения аргументов)? Или существуют контрпримеры: типы, для которых нельзя определить катаморфизм, или типы, для которых существуют два различных, но одинаково приемлемых катаморфизма? Если нет контрпримеров (т.е. Катаморфизм для типа является уникальным и тривиально выводимым), можно ли получить GHC для получения какой-то спецификации для меня, которая автоматически выполняет эту drudgework?

Ответ 1

Катаморфизм, связанный с рекурсивным типом, может быть получен механически.

Предположим, что у вас есть рекурсивно определенный тип, имеющий несколько конструкторов, каждый из которых имеет свою собственную судьбу. Я возьму пример OP.

data X a b f = A Int b
             | B
             | C (f a) (X a b f)
             | D a

Затем мы можем переписать один и тот же тип, заставив каждую из них быть одной, невзирая на все. Аргумент 0 (B) становится единым, если мы добавим единичный тип ().

data X a b f = A (Int, b)
             | B ()
             | C (f a, X a b f)
             | D a

Затем мы можем уменьшить количество конструкторов до единицы, используя Either вместо нескольких конструкторов. Ниже мы просто пишем infix + вместо Either для краткости.

data X a b f = X ((Int, b) + () + (f a, X a b f) + a)

На уровне термина мы знаем, что мы можем переписать любое рекурсивное определение как форма x = f x where f w = ..., записывающая явное уравнение фиксированной точки x = f x. На уровне типа мы можем использовать тот же метод рекурсивным рекурсивным типам.

data X a b f   = X (F (X a b f))   -- fixed point equation
data F a b f w = F ((Int, b) + () + (f a, w) + a)

Теперь отметим, что мы можем автокопировать экземпляр функтора.

deriving instance Functor (F a b f)

Это возможно, потому что в исходном типе каждая рекурсивная ссылка только в положительной позиции. Если это не выполняется, делая F a b f не функтором, то мы не можем иметь катаморфизм.

Наконец, мы можем написать тип cata следующим образом:

cata :: (F a b f w -> w) -> X a b f -> w

Это тип OP xCata? Это. Нам нужно применить только некоторые изоморфизмы типа. Мы используем следующие алгебраические законы:

1) (a,b) -> c ~= a -> b -> c          (currying)
2) (a+b) -> c ~= (a -> c, b -> c)
3) ()    -> c ~= c

Кстати, легко запомнить эти изоморфизмы, если мы пишем (a,b) как произведение a*b, unit () как 1 и a->b как мощность b^a. Действительно, они становятся 1) c^(a*b) = (c^a)^b , 2) c^(a+b) = c^a*c^b, 3) c^1 = c.

В любом случае, давайте начнем переписывать часть F a b f w -> w, только

   F a b f w -> w
=~ (def F)
   ((Int, b) + () + (f a, w) + a) -> w
=~ (2)
   ((Int, b) -> w, () -> w, (f a, w) -> w, a -> w)
=~ (3)
   ((Int, b) -> w, w, (f a, w) -> w, a -> w)
=~ (1)
   (Int -> b -> w, w, f a -> w -> w, a -> w)

Рассмотрим теперь полный тип:

cata :: (F a b f w -> w) -> X a b f -> w
     ~= (above)
        (Int -> b -> w, w, f a -> w -> w, a -> w) -> X a b f -> w
     ~= (1)
           (Int -> b -> w)
        -> w
        -> (f a -> w -> w)
        -> (a -> w)
        -> X a b f
        -> w

Что действительно (переименование w=r) желаемого типа

xCata :: (Int -> b -> r)
      -> r
      -> (f a -> r -> r)
      -> (a -> r)
      -> X a b f
      -> r

"Стандартная" реализация cata равна

cata g = wrap . fmap (cata g) . unwrap
   where unwrap (X y) = y
         wrap   y = X y

Требуется некоторое усилие, чтобы понять из-за его общности, но это действительно предназначенный.

Об автоматизации: да, это может быть автоматизировано, по крайней мере частично. Существует пакет recursion-schemes для взлома, который позволяет один, чтобы написать что-то вроде

type X a b f = Fix (F a f b)
data F a b f w = ...  -- you can use the actual constructors here
       deriving Functor

-- use cata here

Пример:

import Data.Functor.Foldable hiding (Nil, Cons)

data ListF a k = NilF | ConsF a k deriving Functor
type List a = Fix (ListF a)

-- helper patterns, so that we can avoid to match the Fix
-- newtype constructor explicitly    
pattern Nil = Fix NilF
pattern Cons a as = Fix (ConsF a as)

-- normal recursion
sumList1 :: Num a => List a -> a
sumList1 Nil         = 0
sumList1 (Cons a as) = a + sumList1 as

-- with cata
sumList2 :: forall a. Num a => List a -> a
sumList2 = cata h
   where
   h :: ListF a a -> a
   h NilF        = 0
   h (ConsF a s) = a + s

-- with LambdaCase
sumList3 :: Num a => List a -> a
sumList3 = cata $ \case
   NilF      -> 0
   ConsF a s -> a + s

Ответ 2

Катаморфизм (если он существует) уникален по определению. В теории категорий катаморфизм обозначает уникальный гомоморфизм из начальной алгебры в некоторую другую алгебру. Насколько я знаю в Haskell, все катаморфизмы существуют, потому что типы Haskell образуют декартову замкнутую категорию, где существуют конечные объекты, все продукты и все экспоненты. Смотрите также сообщение в блоге Бартоша Милевского о F-алгебрах, которое дает хорошее введение в тему.