每种类型都有独特的变形吗？

Question

最近我终于开始觉得我理解了catamorphisms.我在最近的一个回答中写了一些关于它们的内容,但简单地说,对于递归遍历该类型的值的过程,我会说类型抽象的一个变形,其中该类型的模式匹配在每个类型具有的构造函数中被赋予一个函数. .虽然我欢迎对这一点或上面链接的答案中的较长版本进行任何更正,但我认为我或多或少都有这种情况,这不是这个问题的主题,只是一些背景知识.

一旦我意识到你传递给一个catamorphism的函数完全对应于类型的构造函数,并且这些函数的参数同样对应于那些构造函数的字段的类型,所有这些都突然感觉很机械,我看不到有哪些替代实施的任何摆动空间.

例如,我只是编造了这种愚蠢的类型,没有关于它的结构"意味着什么"的真实概念,并为它导出了一个变形.我没有看到任何其他方式我可以定义这种类型的通用折叠:

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

我的问题是,每种类型都有一个独特的catamorphism(直到参数重新排序)？或者是否存在反例:可以定义没有变构的类型,或存在两种截然不同但同样合理的同态的类型？如果没有反例(即,一个类型的catamorphism是唯一的,并且可以简单地推导出来),是否有可能让GHC为我自动导出某种类型的类型来做这种苦差事？

Answer 1

与递归类型相关的变形可以机械地导出.

假设你有一个递归定义的类型,有多个构造函数,每个构造函数都有自己的arity.我会借用OP的例子.

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

然后,我们可以通过强制每个arity成为一个来重写相同的类型,从而解决所有问题.B如果我们添加单位类型,Arity zero()将变为1 ().

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

这是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,单位()为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-schemeshackage上有一个包可以写一些东西

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