haskell - 编译器如何确定仿函数的固定点以及 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 的不动点，即 List，以计算其长度。

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

我有两个困惑。一、Haskell编译器怎么知道List是 ListF 的不动点？我从概念上知道它是，但是编译器怎么知道，即，如果我们定义另一个与 List 相同的 List'，我敢打赌编译器不会自动推断 List' 也是 ListF 的不动点，或者确实它？ (我会很惊讶)。

其次，由于 cata lenAlg 的递归性质，它总是试图 unFix 数据构造函数的外层以暴露函数的内层(顺便说一下，我的这种解释是否正确？)。但是，如果我们已经在叶子节点，我们怎么能调用这个函数呢？

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 的定义，在叶子上调用 fmap (cata lenAlg)，在这种情况下是 NilF，将返回 NilF。

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

我会接受@n.m. 的回答，因为它直接解决了我的第一个(更大的)问题，但我确实喜欢所有三个答案。非常感谢您的帮助!

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))

这里有些不对劲。问题是我们忘记做 unFix 的相反操作。滚动ListF备份到常规列表中。我会调用这个函数

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

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

我要切换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

另见 my other answer关于变质。