Syl*_*ert 13 haskell type-systems category-theory coinduction
（免责声明：我不是 100% 确定 codatatype 是如何工作的，特别是在不涉及终端代数时）。
考虑“类型类别”，类似于Hask，但进行了适合讨论的任何调整。在这样的类别中，据说（1）初始代数定义数据类型，（2）终端代数定义协数据类型。
我正在努力说服自己相信（2）。
考虑函子T(t) = 1 + a * t。我同意初始T代数是明确定义的并且确实定义了[a]， 的列表a。根据定义，初始的T-algebra 是一个类型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与初始代数相同，只是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。
非常感谢上述故事中任何缺陷的暗示。
And*_*ács 15
(2) 终结代数定义了辅助数据类型。
这是不对的，codatatypes 是终端余代数。对于你的函子来说，余代数是一种与 一起的T类型。和之间的-代数态射是这样的。使用这个定义，终结代数定义了可能无限的列表（所谓的“colists”），并且终结性由函数见证：xf :: x -> T xT(x1, f1)(x2, f2)g :: x1 -> x2fmap g . f1 = f2 . gTunfold
unfold :: (x -> Unit + (a, x)) -> x -> Colist a
请注意，终端T- 代数确实存在：它只是Unit类型和常量函数T Unit -> Unit（这可以作为任何 的终端代数T）。但这对于编写程序来说并不是很有趣。
据说 (1) 初始代数定义数据类型，(2) 终端代数定义辅助数据类型。
关于第二点，实际上是说终端余代数定义了协数据类型。
数据类型t由其构造函数和折叠定义。
F t -> t（例如，Peano 构造函数O : nat S : Nat -> Nat被收集为单个函数in : Unit + Nat -> Nat）。fold f : t -> x然后，折叠给出任何代数的变形f : F x -> x（对于 nats，fold : ((Unit + x) -> x) -> Nat -> x）。协同数据类型t由其析构函数和展开函数定义。
t -> F t（例如，流有两个析构函数head : Stream a -> a和tail : Stream a -> Stream a，并且它们被收集为单个函数out : Stream a -> a * Stream a）。unfold f : x -> t任何代数的变形f : x -> F x（对于流，unfold : (x -> a * x) -> x -> Stream a）。\n\n（免责声明：我不是 100% 确定 codatatype 是如何工作的，特别是在不涉及终端代数时）。
\n
协同数据类型（codata type），或共归纳数据类型，只是一种通过其消除而不是通过引入来定义的类型。
\n似乎有时使用终端代数（非常令人困惑）来指代最终的 coalgebra，这实际上定义了 codata 类型。
\n\n\n考虑上面定义的相同函子 T。终端 T 代数的定义与初始代数相同，只是 m 现在是类型 X -> Y 并且方程现在变为 m 。g = f 。Tm值）。据说这应该定义一个潜在的无限列表。
\n
所以我认为这就是你\xe2\x80\x99出错的地方： \xe2\x80\x9c m \xe2\x88\x98 g = f \xe2\x88\x98 T ( m )\xe2\x80\x9d 应该是反转，读取 \xe2\x80\x9c T ( m ) \xe2\x88\x98 f = g \xe2\x88\x98 m \xe2\x80\x9d。也就是说，最终的余代数由载体集S和映射g : S \xe2\x86\x92 T ( S ) 定义，使得对于任何其他余代数 ( R , f : R \xe2\x86\x92 T ( R )) 存在唯一映射m : R \xe2\x86\x92 S使得T ( m ) \xe2\x88\x98 f = g \xe2\x88\x98 m。
\nm是由映射唯一递归定义的，Left ()每当f映射到Left ()，并且每当f映射到Right (x, m xs)时，它都会返回，即 it\xe2\x80\x99s 将余代数分配给最终余代数的唯一态射，并表示唯一的变形/展开这种类型的流，应该很容易让自己相信，它实际上是一个可能为空且可能为无限的流。Right (x, xs)