问题标签 [coinduction]

（免责声明：我不是 100% 确定 codatatype 是如何工作的，尤其是在不涉及终端代数时）。

考虑“类型的类别”，类似于Hask，但可以进行任何适合讨论的调整。在这样一个类别中，据说（1）初始代数定义数据类型，（2）终端代数定义余数据类型。

我正在努力说服自己相信（2）。

考虑函子T(t) = 1 + a * t。我同意初始的T-algebra 是明确定义的，并且确实定义[a]了 的列表a。根据定义，初始T-algebra 是一个 typeX和一个 function f :: 1+a*X -> X，因此对于任何其他 typeY和 function 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代数的定义与初始代数的定义相同，只是m现在是类型X -> Y并且方程现在变为m . g = f . T(m)。据说这应该定义一个潜在的无限列表。

我同意这有时是真的。例如，当像以前一样g :: Unit + (Unit, Int) -> Int定义时，则表现为和。对于非负数，应该是一个有限的单位列表。对于任何负数，应该是无限长的。可以验证上面的等式对于这样的和成立。() -> 0 | (_,n) -> n+1mm(0) = ()m(n+1) = Cons () m(n)nm(n)nm(n)gm

但是，对于以下两个修改后的定义中的任何一个g，我再也看不到任何明确定义m的了。

首先，when gis 又() -> 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任何东西，所以方程没有明确定义。

其次，wheng又是类型g :: Unit + (Unit, Int) -> Int，但被定义为常数零函数g _ = 0，m必须满足m(g(())) = Nil和m(g(((),i))) = Cons () m(g(i))，这是矛盾的，因为它们的左手边是相同的，都是m(0)，而右手边永远不会相同。

总之，有-T代数没有态射到假定的终端T-代数中，这意味着终端-T代数不存在。余数据类型 Stream （或无限列表）的理论建模，如果有的话，不能基于 functor 的不存在终端代数T(t) = 1 + a * t。

非常感谢上面故事中任何缺陷的暗示。