■

http://d.hatena.ne.jp/m-a-o/20061030
でも書いたLFixとGFixが相変わらずよく理解できなかったり。Wadlerのノートを読み返すと、これは必ずしも自明なもんでもないらしく、論文にもなっているようだけど、論文が入手できん、むー。こういう時、困るなぁ。が、LFixの定義よく見ると、fold(の型)とよく似ている。foldの定義はいい加減目に焼きついた

Lfix X.F X = All X. (F X -> X) -> X.
fold :: forall f.(Functor f) => (forall x.(f x -> x) -> (Fix f) -> x)

flip fold :: forall f.(Functor f) => (Fix f) -> (forall x.(f x -> x)->x)
なので、うまく、（Fix f)から(forall x.(f x -> x) -> x)への写像がつくれる。で、これが一対一対応(という集合論に毒された言い方が正しいのかどうかは知らんが)かどうかなんだけど、今の私にはちょっとよくわからん。

GFixの方も平行して議論できそうだけど、こっちは

Gfix X.F X = Exists X. (X -> F X) * X.
unfold :: forall f.(Functor f) => (forall x.(x -> f x) -> x -> (Fix f))
uncurry unfold :: forall f.(Functor f) => (forall x.(x -> f x , x)) -> (Fix f)

えー、Existsってなんやねーん。まあ、こいつらが関係ないってことはないでしょ、常識的に考えて

あと、自然数のChurch Encoding。
Nat = forall x.(x -> x) -> x -> x
は証明を要するんじゃないのかなー。Natから右辺への写像が存在して、単射なのはいいとして、全射だって、どうやって言うんだろ(いや、2階ラムダ計算の教科書には書いてるのかもしれんけど)