RacketにはRnRSで定義されているcall/ccやdynamic-wind、例外処理、動的束縛に加えて、shift/reset、control/prompt等々といった種々の限定継続オペレータが定義されている。
これらの機能がどのように相互作用するのか理解していなかったので、Adding Delimited and Composable Control to a Production Programming Environmentに書かれている意味論を読みながらメモをしていく。
構文と評価文脈
e ::= m
| (wcm w m)
m ::= x
| v
| (e e ...)
| (begin e e)
| (% e e e)
| (dw x e e)
v ::= (list v ...)
| (λ (x ...) e)
| (cont v E)
| (comp E)
| dynamic-wind
| abort
| current-marks
| cons
| u
u ::= call/cc
| call/comp
| call/cm
w ::= ((v v) ...)
E ::= W
| W[(dw x e E e)]
W ::= M
| (wcm w M)
M ::= []
| (v ... W e ...)
| (begin W e)
| (% v W v)
D ::= []
| E[(dw x e [] e)]
意味論
プロンプト
% は call-with-continuation-prompt に相当する。 prompt-tag, proc, abort 時の handler を引数に取る。
prompt-v
(% v1 v2 v3)
↝ v2
プロンプトの本体部分 v2 が値になったら、それがプロンプト式全体の値になる。
begin
RnRS の beginと同じ。
begin-v
(begin v e1)
↝ e1
begin は左から右に評価し、最初の式が値になったら、その値を破棄し、次の式を評価する。
dynamic-wind
RnRS の dynamic-wind とおおむね同じ。
dw
(dynamic-wind (λ () e1) (λ () e2) (λ () e3))
↝ (begin e1 (dw x1 e1 e2 e3))
where x1 is fresh
dynamic-wind は dw という内部表現に変換する。
このとき、各 dw を識別するために、評価時に新しい識別子 x1 を生成する。
また、 R[567]RSでは dynamic-wind の before/after thunk に継続を使って出入りした場合の挙動は未規定だが、この意味論では、 begin + dw に変換することで挙動を定めている。
dw-v
(dw x e1 v1 e3)
↝ (begin e3 v1)
dw の本体部分が値 v1 になったら、 e3 を評価した上で、 v1 を結果として返す。
abort
abort は abort-current-continuation に相当する。 prompt-tag と v を受け取る（多値には未対応）。
abort
(% v1 W2[(abort v1 v2)] v3)
↝ (v3 v2)
where W2 ≠ E[(% v1 E v)]
abort で指定したタグ v1 を持つ直近のプロンプトまで脱出する。 abort に渡した値 v2 は、プロンプトのハンドラ v3 に渡る。外側のプロンプトは残らない。
where で指定した条件で、プロンプトが直近のものになることを保証している。
abort-post
(dw x1 e1 W2[(abort v1 v2)] e2)
↝ (begin e2 (abort v1 v2))
dynamic-wind の本体部分で abort した場合は、after thunk を実行した上で abort 処理を再開する。
composable continuation
call/comp
call/comp は call-with-composale-continuation に相当する。 prompt-tag と proc を取る。
(% v2 E2[(wcm w1 (call/comp v1 v2))] v3)
↝ (% v2 E2[(wcm w1 (v1 (comp E2)))] v3)
where E2 ≠ E[(% v2 E v)]
call/comp を呼び出すと、指定したタグ v1 を持つ直近のプロンプトまでの継続をcomposable continuationとして切り出す。プロンプトは継続に含まない。また、 call/comp の呼び出しに付加されたcontinuation markも切り出された継続には含まない。
comp-pre
composable continuationの起動（dw 付き）。
((comp W1[(dw x e1 E2 e2)]) v1)
~> ⟦W1[(begin e1 (dw x1 e1 ((comp E2) v1) e2)]⟧_{wcm}
composable continuationのトップレベルが（wcmで包まれた）dwの場合、まずbefore thunkを実行し、 dw を外側に移したうえで、composable continuationを適用する。このとき、もとの継続に付加されていたcontinuation markは意味関数 ⟦・⟧_{wcm} で外側の文脈に付加しなおす（後述）。
comp
composable continuationの起動（dw なし）。
((comp W1) v1)
~> ⟦W1[v1]⟧_{wcm}
dw がない場合は、単純に call/comp で切り出した文脈に引数の値を挿入する。ただし、もとの継続に付加されていたcontinuation markは意味関数 ⟦・⟧_{wcm} で外側の文脈に付加しなおす。
意味関数 ⟦・⟧_{wcm} の定義は以下の通り。
⟦e1⟧_{wcm} = e1
where e1 ≠ (wcm w e)
⟦(wcm () e1)⟧_{wcm} = e1
⟦(wcm ((v1 v2) (v3 v4) ...) e1)⟧_{wcm} =
= (call/cm v1 v2 (λ () ⟦(wcm ((v3 v4) ...) e1)⟧_{wcm}))
意味関数 ⟦・⟧_{wcm} は wcm を call/cm に置き換える。こうすることで、継続を起動した場所のcontinuation frameに破壊的にcontinuation markを追加する（wcm-set や wcm-add 規則を参照）。
このようにせず、継続の起動ごとにcontinuation frameを作成して、そこにcontinuation markを付加するようにすると、継続を末尾位置で起動した場合でもリソースを消費するようになってしまう。
non-composable continuation
Racketの call/cc は full-continuation ではなく、指定されたプロンプトまでの継続を切り取る。 call/comp で切り出した継続とは起動時の意味論が異なる。 delimited/full continuation という関係ではなく、 composable/non-composable continuation の違いと見るのがよいと思う。
call/cc
call-with-current-continuation 相当。 RnRS と異なり、 prompt-tag を取る。
(% v2 E2[(wcm w1 (call/cc v1 v2))] v3)
↝ (% v2 E2[(wcm w1 (v1 (cont v2 E2)))] v3)
where E2 ≠ E[(% v2 E v)]
call/comp とほぼ同じ。non-composable continuationは起動時にもタグを見るので、 cont の下にタグ v2 を持っておく。
cont-post
non-composable continuation の起動で dynamic-wind のafter thunkが起動するケース。
(% v2 D2[E3[(dw x1 e1 W5[((cont v2 D6[E4]) v1)] e2)]] v3)
↝ (% v2 D2[E3[(begin e2 ((cont v2 D6[E4]) v1))]] v3)
where
D2[E3] ≠ E[(% v2 E v)], -- (1)
sameDWs(D2, D6), -- (2)
W5 ≠ E[(% v2 E v)], -- (3)
noShared(E3[(dw x1 e1 W5 E2)], E4)
contは v2 として捕捉時のタグを覚えているので、そのタグに対応する直近のプロンプトを探す。
条件 1, 3 でプロンプトが直近のものであることを保証する（1は dw の外側に他の対応するプロンプトがないこと、3は dw の内側に他に対応するプロンプトがないことを保証する）。
条件 2, 4 は必要なafter thunkだけが実行されることを保証する。
sameDWs と noShared の定義は以下の通り。
sameDWs(W1, W2)
= true
sameDWs(W1[(dw x1 e1 E1 e2)], W2[(dw x1 e1 E2 e2)])
= sameDWs(E1, E2)
otherwise = false
noShared(W1[(dw x1 e1 E1 e2)], W2[(dw x1 e1 E2 e2)])
= false
otherwise = true
sameDWs は文脈内の dw 列が同一であることをチェックする。
noShared は文脈内の最初の dw が同一でないことをチェックする。
cont 実行前の文脈は D2[E3[(dw x1 ...)]] で、実行後の文脈は D6[E4] になる。このとき、 continuation frame は以下のようになる。
実行前
D2 E3 x1
<-----> <-----> <->
..-%--...--o--...--o---o
実行後
D6 E4
<-----> <----->
..-%--...--o--...--o
この場合、 D2 と D6 は同一の dw 列を持つので before/after thunk を実行する必要がない。 E3 + x1 と E4 は同一の dw を共有しないため、この評価規則では、まず最内の x1 のafter thunkを実行する。
cont-pre
non-composable continuation の起動で dynamic-wind の before thunk が起動するケース。
(% v1 D2[W3[((cont v1 k1) v2)]] v3)
↝ (% v1 D6[W4[(begin e1 (dw x1 e1 ((cont v1 k1) v2) e2))]] v3)
where
k1 = D6[W4[(dw x1 e1 E5 e2)]], -- (1)
D2[W3] ≠ E[(% v1 E v)], -- (2)
sameDWs(D2, D6), -- (3)
noShared(W3, W4[(dw x1 e1 E5 e2)]) -- (4)
1の条件は読みやすさのため、2は直近のプロンプトを選択するため、3, 4 は必要なbefore thunk を実行するための条件である。
実行前後で continuation frame は以下のようになる。
実行前
D2 W3
<-----> <----->
..-%--...--o--...--o
実行後
D6 W4 x1
<-----> <------> <->
..-%--...--o--....--o---o
D2 と D6 は同一の dw 列を持つのでbefore/after thunkを実行する必要はない。 W 自体は dw を含まない文脈である。 cont の中にさらに dw が含まれる場合は、上図の x1 までが次の D2 の範囲になり、内側のbefore thunkが実行される。
cont
non-composable continuation の起動で dynamic-wind のbefore/after thunk が実行されないケース。
(% v1 D2[W3[((cont v1 D6[W4]) v2)]] v3)
↝ (% v1 D6[W4[v2]] v3)
where
D2[W3] ≠ E[(% v1 E v)],
sameDWs(D2, D6),
noShared(W3, W4)
D2 と D6 は同一の dw 列を持ち、W3 と W4 は dw を持たないので実行すべきbefore/after thunk はない。
continuation mark
marks
(% v2 E2(current-marks v1 v2) v3)
↝ (% v2 ⟦E2, v1, (list)⟧_{marks} v3)
where
E2 ≠ E[(% v1 E v)]
⟦・, ・, ・⟧_{marks} の定義は以下の通り。
⟦[], v, e2⟧_{marks}
= e2
⟦(wcm w1 E1), v1, e2⟧_{marks}
= ⟦E1, v1, (cons v3 e2)⟧_{marks}
where w1 = ((v v) ... (v1 v3) (v v) ...)
⟦(wcm w1 E1), v1, e2⟧_{marks}
= ⟦E1, v1, e2⟧_{marks}
where v1 ∉ Dom(w1)
⟦(v ... E1 e ...), v1, e2⟧_{marks}
= ⟦E1, v1, e2⟧_{marks}
⟦(begin E1 e), v1, e2⟧_{marks}
= ⟦E1, v1, e2⟧_{marks}
⟦(% v E1 v), v1, e2⟧_{marks}
= ⟦E1, v1, e2⟧_{marks}
⟦(dw x e E1 e), v1, e2⟧_{marks}
= ⟦E1, v1, e2⟧_{marks}
直近の対応するプロンプトまで切り出したものを渡し、 wcm をたぐっていってキー v1 に対応する値を集めてくる。
wcm
call/cm が with-continuation-mark に相当する。 wcm 相当のものは実コード上には陽に現れない。
wcm-v
(wcm w v1)
↝ v1
wcm の本体部分が値になったら、それが wcm 式全体の値になる。
wcm-set
(wcm ((v1 v2) ... (v3 v4) (v5 v6) ...)
(call/cm v3 v7 (λ () e1))
↝ (wcm ((v1 v2) ... (v3 v7) (v5 v6) ...) e1)
call/cm を使うとキーを指定して外側の wcm の continuation mark を書き換えることができる。
wcm-add
(wcm ((v1 v2) ...)
(call/cm v3 v4 (λ () e1))
↝ (wcm ((v1 v2) ... (v3 v4)) e1)
where v3 ∉ (v1 ...)
外側の wcm に対応するキーがない場合は新たにエントリを追加する。
wcm-intro
E1[(u1 v1 ...)]
↝ E1[(wcm () (u1 v1 ...))]
where E1 ≠ E[(wcm w [])]
意味論上 wcm が必要な場合にそれを補う規則。 where の条件で wcmが入れ子にならないようにしている。
TODO
shift/reset, control/prompt、動的束縛、例外処理の実現方法の概要を説明する。
概要:
-
shift/reset,control/prompt等のプロンプトの設定はcall-with-continuation-promptで実現し、継続の切り出しはcall-with-composable-continuationで実現されている。これらのオペレータでは、切り出した継続はshiftやcontrolの継続からは取り除かれる。一見、abort-current-continuationで継続を破棄すればよいように見えるが、それではresetやpromptで設定したプロンプトまで破棄されてしまう（abort 規則を参照）。これらの限定継続オペレータは外側のプロンプトは残したいので、call-with-current-continuationをつかってプロンプトを残したまま継続をすげかえる（例えば cont 規則を参照）。ちなみに、shift0/reset0やcontrol0/prompt0のような外側のプロンプトを残さない限定継続オペレータはabort-current-continuationを使って実現できる。 - 動的束縛はcontinuation markで実現されている。
- 例外処理は、
with-exception-handlerの呼び出しごとに continuation mark に例外ハンドラを設定することで実現している（例外ハンドラが起動したときにcontinuation-marksで例外ハンドラ列を取り出す。ハンドラ実行中の例外ハンドラはいい感じに設定する）。ところで、 RnRS のguard式では、 clause で例外を処理した場合は、その処理結果がguard式の値になる。これは、guardの外側にプロンプトを設定し、 clause の処理結果でそのプロンプトまでabort-current-continuationすることで実現している。このとき、ハンドラに値を返すためのプロンプトとそれ以外の継続操作を区別するためにプロンプトタグを使っている。
付: shift/reset, call/cc の関係
下記の意味論は Final Shift for Call/cc: Direct Implementation of Shift and Reset による。
⟦_⟧_ : Expr → Env → Cont -> Val
Env = Expr → Val
Cont = Val → Val
⟦x⟧ρ = λk. k (ρ x)
⟦λx. M⟧ρ = λk. k (λv.λkʹ. ⟦M⟧(ρ[x↦v]) kʹ)
⟦E1 E2⟧ρ = λk. ⟦E1⟧ρ (λf. ⟦E2⟧ρ (λa. f a k))
⟦call/cc E⟧ρ = λk. ⟦E⟧ρ (λf. f (λv.λkʹ. k v) k)
⟦reset E⟧ρ = λk. k (⟦E⟧ρ (λv. v))
⟦shift c M⟧ρ = λk. ⟦M⟧(ρ[c↦λv.λkʹ. kʹ (k v)]) (λv. v)
shift/reset と call/cc ありのλ計算の意味を、それらのないλ計算への変換で表現すると上記のようになる（continuation semantics）。
ところで、この意味論では、 reset の変換後の項に末尾呼び出しでない適用があるので、右辺にさらにCPS変換をかける。
⟦_⟧_ : Expr → Env → Cont → MCont -> Val
Env = Expr → Val
Cont = Val → MCont → Val
MCont = Val → Val
⟦x⟧ρ = λk.λm. k (ρ x) m
⟦λx. M⟧ρ = λk.λm. k (λv.λkʹ.λmʹ. ⟦M⟧(ρ[x↦v]) kʹ mʹ) m
⟦E1 E2⟧ρ = λk.λm. ⟦E1⟧ρ (λf.λmʹ. ⟦E2⟧ρ (λa.λmʺ. f a k mʺ) mʹ) m
⟦call/cc E⟧ρ = λk.λm. ⟦E⟧ρ (λf.λmʹ. f (λv.λkʹ.λmʺ. k v mʺ) k mʹ) m
⟦reset E⟧ρ = λk.λm. ⟦E⟧ρ (λx.λmʹ. mʹ x) (λr. k r m)
⟦shift c M⟧ρ = λk.λm. ⟦M⟧(ρ[c↦λv.λkʹ.λmʺ. k v (λw. kʹ w mʺ)])
(λw.λmʹ. mʹ w)
m
さらに継続っぽい引数が増えるので、 MCont の方をメタ継続と呼ぶことにする。この意味論をmeta-continuation semanticsと呼ぶ（Abstracting Control も参照。ちなみに、さらにCPS変換をくり返して、メタ継続、メタメタ継続……を操作するような shift/reset の変種を考えることもできる）。
reset 以外はメタ継続を操作しないので、地道にメタ継続引数を渡していく。
reset は継続を空の継続 λv.λm. m v にし、もとの継続をメタ継続に移したうえで本体部分 E を評価する。
この方向で進むと、 call/cc は reset でメタ継続に移された継続は触れないので、 Racket の call/cc がプロンプトを見るのは素直な流れのように見える。