Wadlerのノートがまだよくわからん

なんかやっぱまだ混乱してるっぽい。Wadlerのノートの話なんだが、LFixとFixとGFixがようわからんとか。WadlerのノートにあるLFixとfold(という名前はFixに対して、使うので、ここではcataと書いておく)やらinの定義を、Haskellで素直に書くとこうなる。ついでに、普通の(?)foldの定義を併記しておく

{-# OPTIONS -fglasgow-exts #-}
newtype LFix f = Build (forall x.(f x -> x) -> x)

cata :: (Functor f)=>(forall x.(f x -> x)->(LFix f)->x)
cata k (Build t) = t k

inF :: (Functor f) => f (LFix f) -> (LFix f)
inF s = Build (\k -> k (fmap (cata k) s))

outF :: (Functor f) => (LFix f) -> f (LFix f)
outF = cata (fmap inF)

newtype Fix f = In (f (Fix f))
out (In a) = a

fold :: forall f.(Functor f) => (forall x.(f x -> x) -> (Fix f) -> x)
fold g = g . fmap (fold g) . out

定義から、自動的に

cata k (inF s) 
= cata k (Build (\k -> k (fmap (cata k) s)))
= k (fmap (cata k) s)

fold k (In s) 
= k . (fmap (fold k)) . out (In s) 
= k (fmap (fold k) s)

が従う。つまり、foldもcataも(Fix f)や(LFix f)から、任意のf代数への射を与える。これが一意であることは自明でないので、Wadlerのノートでは、weakly initial algebraと呼んでいる。

で、LFixとFixが一致するのかという話。Fixの定義は、単に、f (Fix f)と(Fix f)が同型になると言ってるだけなんだよなぁ。関手fの不動点は、多分一般には沢山存在するので、別段それとLFixを同一視するa prioriな理由はないはず。けど、Haskellでは、少なくともあるクラスのFunctorに対しては、最小不動点と最大不動点が一致して、不動点は一意に決まる(ホントかよ)のか?ていうか、最小・最大というのは包含関係について最小・最大という理解でいいんだろうか?まあ、仮にそうだとしても、LFixとGFixの一致は何によって保証されてるのか、よくわからん。勿論、直接的には、遅延評価によってというのが答えなんだろうけど、なんか狐に化かされた感がするというか、説明になってないというか･･･

別の道。LFixもFixもweakly initial algebraになので、こいつらが実際に、initial algebraであることを言ってしまえば、LFixとFixが一致することは言えるけど、それを言うには、Wadlerのノートの条件(3)(4)がいえればよく、そのためには多分parametricity theoremが必要で、Haskellでparametricity theoremを保証するのは何なのかという別の問題が。そもそも、ちゃんとしたsemanticsがないので、証明できるような類のもんではないのかもしれんけど、Acid Rain Theoremとか、あのへんの面白い定理の証明は、parametricity theoremに根拠を持ってたりするので、Haskellで融合変換が使えるか否かというのに、直接影響を与える気がする。

ほんでもって、よく見ると(よく見なくても)、cataの定義には、どこにも再帰が入ってないのに対して、foldの定義はそうではない。fixpoint recursionが存在すると、parametricity theoremは制限を受けないといけなくなる(というようなことは、Wadlerの"Theorems for free!"に書いてある)ので、つまりまあ、cataの方は、純粋にSystem Fの範囲で定義できて、parametriciy theoremが成立するようなモデルであれば、LFix fが確かに、f-始代数を与えることを証明できる(多分)けど、foldの方は、そうではないとか。普通の実用的言語では、fixpoint recursionは存在して、parametricity theoremは(制限された形でしか)適用できず、Haskellのようにnon-strictな言語ではLFixやFixが始代数になることは別の手段で言わないといけないと思う。strictな言語の場合は、parametricity theoremの適用に悩む必要はないのかな、たぶん

別に、こんなことを理解したところで、何の役にも立ちはしないんだけど･･･

オレは『納得』したいだけだ！『納得』は全てに優先するぜッ！！でないとオレは『前』へ進めねぇッ！

関係ありそうな仕事(どっちもちゃんと読んでないけど)
・A Formalization of Hylomorphism Based Deforestation with an Application to an Extended Typed Lambda-Calculus
・Shortcut fusion is correct
http://www.crab.rutgers.edu/~pjohann/jfp01.pdf
いずれも、Fixが〜LFixが〜始代数が〜という話ではなくて、タイトル通り、融合変換の正当性の話。まあ、始代数がどうとかより、融合変換が成立するかの方が重要とは思うけど。2000年前後の仕事なので、今はもっとなんかあるかもしれない。どうでもいいけど、recursive typeとかalgebraic data typeとかinductive typeとか、違いがわかんね

後者の論文で使われてる体系PolyPCFは、System Fにfixpoint recursionとリストを付け加えただけに見える。Pittsのparametric polymorphisms and operational equivalenceには、このPolyPCFの範疇では、このリストが、多相型forall x.x->(a->x->x)->xと"observationally isomorphic"(要するに、一方から他方への写像が存在して、互いに逆関数になっている)になることが示されている。つまり、PolyPCF=System F+fixpoint recursionと見なしていいってことかね。cataの場合、shortcut fusionは定義そのものなので、PolyPCFの組み込みのリストがforall x.x->(a->x->x)->xと"同型"と言えた時点で、ほとんど終わってる気もするが、そうでもないのかな。前者の論文で使われてるExtended typed lambda calculusも実質的に、PolyPCFといっしょな気がする。

しかし、いろいろややこしいなー