CPS(型だけ)

CPS（継続渡し方式）変換をJavaScriptで説明してみるべ、ナーニ、たいしたことねーべよ - 檜山正幸のキマイラ飼育記 (はてなBlog) を見て頭がオーバーフローしたので、型だけで見ることにしてみた。

ズルして結果を先取りする。型Aをとって型Bを返す関数f

f::A->B

のCPS変換f*は

f::A -> B	== CPS変換 ==>	f*::(B->X)->(A->X)

だよと。観察すると

• f*は「関数を取って関数を返す」関数
• AとBの順番が入れ替わってる。
• Xはそのつど決まる型。

などなど。
Xが何になるのかは、例えば

f1::A->B
f2::B->C

みたいに、2つの関数があって、B型の値を受け渡す場合

f1::A->B	== CPS変換 ==>	f1*::(B -> C) -> (A -> C)
f2::B->C

と、最終的に返される結果の型(ここではC)になる。直後の関数の戻り型ではないっぽい。
たくさん関数が連なってたら

f1::A->B	== CPS変換 ==>	f1*::(B->E)->(A->E)
f2::B->C	== CPS変換 ==>	f2*::(C->E)->(B->E)
f3::C->D	== CPS変換 ==>	f3*::(D->E)->(C->E)
f4::D->E	== CPS変換 ==>	f4*::(E->E)->(D->E)

になる。
普通の書きかたの方だと計算は

  f1   f2   f3   f4
A -> B -> C -> D -> E

とつなげられる。型もあってる。同じくCPSの方もつなげられる。ただし逆順になる。

      f4*       f3*       f2*       f1*
(E->E) -> (D->E) -> (C->E) -> (B->E) -> (A->E)

型をあわせるにはこうつなげるしかない。
で、この2つが同値になって欲しいと。
ためしにf4*とf3*を合成して、(E->E)として恒等写像を取ると

       (f3*)○(f4*)
(E->E)      ->       (C->E)
id         ├>        f4○f3 ?

○は関数の合成。?は(C->E)な関数だから、f4○f3なんじゃないかと。
もしそうだとこうなる。

      f4*        f3*         f2*            f1*
(E->E) ->  (D->E) -> (C->E)   -> (B->E)      -> (A->E)
id    ├>    f4  ├> f4○f3  ├> f4○f3○f2 ├> f4○f3○f2○f1

いい感じ。普通に書いたのと同じ内容が作りあがった。

ほとんど型しか考えてなかったけど、実際にこうなるように実装できるか考える。

fのCPS変換f*の定義
def f*(cont)
  cont○f
end

これだけでいいんじゃないか。こう定義すれば、たとえば

f4(f3(f2(f1(x))))
f1*(f2*(f3*(f4*(id))))(x)

の2通りの書き方で同じ内容になる。

CPS変換ってこういうことなのかな。