默认情况下haskell数据类型是否为co-algebras？

Question

我正试图绕过F-algebras,这篇文章做得非常好.我理解双重类别理论的概念,但我很难理解F-coalgebras(F-代数的对偶)如何与Haskell中的惰性数据结构相关.

F-代数用endofunctor描述,函数有:F a - > a,如果你把F a看作一个表达式就有意义,而a作为评估该表达式的结果,正如链接文章所解释的那样.

作为F-代数的对偶,F-余代数的相应函数将是 - > F a.维基百科说,F-coalgebras可以用来创建无限的,懒惰的数据结构.a - > F a functon如何创建无限的,懒惰的数据结构？另外,考虑到这一点,既然Haskell处于核心的懒惰状态,Haskell F-coalgebras中的大多数数据类型都是F-algebras？F-algebras没有被懒惰地评估？

如果数据类型(或至少是能够无限数据的数据类型)基于Haskell中的F-coalgebras,那么a - > F是一个列表函数,例如？列表的终端F-coalgebra是什么？

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

list = 1 : map (+ 1) list

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

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-代数)和codata类型(F-coalgebras)之间的区别明确.在这些语言中,您有两种列表类型,代数List和代数Colist.