代数的データ型とF-代数
$ X,\mathrm{Nil},B,AはHask圏の対象。$ aは射。 Hask圏において、関手$ F(X)=\mathrm{Nil}+B\times Xを考える この関手のF-始代数$ (A,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-代数の図と、代入したものの図を並べて書いてみる https://gyazo.com/ecc5f10314a300115e8fabf9ad5482c7
まず、画像右の上の矢印$ \mathrm{Nil}+B\times\mathrm{List}B\to\mathrm{List}Bの射を考える
先ほどの型List bの値コンストラクタの型を調べるとこうなる
code:hs
data 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] を割り当てる
すると上図右はこうなる
https://gyazo.com/cecbdae7c9d3f4b061155e647513f0cd
この図を直和の性質を用いて2つの図にわける ref https://gyazo.com/724ef02fb29930dff760eea8867a6306
緑を左辺、青を右辺とすれば以下の2式が導かれる
$ |[x,f]|\circ c=f\circ(B\times|[x,f]|)
$ |[x,f]|\circ n=x
これはfoldrの定義そのもの
code:hs
foldr :: 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と引数の順番が異なることには注意
まとめるとこうなる
https://gyazo.com/006a951aaaaa5339fd7961fff6070f35
foldlも導ける？
やってみようmrsekut.icon
参考
さいきょうの記事
とちゅう