haskell数据类型是否默认为共代数？

Question

我正试着把我的头放在F-代数上，这篇文章做得很好。我理解范畴中对偶的概念，但我很难理解F-余代数(F-代数的对偶)与Haskell中的惰性数据结构的关系。

F-代数是用一个具有函数的内切函子描述的:f a -> a，如果你把F看作表达式的话，这是有意义的，而a是计算该表达式的结果，正如链接文章所解释的。

作为F-代数的对偶，F-余代数的对应函数是-> F_ a，维基百科说F-余代数可以用来建立无限的、懒惰的数据结构。一个函子的-> F如何允许一个人创建无限的、懒惰的数据结构？同时，考虑到这一点，既然Haskell处于核心懒惰状态，那么Haskell F-余代数中的大多数数据类型是否代替了F-代数？F-代数不是懒散的求值吗？

例如，如果数据类型(或者至少是那些具有无限数据能力的数据类型)是基于Haskell中的F-余代数，那么列表的-> F a函数是什么？列表的终端F-余代数是什么？

列一个无限的列表.在Haskell可能是这样的：

list = 1 : map (+ 1) list

这用了F-余代数吗？无限数据结构是否需要在使用F-余代数的同时使用延迟求值和递归的概念？我是不是漏掉了什么？

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。