为什么代数类型只是初始代数(反之亦然)？

Question

在recursion-schemes包中我们可以表达一个(严格正)代数数据类型的事实

1. 有一个签名仿函数, f
2. 是最初的 - f代数,和
3. 是最后的f代数

例如,我们可以[a]使用以下代码执行此操作

-- (1) define and declare the signature functor, here called Base

data instance Prim [a] x = Nil | Cons a x deriving Functor
type instance Base [a] = Prim [a]

-- (2) demonstrate the initial algebra
instance Foldable [a] where
  project []     = Nil
  project (a:as) = Cons a as

-- (3) demonstrate the final coalgebra
instance Unfoldable [a] where
  embed Nil         = []
  embed (Cons a as) = a:as

值得注意的是,对于我们有(1),(2)和(3)的任何类型,我们应该让那些(project, embed)证人具有同构性.

我的理解是,大型数据类型(或至少是严格肯定的数据类型)总是某些签名函子的最终/初始co /代数 - 事实上,它们总是两者兼而有之.

所以我的问题是:为什么有Foldable和Unfoldable作为单独的类？数据类型何时只是一个或另一个？

目前我可以想象这对于只想提供折叠或展开界面的抽象数据类型可能很有价值,但是还有其他时间吗？

Answer 1

这可能不是您的问题的答案,但严格的正Haskell数据类型是初始代数并不是真的.这样做的原因是,即使在Haskell的整个子集中(这是我们在推理时想要的工作!),您也拥有无限的数据.

例如,无限列表的折叠是部分的.