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

Question

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

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

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

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 получить какой-то класс типов для меня, который автоматически выполняет эту работу?

Answer 1

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

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

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

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

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

Затем мы можем уменьшить количество конструкторов до одного, используя Either вместо нескольких конструкторов. Ниже мы просто пишем инфикс + вместо 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

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

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

Кстати, эти изоморфизмы легко запомнить, если мы напишем (a,b) как продукт a*b, единица измерения () как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

Answer 2

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