默认情况下，Haskell数据类型是否是共代数？

Question

我正在努力理解F-代数，这篇文章讲得很清楚。我了解范畴论中对偶的概念，但我很难理解F-余代数（F-代数的对偶）与Haskell中惰性数据结构的关系。

F-代数用一个自函子和函数F a -> a来描述，如果你把F a看作一个表达式，把a看作求值该表达式的结果，那么这个函数就有意义了，正如链接的文章所解释的那样。

作为F-代数对偶的，相应的F-余代数函数将会是a -> F a。维基百科说F-余代数可用于创建无限惰性数据结构。那么，a -> F a函数如何允许我们创建无限惰性数据结构呢？另外，由于Haskell本质上是惰性的，大多数数据类型是否都是F-余代数而不是F-代数？F-代数不是惰性评估吗？

如果Haskell中的数据类型（或至少是那些能够生成无限数据的数据类型）基于F-余代数，例如对于列表，那么a -> F a函数是什么？列表的终端F-余代数是什么？

在Haskell中创建一个无限列表[1,2,3,4...]可能看起来像这样：

list = 1 : map (+ 1) list

这是否以某种方式使用了F-余代数？无限数据结构是否需要懒惰求值和递归的概念，以及使用F-余代数？我在这里漏掉了什么吗？

- Nathan BeDell

Answer 1

一个余代数A -> F A可以用来剥离（可能是无限的）数据结构的外层。对于列表X，函子是F a = Maybe (X, a)，与代数视图中相同。在Haskell中，余代数的函数为：

headView :: [a] -> Maybe (a, [a])
headView [] = Nothing
headView (x:xs) = Just (x,xs)

unfoldr是对应于该余代数的展开函数，就像foldr是对应于该代数的折叠函数。

如果您将[a]视为列表或程序描述的类型，而不是列表类型，则可以使用必然有限的描述构造（看似）无限的值。

正如您所看到的，Haskell列表既是F-代数又是F-余代数。这是可能的，因为Haskell实际上并不一致。您可以折叠展开，并获得无限循环。像Coq和Agda这样的语言明确区分数据类型（F-代数）和共数据类型（F-余代数）。在这些语言中，您有两种列表类型，代数的List和余代数的Colist。

- Twan van Laarhoven

---

那么，Haskell是否不一致，因为它允许展开生成无限数据结构？（从而导致折叠一个展开不终止） - Nathan BeDell

在总体/一致/Turing不完备语言中展开的东西感觉像生成器：拥有无限的潜力，但它们需要一个“驱动程序”来移动。Haskell是不一致的，因为它允许您将展开视为折叠（统一初始代数和终极余代数），因此可以通过自身来驱动无限的事物。如果您熟悉Python生成器，则调用list时会发生类似的情况，这会在无限生成器上产生一些结果。 - J. Abrahamson