代数的データ型とF-代数
Catamorphismとfoldの対応
リスト型とF-始代数
この関手のF-始代数(A,a)が存在したとすると、
Lembekの定理よりA\cong F(A)が成り立つ
さらにA=\mathrm{List}Bとすると、これらより
\mathrm{List}B\cong\mathrm{Nil}+B\times\mathrm{List}Bになる
data List b = Nil | Cons b (List b) と対応していることがわかる\rm{List}(B)は始対象として扱っていいのか？なんで？
つまり「A=\mathrm{List}Bとすると」は言っていいのか？
今回の話に固有の変数を代入する前のF-代数の図と、代入したものの図を並べて書いてみる
まず、画像右の上の矢印\mathrm{Nil}+B\times\mathrm{List}B\to\mathrm{List}Bの射を考える
先ほどの型
List b の値コンストラクタの型を調べるとこうなるhsdata List b = Nil | Cons b (List b)
-- Nil :: List b
-- Cons :: b -> List b -> List bこれに合うように射を定義する
n:\mathrm{Nil}\to\mathrm{List}B
c:B\times\mathrm{List}B\to\mathrm{List}B
この2つの射をこの記事に倣って[n,c]と表記する
\phiについても
同じノリで[f,x]を割り当てる
すると上図右はこうなる
この図を直和の性質を用いて2つの図にわける ref
なにこれ #??
緑を左辺、青を右辺とすれば以下の2式が導かれる
|[x,f]|\circ c=f\circ(B\times|[x,f]|)
|[x,f]|\circ n=x
これはfoldrの定義そのもの
hsfoldr :: a -> (b -> a -> a) -> List b -> a
(foldr x f) Nil = x
(foldr x f) (Cons a as) = f a ((foldr x f) as)一般のfoldrと引数の順番が異なることには注意
まとめるとこうなる
つまりCatamorphismが
fold に対応するこの記事によると
F-始代数は有限データ構造を表す
Catamorphismはfoldに対応する
F-終余代数は無限のデータ構造を表す
Anamorphismはunfoldに対応する
F-始代数はリスト型以外にも応用可能？
foldlも導ける？
やってみよう
参考
さいきょうの記事
とちゅう