fold/build/augment/unfold/destroy

圏論

というような話がリストでしか言えないなら、新しくデータ型を作るたびに、ルールを発見せねばならず、大して面白くもないんだけど、foldとかbuildとかaugmentは、圏論的背景を持ってて、Haskellの他のデータ構造でも使えるという話なので、素晴らしいかもしれない。けど、実際には、今のHaskellだと、データ型定義するごとに自分でfold/etc...とルールを定義する必要がある気がする

とりあえず、
http://www.cs.ioc.ee/~tarmo/misc/builds-subm.pdf
あたりを読もうと試みる。Cを圏として、FをCの自己関手、Alg(F)を、F-代数の圏とすると、忘却関手U(F):Alg(F)->Cの極限が存在すれば、F-始代数と同等で、双対的に、F-余代数の圏Coalg(F)に対して、忘却関手V(F):Coalg(F)->Cの余極限が存在すれば、終余代数と同等になる。という話までは理解した。

Haskellで書かないとイメージわかん

{-# OPTIONS -fglasgow-exts #-}
data Mu f = Build (forall x. (f x) -> x -> x)
data NatF x = NatC (x->x)
type Nat = Mu NatF

fold :: (f x) -> x -> (Mu f) -> x
fold s z (Build theta) = theta s z

zeroN :: Nat
zeroN = Build (\_ -> id)

nat_to_int :: Nat -> Integer
nat_to_int n = fold (NatC (+1)) 0  n 

instance Show Nat where
 show n = show (nat_to_int n)

とか、こんな感じですか。Church数として自然数が定義できるのはいいけど、標準的(?)なNatの定義(data NatF x = Zero | Suc x;type Nat = Fix NatF)と、どう繋げればいいんだろう。

(2006/11/21追記)上の構成は一応動くけどおかしい。data NatF x = NatC (x->x);type Nat = Mu NatFとか意味不明。NatFは普通に定義して、*1 -> x -> (Nu f)で、リストの場合は、「f x = 1 + a*x」なので、Maybe (a,x)を使ってるだけだ)

*1:Either () x)->x)->xと(x->x)->x->xの間に、自然な一対一対応があるので、それを介して、data NatF x = Zero | Suc x;type Nat = Fix NatFという定義と繋がる。つまり、Mu NatFとFix NatFの間に一対一対応がつくれる。この対応は、任意の関手について半自動的につくれるけど、Haskellの範疇でそれを自動化するのは多分難しい dinaturalityとかは何が嬉しいのかよく分からないので、多分どうでもいいとして、augmentを書こうとして挫折した。Monadに持ち上げるとこの(>>=)が定義できねー。いや、もう眠いから。多分明日には書ける(かもしれない)!こんな複雑な構成思いつくやつは頭がイカレテルと思いますよ！てかねー、仮に書けても、これ使ってコード書くのは大変だよなー。 あとなんか、unfoldrで突然現れるMaybeモナドは何故に？てか、そもそも、Haskellのリストって始代数で終余代数なん？ #(追記)余りにもアホなこと書いてたな〜。私はunfoldの定義を100万回暗誦するべきだと思った。unfold::(x -> (f x