编译器如何确定一个函数对象的不动点，以及 cata 在叶子节点上是如何工作的？

Question

我感觉理解了函数子的不动点这个抽象概念，但我仍在苦苦思索如何准确实现它及其在Haskell中的卡塔范畴。例如，如果我按照《程序员的范畴论》第359页的定义，定义以下代数：

-- (Int, LiftF e Int -> Int)

data ListF e a = NilF | ConsF e a

lenAlg :: ListF e Int -> Int
lenAlg (ConsF e n) -> n + 1
lenAlg NilF = 0

按照范畴论的定义，我们可以将以下函数应用于ListF的不动点，也就是一个列表，来计算其长度。

cata lenAlg :: [e] -> Int
cata lenAlg = lenAlg . fmap (cata lenAlg) . unFix

我有两个疑惑。首先，Haskell编译器如何知道List是ListF的不动点？我知道从概念上讲它确实是，但编译器是怎么知道的？也就是说，如果我们定义了另一个与List完全相同的List'，我打赌编译器不会自动推断List'也是ListF的不动点，对吗？（我会感到惊讶的）。

其次，由于cata lenAlg具有递归性质，它总是尝试去除数据构造函数的最外层，以暴露functor的内部层（顺��问一句，我的解释是否正确？）。但是，如果我们已经在叶子节点上，我们怎么调用这个函数呢？

fmap (cata lenAlg) Nil

举个例子，有人可以帮忙写一个执行跟踪来澄清以下函数调用吗？

cata lenAlg Cons 1 (Cons 2 Nil)

我可能漏掉了一些显而易见的东西，但我希望对于其他有相似困惑的人来说，这个问题仍然是有意义的。

---

回答摘要

---

@n.m. 通过指出为了让 Haskell 编译器弄清楚 Functor A 是 Functor B 的不动点，我们需要明确表达。在这种情况下，表达式为：

type List e = Fix (ListF e)

@luqui和@Will Ness指出，在叶子节点上调用fmap（cata lenAlg）会返回NilF，因为fmap的定义如此。

-- f :: a -> b
fmap f (ConsF e a) = ConsF e (f b)
fmap f NilF        = NilF

我会接受 @n.m. 的答案，因为它直接回答了我的第一个（更重要的）问题，但我也喜欢所有三个答案。非常感谢你们的帮助！

- learnereveryday

Answer 1

编译器了解 ListF e 和 [e] 之间的关系的唯一方法是您告诉它。 您没有提供足够的上下文来准确回答如何做到这一点，但我可以推断出 unFix 具有以下类型：

unFix :: [e] -> ListF e [e]

也就是说，它展开了顶层。 unFix 可能更通用，例如在 recursion-schemes 中，一个类型族被用于将数据类型与其基础函子相关联。但这就是这两种类型相连接的地方。

---

至于你的第二个问题，你需要更清楚地表明何时拥有列表以及何时拥有一个 ListF。它们完全不同。

fmap (cata lenAlg) Nil

在这里，您正在映射的函数对象是 ListF e，可以选择任何您喜欢的 e。也就是说，它是这个fmap：

fmap :: (a -> b) -> ListF e a -> ListF e b

如果您自己实现instance Functor (ListF e)（这总是一个不错的练习），并成功编译，您会发现Nil必须映射为Nil，因此cata lenAlg实际上没有起到任何作用。

让我们看一下Cons 1 (Cons 2 Nil)的类型：

Nil                 :: ListF e a
Cons 2 Nil          :: ListF Int (ListF e a)
Cons 1 (Cons 2 Nil) :: ListF Int (ListF Int (ListF e a))

这里似乎出了些问题。麻烦在将 ListF 回滚到常规列表时，我们忘记执行与 unFix 相反的操作。我将称此函数为

roll :: ListF e [e] -> [e]

现在我们有：

Nil                                      :: ListF e a
roll Nil                                 :: [e]
Cons 2 (roll Nil)                        :: ListF Int [Int]
roll (Cons 2 (roll Nil))                 :: [Int]
Cons 1 (roll (Cons 2 (roll Nil)))        :: ListF Int [Int]
roll (Cons 1 (roll (Cons 2 (roll Nil)))) :: [Int]

现在类型保持得很小，这是一个好兆头。对于执行跟踪，让我们注意到unFix . roll = id，无论它们如何工作。重要的是要注意到这一点。

fmap f (Cons a b) = Cons a (f b)
fmap f Nil        = Nil

也就是说，在 ListF 上的 fmap 只是将函数应用于类型的“递归部分”。

我将切换 Cons 的情况，使跟踪信息更加可读，即 lenAlg (ConsF e n) = 1 + n。仍然有些混乱，祝你好运。

cata lenAlg (roll (Cons 1 (roll (Cons 2 (roll Nil)))))
(lenAlg . fmap (cata lenAlg) . unFix) (roll (Cons 1 (roll (Cons 2 (roll Nil)))))
lenAlg (fmap (cata lenAlg) (unFix (roll (Cons 1 (roll (Cons 2 (roll Nil)))))))
lenAlg (fmap (cata lenAlg) (Cons 1 (roll (Cons 2 (roll Nil)))))
lenAlg (Cons 1 (cata lenAlg (roll (Cons 2 (roll Nil)))))
1 + cata lenAlg (roll (Cons 2 (roll Nil)))
1 + (lenAlg . fmap (cata lenAlg) . unFix) (roll (Cons 2 (roll Nil)))
1 + lenAlg (fmap (cata lenAlg) (unFix (roll (Cons 2 (roll Nil)))))
1 + lenAlg (fmap (cata lenAlg) (Cons 2 (roll Nil)))
1 + lenAlg (Cons 2 (cata lenAlg (roll Nil)))
1 + 1 + cata lenAlg (roll Nil)
1 + 1 + (lenAlg . fmap (cata lenAlg) . unFix) (roll Nil)
1 + 1 + lenAlg (fmap (cata lenAlg) (unFix (roll Nil)))
1 + 1 + lenAlg (fmap (cata lenAlg Nil))
1 + 1 + lenAlg Nil
1 + 1 + 0
2

请参见有关Haskell中的catamorphisms的我的其他答案。

- luqui

Answer 2

不，unFix暴露了结构，然后fmap f在其上应用一个函数f。如果它是叶子节点，fmap f将执行其为叶子定义的操作-即，无操作。正如通常在Haskell的基于情况的定义中一样，是fmap“知道”如何处理每种情况的。

Fix (ListF e) = ListF e (Fix (ListF e)) 
              = NilF | ConsF e (Fix (ListF e))

将 Fix (ListF e) 重命名为 Listof e，则我们得到：

Listof     e  = NilF | ConsF e (Listof e) 

Listof e是一种递归类型。ListF e r是一种非递归类型。Fix将其转换为递归类型。ListF e作为Functor意味着fmap处理肉，ListF e是这个“水果”的“硬外壳”。

data ListF e a = NilF | ConsF e a

newtype Fix f = X { unFix    :: (f       (Fix f)) }

-- unFix ::    Fix f          -> f       (Fix f        )
-- unFix (_ :: Fix (ListF e)) :: ListF e (Fix (ListF e))

lenAlg :: ListF e Int -> Int
lenAlg (ConsF e n) = n + 1
lenAlg NilF        = 0

instance Functor (ListF e) where
    -- fmap :: (a -> b) -> (ListF e a) -> (ListF e b)
    fmap f NilF        = NilF
    fmap f (ConsF e r) = ConsF e (f r)

cata :: (ListF e Int -> Int) -> Fix (ListF e) -> Int
cata lenAlg x = (lenAlg . fmap (cata lenAlg) . unFix) x
              =  lenAlg ( fmap (cata lenAlg) ( unFix  x ))
--------
        x       ::       Fix (ListF e)
        unFix x ::            ListF e (Fix (ListF e))
        fmap (cata lenAlg) :: ListF e (Fix (ListF e)) -> ListF e (Int)
              cata lenAlg  ::          Fix (ListF e)  ->          Int

        fmap (cata lenAlg)   (unFix  x              ) :: ListF e  Int 
 lenAlg (_                                            :: ListF e  Int ) :: Int

看到了吗？所有的电线都连接到了它们应该连接的位置。fmap递归地转换内部部分r，然后lenAlg代数应用一个最后的转换，一个最后一步将其所有内部部分折叠成一个r递归result的结构中。从而产生最终的result。

---

作为一个具体的例子，对于包含两个数字1和2的列表，我们有

-- newtype Fix f  = X { unFix :: (f      (Fix f         )) }
--             _\_______       ____\____      _\________
onetwo :: Fix (ListF Int) -- ~ ListF Int (Fix (ListF Int))
onetwo = X (ConsF 1
                  (X (ConsF 2
                            (X NilF))))

cata lenAlg :: Fix (ListF e) -> Int
cata lenAlg    onetwo
  = {- definition of cata   -}
    lenAlg . fmap (cata lenAlg) . unFix  $ onetwo
  = {- definition of onetwo -}
    lenAlg . fmap (cata lenAlg) . unFix  $ 
                           X (ConsF 1 (X (ConsF 2 (X NilF))))
  = {- definition of unFix  -}
    lenAlg . fmap (cata lenAlg) $ 
                              ConsF 1 (X (ConsF 2 (X NilF)))
  = {- definition of fmap   -}
    lenAlg $ ConsF 1 (cata lenAlg     (X (ConsF 2 (X NilF))))
  = {- definition of lenAlg -}
    (+ 1)  $          cata lenAlg     (X (ConsF 2 (X NilF)))
  = {- definition of cata   -}
    (+ 1)  $ lenAlg . fmap (cata lenAlg) . unFix $ 
                                       X (ConsF 2 (X NilF))
  = {- definition of unFix  -}
    (+ 1) $ lenAlg . fmap (cata lenAlg) $ ConsF 2 (X NilF)
  = {- definition of fmap   -}
    (+ 1) $ lenAlg $ ConsF 2 $ cata lenAlg        (X NilF)
  = {- definition of lenAlg -}
    (+ 1) $ (+ 1)  $           cata lenAlg        (X NilF)
  = {- definition of cata   -}
    (+ 1) $ (+ 1)  $ lenAlg . fmap (cata lenAlg) . unFix $ 
                                                  (X NilF)
  = {- definition of unFix  -}
    (+ 1) $ (+ 1)  $ lenAlg . fmap (cata lenAlg) $   NilF
  = {- definition of fmap   -}
    (+ 1) $ (+ 1)  $ lenAlg $                        NilF
  = {- definition of lenAlg -}
    (+ 1) $ (+ 1)  $ 0
  = (+ 1) $ 1
  = 2

同时，

squaringAlg :: ListF Int [Int] -> [Int]
squaringAlg (ConsF e r) = e*e : r
squaringAlg NilF        = []

filteringAlg :: (e -> Bool) -> ListF e [e] -> [e]
filteringAlg p (ConsF e r) | p e       = e : r
                           | otherwise = r
filteringAlg _ NilF                    = []

etc.

- Will Ness

---

你能详细解释一下为什么 Fix (ListF e) = ListF e (Fix (ListF e)) = NilF | ConsF e (Fix (ListF e)) 吗？根据 newtype Fix f = Fix (f (Fix f)) 的定义，Fix 数据构造函数不应该被应用于 ((ListF e) Fix (ListF e)) 吗？ - learnereveryday

我使用X作为数据构造函数，以避免混淆。 Fix是类型构造函数。因此，类型Fix（ListF e）符合定义newtype Fix f = X（f（Fix f）），其中类型参数f变为（ListF e）。因此，通过替换，我们得到类型f（Fix f）为ListF e（Fix（ListF e））。而ListF有两个数据构造函数情况。这就是我所说的那两个非正式的“方程式”的意思。 - Will Ness

主要的代码块都是真实的代码。你所要求的推导过程使用它，并且按照其定义一步一步地进行。 - Will Ness

“被接受的答案表明，为了让Haskell编译器确定Functor A是Functor B的不动点，我们需要明确表示。” 不，那个答案告诉你相反的事情：编译器什么也不知道。 “明确”这一点只是意味着我们必须显式地提供缺失的Functor实例。一个数学家看到这些定义后会得出结论，类型Fix f是类型f的类型级不动点。一个Haskell实现只是遵循定义，就像我在我的回答中展示的那样。对于它来说，类型Fix（ListF e）或ListF e（Fix（ListF e））只是另一种类型。 - Will Ness

"Fix" 只是另一种类型名称。它可以被命名为 "T"，对它来说都无所谓。 :) 数据构造函数也是如此，这就是我在那里使用 "X" 的原因。 - Will Ness

Answer 3

"List是ListF的不动点"是一种快速而松散的说法。虽然快速而松散的推理在道德上是正确的，但你始终需要记住那些乏味的正确事情。具体如下：

任何ListF e的最小不动点同构于[e]。

现在，"编译器"(顺便说一句，这是"Haskell语言"的一个快速且松散的说法)并不知道此类同构。你可以整日编写同构类型。

data []    x = []   | (:)   x ([]    x)    -- the imaginary built-in definition of []
data ListA x = NilA | ConsA x (ListA x)
data ListB x = NilB | ConsB x (ListB x)
data ListC x = NilC | ConsC x (ListC x)

并且编译器永远不会将它们视为“相同类型”。编译器也不知道ListF e的不动点与[e]相同，或者什么是不动点。如果你想使用这些同构，你需要通过编写一些代码（例如定义Data.Types.Isomorphic的实例），并在每次使用时明确指定同构来教导编译器！

考虑到这一点，让我们看一下您定义的cata函数。首先映入眼帘的是尝试定义类型签名的语法错误。让我们删除它，并在GHCi中定义这个函数（我更改了参数名称为f以避免混淆，并在ListF的定义中修正了一些拼写错误）。

Main> data ListF e a = NilF | ConsF e a
Main> let lenAlg :: ListF e Int -> Int
Main|     lenAlg (ConsF e n) = n + 1
Main|     lenAlg NilF = 0
Main|
Main>
Main> :m + Data.Fix
Main Data.Fix> cata f = f . fmap (cata f) . unFix
Main Data.Fix> :t cata
cata :: Functor f => (f b -> b) -> Fix f -> b
Main Data.Fix> :t cata lenAlg
cata lenAlg :: Functor (ListF e) => Fix (ListF e) -> Int

这段话的意思是，为了使用lenAlg，你需要：

• 为ListF e定义一个Functor实例
• 显式地使用Fix (ListF e)（它是ListF的一个不动点）。只是希望"ListF的不动点"存在是行不通的。没有魔法。

因此，让我们这样做：

Main Data.Fix> instance Functor (ListF e) where
Main Data.Fix|     fmap f NilF = NilF
Main Data.Fix|     fmap f (ConsF e a) = ConsF e (f a)
Main Data.Fix>
Main Data.Fix> :t cata lenAlg
cata lenAlg :: Fix (ListF e) -> Int

太好了，现在我们可以计算基于ListF的Fix-wrapped列表的长度。但是让我们先定义一些辅助定义。

Main Data.Fix> type List e = Fix (ListF e)
Main Data.Fix> nil = Fix (NilF)
Main Data.Fix> let infixr 7 ~~                   -- using an infix operator for cons
Main Data.Fix|     h ~~ t = Fix (ConsF h t)
Main Data.Fix|
Main Data.Fix>
Main Data.Fix> myList = (1::Int) ~~ 2 ~~ 3 ~~ 4 ~~ nil
Main Data.Fix> :t myList
myList :: Fix (ListF Int)

这是我们的“列表”（一个与[Int]同构的类型成员，确切地说）。让我们对它进行cata lenAlg操作：

Main Data.Fix> cata lenAlg myList
4

成功！

最重要的是编译器什么都不知道，你需要向它解释一切。

- n. m.