継続、call/cc

スマートコン @mr_konn

call/ccの挙動は知っているがちゃんと理解していないのでこの期に頑張ろう

スマートコン @mr_konn

うーん、cc が入って簡約が比較的簡単な例をつくろう

スマートコン @mr_konn

継続って評価戦略に依存しますよね？

スマートコン @mr_konn

結局 call/cc っていうのは reset 即 shift みたいな理解で良いんだな

スマートコン @mr_konn

call/cc は全体を reset で囲んである場合の shift だと勝手に誤解していた

Yusuke Endoh @mametter

@mr_konn あれ、違うんでしたっけ。

スマートコン @mr_konn

@mametter たとえば reset (3 + shift (const 12)) の答は 12 ですけど、3 + callcc (const 12) の答は15ですよね

Yusuke Endoh @mametter

@mr_konn そうか。継続を呼ばないとそうなりますね。でも reset (shift (fun k -> (k 1) + 2)) は 3 だけど callcc (fun k -> (k 1) + 2) は 1 になるので単純に reset 即 shift でもない気がする

スマートコン @mr_konn

@mametter あーそうか、確かにそうですね……。うーん、どう考えるのがいいんですかね……。

Yusuke Endoh @mametter

@mr_konn callcc M は全体を reset で囲った上で shift (fun k -> k M) と同じ？（ただしプログラムは最後に exit するので reset には到達し得ないこととする）

スマートコン @mr_konn

@mametter そうすると Mの中で k を使う時に型があわない気がします……

Yusuke Endoh @mametter

@mr_konn 型とかいう発想を忘れていた。普通の継続の型は t -> \bot です。部分継続でも同じだと思いますが、プログラム全体を reset で囲むのは仮想的にはできるけど実際にはできなくて現実の型システムは通らないかも？という話かしら？

スマートコン @mr_konn

@mametter たとえば callcc で囲われた部分全体が型 t だとした時の継続が t → ⊥ だということですよね。それはいいんですけど、この時 callcc M の M は (t → ⊥) 型を引数にとるので、k M って道理に合わないのでは……？と思ったのです

Yusuke Endoh @mametter

@mr_konn 普通に間違えてますね。callcc M は shift (fun k -> k (M k)) と同じか

スマートコン @mr_konn

@mametter ああそれですね！こうやってみてみると、call/cc はやっぱり不必要に複雑だという感じがしますね……。

ると @cocoa_ruto

@mametter @mr_konn call/cc (λk. (k 1) + 1) + 2は3ですが、reset (shift (λk. k ((k 1) + 1)) + 2)は6ですし、reset (shift (λk. k ((k 1) + 1))) + 2は4です。

Yusuke Endoh @mametter

@cocoa_ruto @mr_konn callcc (λk. (k 1) + 1) + 1 は reset (exit (shift (λk. k ((k 1) + 1)) + 2)) と同じという主張です。exit は引数を評価してプロセス終了するような何か

スマートコン @mr_konn

@mametter @cocoa_ruto 手で展開していくと、exit が正格評価と定められているのでちゃんと 3 を返して終わる筈ですね。

ると @cocoa_ruto

@mametter @mr_konn exitを許すならばそうなります。ただしネストした場合はexitではなく、「1つ外側の部分継続」になります。 gist.github.com/taku0/b3dd6298… で、その「1つ外側の部分継続」をどうやって取るのかという問題に行き着きます。

スマートコン @mr_konn

@cocoa_ruto @mametter あーネストした場合については全然考えてなかったですね……。そもそも shift/reset で call/cc を表現しようというのが間違いという事なんですかね？

ると @cocoa_ruto

@mr_konn @mametter 「1つ外側の部分継続」を動的スコープ変数に入れるとすれば、「call/ccとは、exit+shift/reset+動的スコープ変数」と言えます。

スマートコン @mr_konn

@cocoa_ruto なるほど……。そうするとあんまり綺麗じゃなくなってかなしいですね……。

ると @cocoa_ruto

@mr_konn @mametter 別の捉え方としては、部分継続が外側からk1, k2, k3であるときに、それにexitを付けて合成したexit.k1.k2.k3が普通の継続であるとも言えます(「部分」を全て繋げると「全体」になる)。

Yusuke Endoh @mametter

@mr_konn @cocoa_ruto @mametter プログラム内で shift/reset 使わないでください ^^ 使いたいなら、shift/reset でエンコードした callcc を使って shift/reset を定義してください

スマートコン @mr_konn

@mametter @cocoa_ruto あれ、今の話はcall/cc を二重以上にネストするという事ですよね……？