CodataType真的是终端代数吗？

Question

考虑一下“类型的类别”，类似于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)解释为递归操作，在给定G中定义的任何初始值和任何步进函数的情况下，该等式本质上断言函数m的惟一存在性，这就需要一个行为良好的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定义中的任何一个，我再也看不到任何定义良好的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-代数不存在。codatatype流（或无限列表）的理论建模（如果有的话）不能基于函子t(t)=1+a*t的不存在的终端代数。

非常感谢上面故事中任何瑕疵的暗示。

Answer 1

（2）终端代数定义同数据类型。

这是不对的，codataType是终端余代数。对于T函子，余代数是x和f::x->tx的类型。(x1,f1)和(x2,f2)之间的t-余代数态性是g::x1->x2，使得fmap g。f1=f2。g。使用这个定义，终端t-algebra定义了可能无限的列表（所谓的“colists”），而结束由unfold函数见证：

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

但是请注意，终端t-algebra确实存在：它只是Unit类型和常数函数t unit->Unit（对于任何t，它都是终端代数）。但这对于编写程序来说并不是很有趣。