delimited continuationの夏
こんにちは、びしょ〜じょです。 control/promptとprompt tagへの理解が必要になったため、やっていきましょう。
1. continuation??? 継続??? is power ???
継続とは "残りの計算" などと言われます。 \(e_1+e_2\)という式があって、左辺から計算がおこなわれていくとする。 \(e_1 \Downarrow v_1\)となると、残りの計算は\(\lambda x. x + e_2 \)となります。 \(\lambda x. x + e_2 \)はよく\([\ ]+e_2\)と表現され、この\([\ ]\)はholeと呼ばれたりする。 この継続を\(E\)などとおいて、\(E\)をぶっこ抜いてきてなにか値を渡したりするときは\(E[x]\)と表記し、holeに\(x\)が入っていく。 OK、私も皆さんも 完全に理解した と思うので話を進めよう。
2. Delimited continuation
和訳すると限定継続です。これで9割は分かったと思うが、call/ccよりも取ってくる継続の範囲が限定されているというイッメジです。 StackOverflowのこれ1が図解付きでわかりやすい。
2-1. shift/reset
久しぶりにRacket引っ張ってきます。Schemeでもなんでもdelimited continuationが使えれば良いですが。
Racketだとshift/resetを使うには(require racket/control)
する必要がある。
Guileだと(use-modules (ice-9 control))
やね。
(- 4 (call/cc (lambda (k) (+ 3 (k 20)))))
; displays "-16"
; (require racket/control)
(reset (- 4 (shift k (+ 3 (k 20)))))
; displays "-13"
(- 4 (shift k (+ 3 (k 20))))
; displays "-13" (work in the same way as above)
(- 4 (reset (shift k (+ 3 (k 20)))))
; displays "-19"
雑な説明でしたが、call/cc
は中のコンテキスト(+ 3 [])
も継続の呼び出し時に捨ててますね。
あとRacketのshift
はreset
が見つからなかったらエラーにならずに最外のコンテキストを持ってくるんですねぇ。
shift/resetの詳細は文献2をご覧ください。
…ちょっと待って! shift0
が無いやん! ということで文献3を見る。
まずshift
の定義を見ます。
\[ \begin{array}{r} M\left[\left(\mathtt{reset}\ C\left[\left(\mathtt{shift\ f}\ E\right)\right]\right)\right] \triangleright M\left[\left(\mathtt{reset}\ E'\right)\right]\\\ \mathrm{where}\ E'=E \{\mathtt{f}\mapsto \left(\mathtt{lambda}\ \left(\mathtt{x}\right)\ \left(\mathtt{reset}\ C[\mathtt{x}]\right)\right)\} \end{array} \]
おk。
ではshift0
はどうかな?
\[ \begin{array}{r} M\left[\left(\mathtt{reset}\ C\left[\left(\mathtt{shift0\ f}\ E\right)\right]\right)\right] \triangleright M\left[E'\right]\\\ \mathrm{where}\ E'=E \{\mathtt{f}\mapsto \left(\mathtt{lambda}\ \left(\mathtt{x}\right)\ \left(\mathtt{reset}\ C[\mathtt{x}]\right)\right)\} \end{array} \]
えっ何が違うん? と一瞬困るわけですが、shift0
では一発評価が進むとM
の中からreset
が消えてますね。
なのでE'
の中の最外のshift0
はM
まで行ってしまうわけです。
shift
とshift0
の違いを実際に文献の例から見てみます。
(reset (cons 'a
(reset (shift f (shift g '())))))
; returns '(a)
ここのreset
外のコンテキストM
は(reset (cons 'a []))
となる。
つまり変換規則で対象となっているreset
は内側のほう。
shift
外のコンテキストC
は[]
、つまり空ですので最外のshift
が対象となっている。
E
は(shift g '())
となる。
ではワンステップすすめるとM[(reset E{f := (lambda (x) (reset C[x]))})]
なので
(reset (cons 'a
(reset (shift g '()))))
あとは同様にやっていく。内側のreset
をやっていくので(reset (cons 'a (reset '())))
で、あとはアーナンダビッグステップに行くぞということで'(a)
が得られる。
続いてshift0
について見よう。
文献3ではdelimiterはreset
のみだったが、racket/controlのshift0
に対応するdelimiterはreset0
となる。
(reset0 (cons 'a
(reset0 (shift0 f (shift0 g '())))))
; returns '()
オッなんか違うな。当然違うわけだ。
だいたい形は同じなのですが、
ワンステップすすめるとM[(E{f := (lambda (x) (reset0 C[x]))})]
となる。
E
の外にreset(0)
がつかないわけだ。
(reset0 (cons 'a
(shift0 g '())))
でreset0
とshift0
の間のコンテキストは拾われずにshift0
内のexpressionが生き残るので、'()
を返す。
あ〜〜 完全に理解した 。 この "resetは1度しか使えない" という回数制限はlinear logicの影が潜んでいそうだ。 実際この回数制限nessを型で表そうとするとそんな雰囲気になるはずだ。
2-2. control/prompt
だいたいshift/resetというと語弊があるが、だいたいそんな感じという認識がある(間違ってると思うのでご教授願います。)。
prompt
はcontrol
と対応するdelimiterに過ぎず、動きとしてはreset
同様に継続を区切るだけだ。
"control prompt"で検索するときは、"-command"を付けないとコマンドプロンプトに関する話が大量に出てきて血管ブチ切れそうになる。
control
は文献3より、
\[
\begin{array}{r}
M\left[\left(\mathtt{reset}\ C\left[\left(\mathtt{control\ f}\ E\right)\right]\right)\right] \triangleright M\left[\left(\mathtt{reset}\ E'\right)\right]\\\
\mathrm{where}\ E'=E \{\mathtt{f}\mapsto \left(\mathtt{lambda}\ \left(\mathtt{x}\right)\ \left(C[\mathtt{x}]\right)\right)\}
\end{array}
\]
この論文ではdelimiterがreset
だがとりあえずOKとしたい。
f
にバインドされる継続の中にreset
がないという点でshift
と異なっている。
論文の例を見てみよう。
(reset (let {[y (shift f (cons 'a (f '())))]}
(shift g y)))
; returns '(a)
Racketは3種類のカッコが使えるからS式もちょっぴり分かりやすくなるぞ! これを規則にそって解いてくと次のように進む。
; 1
(reset (cons 'a
[(lambda (x) (reset (let {[y x]} (shift g y))))
'()]))
; 2
(reset (cons 'a
(reset (let {[y '()]} (shift g y)))))
; 3
(reset (cons 'a (reset shift g '())))
; 4
(reset (cons 'a (reset '())))
; 5
'(a)
ふむふむ。はい。
ではshift
をcontrol
にしたらどうなるか―
(reset (let {[y (control f (cons 'a (f '())))]}
(control g y)))
; returns '()
結果が異なるわけだな。
; 1
(reset [cons 'a
((λ (x)
(let {[y x]} (control g y)))
'())])
; 2
(reset [cons 'a
(let {[y '()]} (control g y))])
; 3
(reset [cons 'a (control g '())])
; 4 gが使われないので `[cons 'a ...]` が破棄される
(reset '())
; 5
'()
わかった。 とりあえずこのへんで 完全に理解した ということにいたしましょうか…。
3. prompt tag
継続をキャプチャするオペレータ(shift
, shift0
,control
など)はそれぞれ対応する、取るべき継続を区切ってくれるdelimiterがある。
例えばracket/controlではshift
に対応するのはreset
で、shift0
にはreset0
が対応する。
更には同じshift
でも、shift
式4のコンテキストで最も近いreset
が動的に対応付けられる。
この、shift
やcontrol
などのcontrol operatorとdelimiterの対応をもっと柔軟にしたい! という要望に応えるのがprompt tagである。
(let {
[p (make-continuation-prompt-tag 'p)]
[p~ (make-continuation-prompt-tag 'p~)]}
(reset-at p
(+ 3 (reset-at p~
(begin
(shift-at p f {begin
(display "this is p")
(f 4)})
(shift-at p~ g {begin
(display "this is p~")
(g 20)}))))))
; display "this is pthis is p~23"
確かに、最寄りのreset
ではなく、プロンプトに対応するreset-at
の継続を取っている。
ちなみにOCamlのdelimited continuationライブラリdelimccでは、prompt tagのみが使われている。
なんだか日本語が足りないが、Racketのshift
やreset
はなく、shift-at
やreset-at
のみ、という感じ。
let open Delimcc in
let p = new_prompt () in
let reset = push_prompt p in
let shift f = shift0 p f in
reset @@ fun () -> List.cons `A @@
reset @@ fun () -> shift @@ fun f -> shift @@ fun g -> [];;
(* returns [] *)
これは何故か。多分answer-type polymorphismをOCamlではサポートしてないからじゃないかな。 詳細はdelimccに関する文献5を読めって話ですよ。読んでへん。
とりあえずここは 完全に理解した ということで、よろしいでしょうか。
4. おわりに
なんとなくつかめてきた気がします。 夏服の剣持力也くんがうさんくさいメガネ掛けててよかった。
-
浅井健一. "shift/reset プログラミング入門." ACM SIGPLAN Continuation Workshop 2011. 2011. http://pllab.is.ocha.ac.jp/~asai/cw2011tutorial/main-j.pdf ↩
-
Shan, Chung-chieh. "Shift to control." Proceedings of the 5th workshop on Scheme and Functional Programming. 2004. ftp://cs.indiana.edu/pub/techreports/TR600.pdf#page=103 ↩
-
racket/controlの
shift
はマクロ! はいごもっとも! ↩ -
Oleg Kiselyov. "Delimited Control in OCaml, Abstractly and Concretely: System Description." FLOPS 2010. 2010. https://link.springer.com/chapter/10.1007/978-3-642-12251-4_22 ↩