15

（免责声明：我不是 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。

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

4

3 回答 3

16

(2) 终结代数定义了余数据类型。

这是不对的， codatatypes 是终端colgebras。对于您的函子，余代数与 .一起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（这可以作为 any 的终端代数T）。但这对于编写程序并不是很有趣。

于 2021-11-26T19:48:16.150 回答
9

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

余数据类型或协导数据类型只是由它的消除而不是它的引入来定义的。

似乎有时使用终端代数（非常令人困惑）来指代最终的 colgebra ，这实际上定义了余数据类型。

考虑上面定义的相同的仿函数 T。终端 T 代数的定义与最初的相同，只是 m 现在是 X -> Y 类型，方程现在变成 m 。g = f 。Tm值）。据说这应该定义一个潜在的无限列表。

所以我认为这就是你出错的地方：“<em>m ∘ g = f ∘ T ( m )”应该颠倒过来，改为“<em>T( m ) ∘ f = g ∘ m ”。也就是说，最终的余代数由载体集S和映射g : S → T ( S ) 定义，使得对于任何其他余代数 ( R , f : R → T ( R )) 都有唯一的映射m : R → S使得T (米) ∘ f = g ∘米。

m由当f映射到和Left ()每当f映射到时返回的映射唯一地递归定义，即它是将余代数分配给其唯一态射到最终余代数，并表示这种类型的唯一变形/展开，应该容易说服自己实际上是一个可能是空的，可能是无限的流。Left ()Right (x, m xs)Right (x, xs)

于 2021-11-26T20:03:56.353 回答
8

据说（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）。

codatatypet由其析构函数和展开定义。

  • 析构函数可以用余代数建模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）。
于 2021-11-26T19:59:11.637 回答