System F

Wadlerのノートにあった
Lfix X. F X = All X. (F X -> X) -> X.
Gfix X. F X = Exists X. (X -> F X) * X.
という定義はどっから降ってきたのかというと、単に、こういう話のような。

以下、fをFunctor、inF::f(Fix(f))->Fix(f)として、
buildF::(forall x.(f x -> x) -> x) -> Fix f
buildF(g)=g(inF)
とすると、acid rain theoremから、g::forall x.(f x -> x) -> xに対して、
fold phi (buildF g) == g(phi)
が成り立って、
flip fold (buildF g) == g
逆に、a::Fix fについて、
buildF (flip fold a) == flip fold a inF = fold inF a = a
より、buildFとflip foldは互いに「逆写像」 

buildの意味をよく理解してなかったよ。GFixに対して、unfold/destroyで同じことができそうだけど、Existsというのは、どっからでてきたのか謎。

(2006/11/30追記)http://citeseer.ist.psu.edu/519604.htmlの214ページあたりによると、
exists x.t = forall c.(forall x.(t->c)->c) (但し、cはtの自由変数でない)
という定義で、destroyの型が
destroy :: Functor f => (forall x . (x -> f x) -> x -> c) -> Fix f -> c
なので、destroyをflipしたものが、同形を与えるんでないかな。確かめてないけど、きっとそう

Church Encodingについて。結局自然数型Natには、2種類定義があって、その二つが一致するのは何でかという話に。一つ目の定義は、関手NatFの不動点で、もう一つの定義は、
Nat = forall x.(x->x)->x->x
で、もう一つの定義は、関手NatFの不動点。
NatF t = ZeroF | SucF t

で、(一般化した)buildの定義を思い出すと
buildF::(forall x.(NatF x ->x)->x)->(Fix NatF)
で、buildFは「同形写像」なので、(forall x.(NatF x ->x)->x) <=> forall x.(x->x)->x->xが言えればよくて(<=>は自然な一対一対応が存在するという意味)、形式的に
(NatF x -> x) -> x<=> ((Either () x) -> x) -> x<=> (x->x)->x->x
が成り立つという、そんだけの話か。Fix(NatF)に、どういう要素が含まれるかは、一概にはいえないけど、集合の圏で考えれば、通常の自然数の集合になる(はず)。

分かって見ると、しょうもないというか、これが理解できないと、普通のリストに対するfoldr/buildとgenericなfold/buildが繋がらないな･･･(なんか勘でやってたけど)

foldr::forall a. (forall x.(a->x->x)->x->[a]->x)
forall a. (forall x.(a->x->x)->x->[a]->x)
<=> forall a. (forall x.((a,x)->x)->x->[a]->x)
<=> forall a. (forall x.((Either () (a,x))->x)->[a]->x)
<=> forall a. (forall x.((ListF a x)->x)->[a]->x) where ListF a t = Nil | Cons a t

build :: forall a . (forall b . (a -> b -> b) -> b -> b) -> [a]
forall a . (forall b . (a -> b -> b) -> b -> b) -> [a]
<=> forall a. (forall b. ((a,b)->b) -> b -> b) -> [a]
<=> forall a. (forall b. ((Either () (a,b)) -> b) -> b) -> [a]
<=> forall a. (forall b. ((ListF a b) -> b) -> b) -> [a]

今まで如何に何も理解せず書いていたかという。もっと早く気付けよ、頭悪すぎてorzまあいい、まあいいんだ。これから賢くなれば！ところで、最小不動点・最大不動点ということは、(LFix f)->(GFix f)という「埋め込み」が構成できそうな気もするけど、どうなんだろう。ありそうな気もするし、無理そうな気もする。

buildの定義を見ると、(f x -> x) -> xが入ってるので、Haskellで書けるような関手fに対しては、(f x -> x) -> xは、「EitherやTupleを明示的に含まない」形に変形できる(はず)。というか、
data SumF a b t = LeftF a | RightF b
data PairF a b t= Pair a b
とすると(SumF a b)と（PairF a b)は自然に定数関手で、

Either a b
<=> Fix (SumF a b)
<=> forall x.((SumF a b x) -> x) -> x
<=> forall x.((Either a b) -> x) -> x
<=> forall x.(a->x , b->x)->x
<=> forall x.(a->x)->(b->x)->x

(a,b)
<=> Fix (PairF a b)
<=> forall x.((PairF a b x) -> x) -> x
<=> forall x.((a,b) -> x) -> x
<=> forall x.(a -> b -> x) -> x

polybool 
<=> Either True False
<=> forall x.(()->x)->(()->x)->x
<=> forall x.x->x->x

結局、Haskellで使えるデータ型は、全て多相ラムダ計算の範疇でモデル化できることに。多相ラムダ計算って、よくできてるな〜。と思って、WikipediaのSystem Fの項見てたら、Girardの書いた教科書っぽいものが、Referenceにー。しかし、なんか長いなぁ。強正規化定理/Reparesentable theorem/型推論の決定不能性の証明を理解すること(そのうち)。理解してやるってセリフは、、、終わってから言うもんだぜ。俺たちギャングの世界ではな

どうでもいいけど、System Fの名前の由来は何だろう。System Fというと、まずこれを思い浮かべるんだが