Algebra of Programming - initial algebra

01-31

哈嘍！失蹤人口回歸啦，上篇文章還是半年前寫的，w(?Д?)w，鬼知道我經歷了什麼。。。

本文主要是填上文的一些坑，並得出一點小結論，以便更好的應用初始代數以及catamorphisms, fold等

上文砍掉了很多東西，本文就更詳細的展開討論一下初始代數（initial algebra）和代數數據類型（algebraic data type（product & sum））

前面我們用initial algebra去表示recursively defined datatype，採用的是比較抽象的方式（用了函子的不動點做初始代數，這已經涉及到了 Lambek』s Lemma）

我們考慮從普通方式一步步走到那裡去，先回看F-代數，初始代數的定義

F-algebra

首先是有一個自函子，F：C <- C，一個對象：A，一個箭頭：A <- FA (先不要在意用<-，而不是->)，這個箭頭就是F-algebra啦，對象A為代數的carrier

栗子：自然數加法：algebra (Nat, +)，是函子F（FA = A x A & Fh = h x h）（F是個squaring functor）的代數, 也就是A為Nat，代數為： $algebra(+): Nat leftarrow Nat^{2}$

(+) (1, 2) = 3n

F-homomorphism：從一個代數 g: B <- FB 到一個代數 f: A <- FA 的一個箭頭 h: A <- B，使得：h . g = f . Fh

用圖來表示type information：

栗子：前面的 $algebra(+ )$ 和加法模p的代數： $algebra(oplus ): Nat _{p} leftarrow Nat^{2}_{p}$ ，（ $Nat_{p} = left{0, 1,... p-1 right}, n oplus m =$ (n + m) mod p）則函數：h n = n mod p是 $algebra(+ )$ 到 $algebra(oplus )$ 的F-homomorphism （後面簡稱為homomorphism）

Initial algebra

下面將一個代數如alg: A <- FA 作為一個對象討論，其Identity arrows是F-homomorphism，F-homomorphism 組合上F-homomorphism還是F-homomorphism，所以：

將F-代數作為對象，將F-homomorphism作為箭頭，就形成了一個範疇：Alg(F) （F指代數的函子），那麼其initial object 就是 initial F-algebra （到所有其它代數都有唯一的箭頭（F-homomorphism））；並且對於很多函子（包括polynomial functors）都存在這種範疇的initial object（證明：略）

下面就可以對初始代數進行定義了：就是範疇Alg(F)的初始對象，記為 a : T<- FT，或（a, T），（在程序中T指Type）

利用初始對象的性質，我們發現初始代數a到其它代數如f : A<- FA都有唯一的homomorphism，我們將此homomorphism記為：([ f ])，所以([ f ]) : A <- T，有如下性質：

h = ([ f ]) ≡ h . a = f . Fhn

Catamorphisms

所有像([ f ])這樣形式的箭頭就叫做catamorphisms，我們可以理解為接收一個代數f，返回一個homomorphism： ([ f ])

（也就和前文的cata函數對應了）

recursively defined datatype

Natural numbers

下面就來看recursively defined datatype，先從最簡單的Nat開始：

Nat ::= zero | succ Natn

這其實定義了一個初始代數：[zero, succ] : Nat <- F Nat，函子F為FA = 1 + A & Fh = id1 + h；

（這個函子是polynomial，所以它的Alg(F)範疇存在initial object，也就是存在初始代數）

zero : Nat <- 1 是一個常量函數，succ則是Nat <- Nat的函數

1 是terminal object，在程序中指只有一個實例的type，如Unit，它的唯一實例為：()

id1 是terminal object 的恆等態射（Unit -> Unit）了，我們將這個代數畫出來：

這裡是個coproudct結構(sum type)，所以對Type，F為 A -> Coproduct[Unit, A]，對態射（箭頭）：

Fh = id1 + hn = [inl . id1, inr . h] ;{coproduct functor的性質：f + g = [inl . f, inr . g]}n = bimap( inl . id1, inr . h ) : Unit + A => Unit + Bn

所以可以找個coproudct的實例如：Either[A, B] (inl和inr就對應left和right構造子了)來指代該函子

所以函子F就可以是Either[Unit, A]，fmap f 就是Either[Unit, A].bimap(left . id1, right . f )

所以函子F就是將bifunctor: Either[A, B] fix type A之後的函子Either[Unit, A]

所以可以用一個bifunctor去表示該代數（natural numbers）：

_zero () = Left(zero)n_succ n = Right(succ n)n0 : bimap(_zero, _succ) Left(()) => Left(zero)n1 : bimap(_zero, _succ) Right(zero) => Right(succ(zero))n2 : bimap(_zero, _succ) Right(succ(zero) ) => Right(succ(succ(zero)))n

至此我們可以看出一點結論：函子F(A)，是一個二元函子F(A, B) fix 一個type之後的產物，其次這個type declaration 就是為了給initial algebra一個name

([ c, f ])

對每一個函子F: C -> C的代數都有[c, f]這樣的形式（如上[zero, succ]），一個常量函數c: A <- 1，一個函數f: A <- A

另代數h : A <- FA，有h = [h . inl, h . inr]，原因為c = h . inl，f = h . inr，如下圖：

所以代數h = [c, f]的homomorphism，([ f ])就是([ [c, f] ])，括弧太多簡記為([ c, f ])，或者用代碼的寫法：cata( [c, f] )

(註：形式[c, f]從coproduct的universal property來： [c, f] . inl = c，[c, f] . inr = f)

我們考慮初始代數a = [zero, succ]，到其它代數[c, f]的homomorphism，如圖：

通過交換圖聯通：

得到了：h zero = c & h succ = f . h，這個等式的唯一解h為：

h (0) = cnh (n +1) = f(h n)n

因為homomorphism：h又寫為：([ c, f ])的形式，故h = ([ c, f ])，且觀察上面h函數和Nat的foldn：

foldn(c, f) (0) = c ; 0為zero nfoldn(c, f) n + 1 = f(foldn(c, f) n) ; n + 1 為 succ(n)n

所以得出：h = ([ c, f ]) = foldn(c, f) = cata( [c, f] ) in the datatype Nat， foldn(c, f)就是個homomorphism

所以取不同的c，f函數值，便可以表示Nat的其他homomorphisms如：

plus m = foldn (m, succ)nmult m = foldn (0, plus m)nfact = outr . foldn ((0,1), f) where outr(m, n) = n & f(m, n) = (m + l,(m + 1) x n)nfib = outl . foldn ((0,1), f) where outl(m, n) = m & f(m, n) = (n,m + n)n

也可簡記為：plus m = ([m, succ]) ， ([ _ ]) 被視為一種新的函數組合方式（組合子）

String

下面來看另一種特殊的recursively defined datatype，String

String ::= nil | cons (Char, String)n

它特殊的地方在於String 就是 [Char]，它就是一個list Char，為推廣至list A 做準備，先看一下初始代數String

它聲明了代數[nil, cons]: String <- F String 為函子F (FA = 1 + (Char x A)，Ff = id + (id x f))的初始代數：

如Nat，該函子F的每個代數都有形式：[c, f]，其中c: A <- 1，f: A <- Char x A

看圖，得出該函子F為A -> Either[Unit, Tuple2[Char, A]]，序對（product type）：Char x A，可以用Tuple2或pair來表示，也就是說它是：F[A] = Either[Unit, Tuple2[Char, A]] 這樣的函子，顯然它是polynomial，並且它可以由二元函子Either[Unit, Tuple2[A, B]] fix type A 之後得到，這裡將A = Char，而二元函子又可以由二元函子Either[C, D] fix type C = Unit，type D = Tuple2[A, B] 得到，type D = Tuple2[A, B] 也是個二元函子（proudct functor），這種結構和類型聲明的形式是完全契合的，或者說和代數數據類型的形式完全契合（nil => Unit -> String，| => coprouct functor，cons => Char x String，x => product functor）

同樣的：h = ([ c, f ]) = foldr(c, f) in the datatype String，並且([ c, f ]) 和 fold操作是一致的

List

下面推廣到list A這種帶類型參數的情況，我們用cons-list（listr，還有一種snoc-list叫listl）表示：

listr A ::= nil | cons(A, listr A)n

這聲明了 $[nil, cons]_{A}: listr A leftarrow F_{A}(listr A)$ 為函子 $F_{A}$ （ $F_{A}(B) = 1 + (A times B) , F_{A}(f) = id + (id times f)$ ）的初始代數

根據前面我們知道函子FA可以由一個二元函子F fix 前一個type得到，將 $F_{A}$ 寫為 F(A, B)，則：

$F_{A}$ (f) = F(idA, f) = id + (idA x f) <= F(g, f) = id + (g x f)

F(A, B) = 1 + A x B

（故：[nil, cons]是bifunctor F的初始代數）

看類型信息：

這個菱形（將product和coproduct組合在了一起），更清晰的展示了前面String時說的代數與代數數據類型的關係，無非就是將Char換回了類型參數A

這個二元函子可以用Either[Unit, Tuple2[A,B]]來表示

而類型構造子listr本身也可被定義為一個函子，稱其為type functor：有二元函子F以及初始代數集合 $a_{A} : TA leftarrow F(A, TA)$ （fix A 可得代數 TA <- FA(TA)），T為類型構造子，則T可以被定義為一個函子：Tf = ([ a . F(f, id) ])

栗子：對cons-list的函子定義為： listr f = ([ [nil, cons] . (id + (f x id)) ])

又因為coproduct functor的性質(fusion law)：[f, g] . (h + k) = [f . h, g . k]，所以:

[nil, cons] . (id + (f x id)) = [nil . id, cons . (f x id)]n

故：

listr f = ([ [nil, cons] . (id + (f x id)) ])n= ([ nil . id, cons . (f x id) ]) n= cata([nil, cons] . (id + (f x id)))n= foldr(nil . id, cons . (f x id) )n

通過listr f = ([ nil . id, cons . (f x id) ]) 就可以看出這個listr 就是 fmap，f只會對cons的左邊有影響

Fusion

對函子T應用fusion得到：([h]) . Tg = ([ h . F(g, id) ])，也就是說catamorphism和函子T組合得到了單個catamorphism，這非常有用，因為前面Nat的時候列舉過一些操作就是代數的同態函數

如對list有：sum = ([zero, plus])，sum: Nat <- listr Nat，則：

sum . listr f = ([zero, plus . (f x id)]) = foldr(zero, plus . (f x id) )，再結合以後會提到的banana-split law 可能是提升性能的關鍵

Lambeks Lemma

下面插播一條引理：

所以我們的初始代數就是一個isomorphism，證明過程如下圖：

存在g: a -> Fa，使得： $g cdot f = Ff cdot Fg = F(f cdot g) = Fid_{a} = id _{Fa}$

最重要的是Lambek稱：初始代數(a, f)為函子F的不動點（在代碼中該初始代數就是前文的(Fix, f(Fix f) -> Fix f)）

前面的recursively defined datatype 都是聲明了某代數為某函子的初始代數，但是我們也可以像前文那樣通過Fix + non-recursive type的方式去表示 recursive type

（F為ListFInt[A]），讓我們以這篇文章的知識解構一下前文中的代碼

recursive 並沒有消失，而是移交給了Fix和cata (抽象提升了)

end

本文主要講了，初始代數與遞歸類型，代數數據類型的關係，新的函數組合形式：([_])，以及對前文Fix不動點的填坑，對《Algebra of Programming》第二章節的核心內容做了一點點補充

以category theory做meta language討論函數式編程，不過本文停留在『是什麼？』的階段，後續會出『怎麼用？』（( ｀д′) 我褲子都脫了，你就讓我看這個？有生之年系列？）