Warm fusionとか
融合変換のための前処理として、普通の再帰的定義で書かれた関数を、foldなりhylomorphismを使った形に変換しないといけない。で、recursive definitionをcata/build formに変換するのが、warm fusionらしい。一応、Warm Fusion: Deriving Build-Catas from Recursive Definitionsを読んだけど、なんかよくわかんね。これほんとにうまくいくのかね〜。なんか、胡乱な感じが(勿論、うまくいくには決まってるけど、つまりどのくらい効果があるのかというのが)
promotion theoremは、リストの場合、strictな関数gに対して
g f1 = h1
g (f2 y1 y2) = h2 y1 (g y2)
が成り立つならば、
g (foldr f2 f1 x) = foldr h2 h1 x
が成り立つという定理。f1= , f2=(:)に取ると、
g = h1
g (x:xs) = h2 x (g xs)
ならば、(foldr (:) [] = idに注意して)
g = foldr h2 h1
が成り立つ、という、foldrの定義そのものが得られる。
で、例えば、mapの場合
map f [] = h1 map f (y:ys) = h2 y (map f ys) where h1 = [] h2 z1 z2 = (f z1):z2
なので、
map f x = foldr h2 h1 x where h1 = [] h2 z1 z2 = (f z1):z2
が成り立つ。まあ、当たり前すぎて面白くもないが。論文では、自動化できるように、もうちょいちゃんとやってる気がする
あと、多分あとでうまくfusionできるようにするためだと思うけど、buildを外側に持ってこないといけないっぽい(論文の"syntax-to-syntax translation B")
map = {foldr (:) []=idとbuildの定義から} \f x -> build (\c n -> foldr c n (map f x)) = {recursive definition of map} \f x -> build (\c n -> foldr c n (case x of []->[];(y:ys)->(f y):(map f ys))) = {distribute foldr across the case expression} \f x -> build (\c n -> (case x of [] -> (foldr c n []); (y:ys) -> (foldr c n ((f y):(map f ys))))) = {definition of foldr} \f x -> build (\c n -> (case x of []->n;(y:ys)->(c (f y) (map f ys)))) = {promotion theorem} \f x -> build (\c n -> (foldr (mapFB c f) n x)) where mapFB c f z zs = c (f z) zs
というわけで、GHC.Baseにある"map" RULESの謎(なんで、わざわざmapFBを経由してるのか)が解けた。
{-# RULES "map" [~1] forall f xs. map f xs = build (\c n -> foldr (mapFB c f) n xs) "mapList" [1] forall f. foldr (mapFB (:) f) [] = map f "mapFB" forall c f g. mapFB (mapFB c f) g = mapFB c (f.g) #-}
けど、"mapFB" RULESは、結局、人間が手でいれてやらないといけないのね。なんか中途半端だ。"translation B"を施した後、second-order fusionを使う道もあるよ、とか書いてあるけど、よくわからんかった。まあよい
しかしまあ、そういうことを理解すると、以前mssの融合変換がGHCのRULESプラグマを使ってやろうとして、うまくいかなかったのは至極当然だな。
けど結局、"mapFB" RULESの例とかみると、融合変換そのものだけでできることはしれてるとか、そんな気がする。それはhylomorphism使っても同じで、"basic functors and related combinators"(ここで書いたinl,inr,split,junc,etc..みたいなやつ。もっといい名前はないのか)を使って徹底的に関数を分解してやらんといかんとか、そういうことなんだろうなー。しらんけど。それと、foldだけだと(たぶん)表現力に限りがあるので、いなくなってしまったunfoldのこと時々でいいから思い出してください・・・(foldとunfoldでhylomorphismと等価で、hylomorphismはprimitive recursiv functionを表現できる程度には強力らしいので)
いつか、まともなコンパイラなら融合変換くらいやって当たり前みたいな時代がくるんだろうかね