限定継続について勉強してみた(continued)

日にちが開いてしまったけれど、前回の続き。

まず、meta continuation、メタ継続について。メタ継続とはつまり、「継続の継続」のことで、次のような動機により導入される概念らしい。

resetとshiftの継続意味論を再掲。

ここで、resetがnon-tail callを含んでいることに注意。継続kの呼び出しは、式Eをという継続とともに評価して、値が「返って」くるまで実行がサスペンドされる。関数がreturnすることを強制されるのでtail callではない。

では、tail callにするために

としてはダメなのかといえば、これはよくない。Eに与えられる継続は、shiftからの脱出によって捨てられる可能性があるためだ(resetの継続kは、shiftから脱出したときでも実行されるのだから、脱出によって捨てられてしまってはいけない)。

shift内で捕捉される継続についても、tail callでない形をしている。これらをtail callの形にしようというのがメタ継続。のはず。

メタ継続を導入すると、resetとshiftのsemanticsは次のようになる。

継続は値とメタ継続を引数にとり、メタ継続は値のみを引数にとる。変数、関数抽象、関数適用それぞれに対するsemanticsはここには載せてないけれど、全部を眺めてみても、どのメタ継続がどの継続の継続処理として実行されるのかは追いきれてなかったりする。とりあえず、shift/resetのsemanticsが完全にCPSで表すことができるってことが分かればいいんだろか。それから、継続は捨てられることがあってもメタ継続は必ず実行されるということが保証されるのかな(これは実装コードからの逆算だけど)。

今まで見たきただけではメタ継続のありがたみというのは分からないんだけど、メタ継続を取り入れることでcall/ccによるshift/resetの実装ができるようになるらしい。