Skip to content

Latest commit

 

History

History
247 lines (187 loc) · 8.97 KB

2018-07-19-delimited continuationの夏.md

File metadata and controls

247 lines (187 loc) · 8.97 KB
Raw
layout title tags
post
delimited continuationの夏
Delimited Continuation
Racket
OCaml

こんにちは､びしょ〜じょです｡ control/promptとprompt tagへの理解が必要になったため､やっていきましょう｡

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､私も皆さんも 完全に理解した と思うので話を進めよう｡

Delimited continuation

和訳すると限定継続です｡これで9割は分かったと思うが､call/ccよりも取ってくる継続の範囲が限定されているというイッメジです｡ StackOverflowのこれ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の定義を見ます｡

\[ @importmd(src/20180710/shift.tex) \]

おk｡

ではshift0はどうかな?

\[ @importmd(src/20180710/shift0.tex) \]

えっ何が違うん? と一瞬困るわけですが､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を型で表そうとするとそんな雰囲気になるはずだ｡

control/prompt

だいたいshift/resetというと語弊があるが､だいたいそんな感じという認識がある(間違ってると思うのでご教授願います｡)｡ promptはcontrolと対応するdelimiterに過ぎず､動きとしてはreset同様に継続を区切るだけだ｡ "control prompt"で検索するときは､"-command"を付けないとコマンドプロンプトに関する話が大量に出てきて血管ブチ切れそうになる｡

controlは文献3より､ \[ @importmd(src/20180710/control.tex) \]

この論文では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
'()

わかった｡ とりあえずこのへんで 完全に理解した ということにいたしましょうか…｡

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を読めって話ですよ｡読んでへん｡

とりあえずここは 完全に理解した ということで､よろしいでしょうか｡

おわりに

なんとなくつかめてきた気がします｡ 夏服の剣持力也くんがうさんくさいメガネ掛けててよかった｡

Footnotes

  1. What exactly is a “continuation prompt?” ↩

  2. 浅井健一. "shift/reset プログラミング入門." ACM SIGPLAN Continuation Workshop 2011. 2011. http://pllab.is.ocha.ac.jp/~asai/cw2011tutorial/main-j.pdf ↩

  3. 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 ↩ ↩2 ↩3

  4. racket/controlのshiftはマクロ! はいごもっとも! ↩

  5. 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 ↩