11

最近我终于开始觉得我理解变态现象了。我在最近的一个答案中写了一些关于它们的内容，但简要地说，我会说一个类型的变态抽象了递归遍历该类型的值的过程，该类型的模式匹配被具体化为该类型具有的每个构造函数的一个函数. 虽然我欢迎对这一点或上面链接的我的答案中的较长版本进行任何更正，但我认为我或多或少地对此有所了解，这不是这个问题的主题，只是一些背景。

一旦我意识到传递给 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（直到参数重新排序）？或者是否有反例：不能定义变质的类型，或者存在两种不同但同样合理的变质的类型？如果没有反例（即，一个类型的变态是唯一的并且可以简单地派生），是否有可能让 GHC 为我派生某种类型类来自动完成这项繁重的工作？

4

2 回答 2

6

与递归类型相关的变质可以机械地推导出来。

假设您有一个递归定义的类型，具有多个构造函数，每个构造函数都有自己的数量。我会借用OP的例子。

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

然后，我们可以通过强制每个 arity 为一个来重写相同的类型，取消所有内容。B如果我们添加一个单位类型， Arity zero( ) 就会变成一()。

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

顺便说一下，如果我们写成 product 、 unit 和 power ，就很容易(a,b)记住a*b这些同构。确实他们变成了()1a->bb^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

由于其普遍性，需要一些努力才能理解，但这确实是预期的。

关于自动化：是的，这可以自动化，至少部分自动化。hackage 上有一个包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
于 2017-10-04T12:08:36.400 回答
2

根据定义，变质（如果存在）是唯一的。在范畴论中，变态表示从初始代数到其他代数的唯一同态。据我所知，Haskell 存在所有变态，因为 Haskell 的类型形成了一个笛卡尔封闭类别，其中存在终端对象、所有产品、总和和指数。另请参阅 Bartosz Milewski关于 F-algebras 的博客文章，该文章很好地介绍了该主题。

于 2019-06-21T07:12:58.273 回答