codatatypes真的是終端代數嗎？

（免責宣告：我不是 100% 確定 codatatype 是如何作業的，尤其是在不涉及終端代數時）。

考慮“型別類別”，類似于Hask，但進行了適合討論的任何調整。在這樣的類別中，據說 (1) 初始代數定義資料型別，和 (2) 終結代數定義輔助資料型別。

我正在努力說服自己（2）。

考慮函子T(t) = 1 a * t。我同意初始T-algebra 是明確定義的，并且確實定義[a]了a. 根據定義，初始T-algebra 是一個型別X和一個 function f :: 1 a*X -> X，這樣對于任何其他型別Y和 function g :: 1 a*Y -> Y，只有一個函式m :: X -> Y使得m . f = g . T(m)(where.表示 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)。據說這應該定義一個潛在的無限串列。

我同意這有時是真的。例如，wheng :: 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了。

首先，when gis again () -> 0 | (_,n) -> n 1but is of type 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代數不存在。如果有的話，codatatype Stream（或無限串列）的理論建模不能基于不存在的函子的終端代數T(t) = 1 a * t。

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

uj5u.com熱心網友回復：

(2) 終端代數定義codatatypes。

這是不對的，codatatypes 是終端代數。對于您的T函子，余代數是一種型別x，與f :: x -> T x. 和T之間的-coalgebra 態射是這樣的。使用這個定義，終結符 -algebra 定義了可能的無限串列（所謂的“colists”），并且終結性由函式見證：(x1, f1)(x2, f2)g :: x1 -> x2fmap g . f1 = f2 . gTunfold

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

請注意，雖然終端T-algebra 確實存在：它只是Unit型別和常量函式T Unit -> Unit（這可以作為 any 的終端代數T）。但這對于撰寫程式來說并不是很有趣。

uj5u.com熱心網友回復：

（免責宣告：我不是 100% 確定 codatatype 是如何作業的，尤其是在不涉及終端代數時）。

一個 codata 型別，或 coductive 資料型別，只是通過它的消除而不是它的引入來定義的。

似乎有時使用終端代數（非常令人困惑）來指代最終的coalgebra，它實際上定義了一個codata型別。

考慮上面定義的相同的函子 T。終端 T 代數的定義與初始定義相同，除了 m 現在是 X -> Y 型別并且方程現在變為 m 。g = f。Tm值）。據說這應該定義一個潛在的無限串列。

所以我認為這就是你出錯的地方：“ 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由Left ()在f映射到Left ()和f映射到Right (x, m xs)時回傳的映射遞回地唯一定義，即將余代數分配給其唯一態射到最終的余代數，并表示這種型別的唯一變形/展開，這應該容易說服自己實際上是一個可能是空的和可能是無限的流。Right (x, xs)

uj5u.com熱心網友回復：

據說（1）初始代數定義了資料型別，（2）終端代數定義了codatatypes。

關于第二點，實際上是說終端代數定義了codatatype。

資料型別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）的 catamorphism 。

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）。

標籤：哈斯克尔 类型系统 范畴论 共同归纳

上一篇：如何避免不可謂的多型性并定義鏡頭的鏡頭

下一篇：GHCi中的“Prelude”前綴是什么意思？