haskell - 余数据类型真的是终端代数吗？

Question

(免责声明:我不是 100% 确定 codatatype 是如何工作的，尤其是在不涉及终端代数时)。
考虑“类型的类别”，例如 Hask但是进行任何适合讨论的调整。在这样一个类别中，据说(1)初始代数定义数据类型，(2)终端代数定义余数据类型。
我正在努力说服自己相信(2)。
考虑仿函数 T(t) = 1 + a * t .我同意最初的 T -代数定义明确，确实定义了[a] ，列表a .根据定义，初始 T -代数是一个类型X连同一个函数 f :: 1+a*X -> X , 这样对于任何其他类型 Y和功能 g :: 1+a*Y -> Y ，只有一个函数m :: X -> Y这样m . f = g . T(m) (其中 . 表示 Haskell 中的函数组合运算符)。与 f解释为列表构造函数，g初始值和阶跃函数，T(m)递归操作，方程本质上断言函数m的唯一存在给定 g 中定义的任何初始值和任何阶跃函数，这需要一个行为良好的基础 fold与基础类型一起，a 的列表.
例如，g :: Unit + (a, Nat) -> Nat可能是 () -> 0 | (_,n) -> n+1 , 在这种情况下 m定义长度函数，或 g可能是 () -> 0 | (_,n) -> 0 ，然后 m定义一个常数零函数。这里的一个重要事实是，无论 g , m总是可以唯一定义的，就像 fold不会对其论点施加任何约束，并且始终会产生独特的明确定义的结果。
这似乎不适用于终端代数。
考虑相同的仿函数 T定义如上。终端定义T -algebra 和最初的一样，除了 m现在是 X -> Y 类型方程现在变为 m . g = f . T(m) .据说这应该定义一个潜在的无限列表。
我同意这有时是真的。例如，当 g :: Unit + (Unit, Int) -> Int定义为 () -> 0 | (_,n) -> n+1像以前一样，m然后行为使得 m(0) = ()和 m(n+1) = Cons () m(n) .对于非负n , m(n)应该是一个有限的单位列表。对于任何负数n , m(n)应该是无限长的。可以验证，上面的等式对于这样的 g 成立。和 m .
使用以下两个修改后的 g 定义中的任何一个，但是，我没有看到任何明确定义的 m了。
一、当g又是() -> 0 | (_,n) -> n+1但类型为 g :: Unit + (Bool, Int) -> Int , m必须满足 m(g((b,i))) = Cons b m(g(i)) ，这意味着结果取决于 b .但这是不可能的，因为 m(g((b,i)))真的只是m(i+1)没有提到b无论如何，所以方程不是很好定义的。
二、当g又是 g :: Unit + (Unit, Int) -> Int 类型但被定义为常数零函数g _ = 0 , m必须满足 m(g(())) = Nil和 m(g(((),i))) = Cons () m(g(i)) ，这是矛盾的，因为它们的左手边是相同的，都是 m(0) , 而右手边永远不一样。
综上，有T -没有态射到假定终端的代数T -代数，这意味着终端T -代数不存在。余数据类型 Stream(或无限列表)的理论建模，如果有的话，不能基于仿函数 T(t) = 1 + a * t 的不存在终端代数。 .
非常感谢上面故事中任何缺陷的暗示。

Answer 1

(2) terminal algebras define codatatypes.

这是不对的，余数据类型是终端余代数。为您的T仿函数，代数是一种类型 x连同 f :: x -> T x .一个 T -(x1, f1) 之间的代数态射和 (x2, f2)是 g :: x1 -> x2这样fmap g . f1 = f2 . g .使用这个定义，终端 T -algebra 定义了可能无限的列表(所谓的“colists”)，并且unfold 见证了终结性。功能:

unfold :: (x -> Unit + (a, x)) -> x -> Colist a

请注意，终端 T -代数确实存在:它只是 Unit与常量函数 T Unit -> Unit 一起键入(这可以作为任何 T 的终端代数)。但这对于编写程序并不是很有趣。