haskell - 默认情况下，haskell 数据类型是协代数吗？

Question

我正在尝试了解 F 代数和 this article做得很好。我理解范畴论中对偶的概念，但我很难理解 F-coalgebras(F-algebras 的对偶)如何与 Haskell 中的惰性数据结构相关联。

F-代数是用具有以下功能的内仿函数来描述的:F a -> a，如果您将 F a 视为一个表达式，并且 a 是对该表达式求值的结果，那么这是有道理的，正如链接文章所解释的那样。

作为 F 代数的对偶，F 代数的对应函数是 a -> F a。 Wikipedia说 F-coalgebras 可以用来创建无限的惰性数据结构。 a -> F a 函数如何允许创建无限的惰性数据结构？此外，考虑到这一点，由于 Haskell 的核心是惰性的，Haskell F-coalgebras 中的大多数数据类型是不是 F-algebras？ F-代数不是惰性求值吗？

如果数据类型(或至少能够处理无限数据的数据类型)基于 Haskell 中的 F 代数，例如，列表的 a -> F a 函数是什么？列表的终端 F 代数是什么？

在 Haskell 中创建一个无限列表 [1,2,3,4...] 可能如下所示:

list = 1 : map (+ 1) list

这是否以某种方式使用 F 代数？无限数据结构在使用 F 代数的同时需要惰性求值和递归的概念吗？我在这里错过了什么吗？

Answer 1

一个代数A -> F A可用于剥离(可能是无限的)数据结构的外层。对于 X 的列表, 仿函数是 F a = Maybe (X, a) ，与代数 View 中的相同。在haskell中，余代数的函数是

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

unfoldr是对应于这个余代数的展开，就像 foldr是对应于这个代数的倍数。

如果你考虑 [a]不是作为列表的类型，而是作为列表或程序的描述类型，那么这允许您构造(看似)无限的值，只是具有必然的有限描述。

如您所见，Haskell 列表看起来既像 F 代数又像 F 代数。这是可能的，因为 Haskell 实际上并不一致。您可以折叠展开，并获得无限循环。像 coq 和 agda 这样的语言明确区分了数据类型(F-algebras)和 codata 类型(F-coalgebras)。在这些语言中，您有两种列表类型，一种是代数 List和一个代数 Colist .