codatatypes真的是终端代数吗？
Are codatatypes really terminal algebras?
（免责声明：我不是 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.[=77= 的列表]
例如，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-代数不存在。 codatatype Stream（或无限列表）的理论建模（如果有的话）不能基于函子的不存在的终端代数 T(t) = 1 + a * t.
非常感谢以上故事中任何缺陷的暗示。
(2) terminal algebras define codatatypes.
这是不对的，余数据类型是终端 coalgebras。对于您的 T 函子，余数是 x 和 f :: x -> T x 类型。在 (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-代数确实存在：它只是 Unit 类型和常量函数 T Unit -> Unit （这可以作为任何终结符代数T)。但是这对于写程序来说并不是很有趣
it is said that (1) the initial algebras define datatypes, and (2) terminal algebras define codatatypes.
关于第二点，其实是说terminal coalgebras define codatatypes.
数据类型 t 由其构造函数和折叠定义。
- 构造函数可以通过代数建模
F t -> t（例如，Peano 构造函数 O : nat S : Nat -> Nat 被收集为单个函数 in : Unit + Nat -> Nat）。
- 折叠然后给出任何代数
f : F x -> x 的变质 fold f : t -> 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 ).
- 展开然后为任何余数
f : x -> F x（对于流，unfold : (x -> a * x) -> x -> Stream a）提供变形unfold f : x -> t。
(Disclaimer: I'm not 100% sure how codatatype works, especially when not referring to terminal algebras).
余数据类型或余归数据类型只是由其消除而不是其介绍.[=16=定义的类型]
似乎有时 terminal algebra 被用来（非常令人困惑）指代 final coalgebra，这实际上定义了一个编码数据类型。
Consider the same functor T defined above. The definition of the terminal T-algebra is the same as the initial one, except that m is now of type X -> Y and the equation now becomes m . g = f . T(m). It is said that this should define a potentially infinite list.
所以我认为这是你出错的地方：“m ∘ g = f ∘ T(m)”要倒过来读“T(m) ∘ f = g ∘ m”。也就是说，最终的余代数由载体集 S 和映射 g 定义： S → T(S) 这样对于任何其他余数 (R, f : R → T(R)) 有一个独特的地图m : R → S 这样 T(m) ∘ f = g ∘ m.
m 由 returns Left () 每当 f 映射到 Left (), 和 Right (x, m xs) 每当 f 映射到 Right (x, xs), 即它是余代数对其唯一态射赋值给最终余代数, 并表示唯一anamorphism/unfold 这种类型，应该很容易说服自己实际上是一个可能为空且可能为无限的流。
（免责声明：我不是 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.[=77= 的列表]
例如，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-代数不存在。 codatatype Stream（或无限列表）的理论建模（如果有的话）不能基于函子的不存在的终端代数 T(t) = 1 + a * t.
非常感谢以上故事中任何缺陷的暗示。
(2) terminal algebras define codatatypes.
这是不对的，余数据类型是终端 coalgebras。对于您的 T 函子，余数是 x 和 f :: x -> T x 类型。在 (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-代数确实存在：它只是 Unit 类型和常量函数 T Unit -> Unit （这可以作为任何终结符代数T)。但是这对于写程序来说并不是很有趣
it is said that (1) the initial algebras define datatypes, and (2) terminal algebras define codatatypes.
关于第二点，其实是说terminal coalgebras define codatatypes.
数据类型 t 由其构造函数和折叠定义。
- 构造函数可以通过代数建模
F t -> t（例如，Peano 构造函数O : natS : Nat -> Nat被收集为单个函数in : Unit + Nat -> Nat）。 - 折叠然后给出任何代数
f : F x -> x的变质fold f : t -> 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). - 展开然后为任何余数
f : x -> F x（对于流，unfold : (x -> a * x) -> x -> Stream a）提供变形unfold f : x -> t。
(Disclaimer: I'm not 100% sure how codatatype works, especially when not referring to terminal algebras).
余数据类型或余归数据类型只是由其消除而不是其介绍.[=16=定义的类型]
似乎有时 terminal algebra 被用来（非常令人困惑）指代 final coalgebra，这实际上定义了一个编码数据类型。
Consider the same functor T defined above. The definition of the terminal T-algebra is the same as the initial one, except that m is now of type X -> Y and the equation now becomes m . g = f . T(m). It is said that this should define a potentially infinite list.
所以我认为这是你出错的地方：“m ∘ g = f ∘ T(m)”要倒过来读“T(m) ∘ f = g ∘ m”。也就是说，最终的余代数由载体集 S 和映射 g 定义： S → T(S) 这样对于任何其他余数 (R, f : R → T(R)) 有一个独特的地图m : R → S 这样 T(m) ∘ f = g ∘ m.
m 由 returns Left () 每当 f 映射到 Left (), 和 Right (x, m xs) 每当 f 映射到 Right (x, xs), 即它是余代数对其唯一态射赋值给最终余代数, 并表示唯一anamorphism/unfold 这种类型，应该很容易说服自己实际上是一个可能为空且可能为无限的流。