haskell - 编译器如何找出仿函数的不动点以及 cata 如何在叶级工作？

我想理解仿函数不动点的抽象概念，但是，我仍在努力弄清楚它的确切实现及其在 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

根据 catamorphism 的定义，下面的函数可以应用于 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. 的答案，因为它直接解决了我的第一个(更大的)问题，但我确实喜欢所有三个答案。非常感谢您的帮助!

最佳答案

“List 是 ListF 的不动点”是一个又快又松的修辞格。而 fast and loose reasoning is morally correct ，你总是需要记住无聊的正确的事情。如下:
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 ，您需要:

为 Functor

定义一个 ListF e 的实例

显式使用 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

成功!

底线:编译器什么都不知道，你需要解释一切。