编译器如何计算出仿函数的固定点以及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

根据catamorphism的定义,可以将以下函数应用于ListF的固定点,即List,以计算其长度.

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

我有两个困惑.首先,如何Haskell编译知道名单是THE LISTF的固定点？我从概念上知道它是,但是编译器如何知道,即,如果我们定义另一个列表,那就是与List相同的一切,我打赌编译器不会自动推断出List'也是ListF的固定点,或者它？(我会感到惊讶).

其次,由于cata lenAlg的递归性质,它总是试图取消修复数据构造函数的外层以暴露仿函数的内层(我的解释是否正确？).但是,如果我们已经在叶子上,我们怎么能调用这个函数调用呢？

fmap (cata lenAlg) Nil

举个例子,有人可以帮助为下面的函数调用写一个执行跟踪来澄清吗？

cata lenAlg Cons 1 (Cons 2 Nil)

我可能遗漏了一些显而易见的事情,但是我希望这个问题对于其他有类似困惑的人来说仍然有意义.

---

回答总结

---

@nm回答了我的第一个问题,指出为了让Haskell编译器弄清楚Functor A是Functor B的一个固定点,我们需要明确.在这种情况下,它是

type List e = Fix (ListF e)

@luqui和@Will Ness指出,在叶子上调用fmap(cata lenAlg),在这种情况下是NilF,由于fmap的定义,将返回NilF.

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

我接受@ nm的答案,因为它直接解决了我的第一个(更大的)问题,但我确实喜欢这三个答案.非常感谢您的帮助!

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

另见我关于catamorphisms的其他答案.

Answer 2

“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，您需要：

• 定义一个Functorfor的实例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

成功！

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