OchaCamlで限定継続/answer type modificationを勉強する

限定継続は面白いのですが、型がつくとイマイチ自分にはよくわからなくなってしまいます…。何度目かの正直で、去年の Continuation Workshop 2011 Tutorialで紹介された OchaCaml を使って勉強してみます。何となくしか限定継続を分かってない自分用メモ。

難しいと感じる理由：型が変わる

自分が限定継続の型をムズカシイと思ってしまうのは

# reset (fun () -> 1);;
- : int = 1

のように、resetの中にshiftが無い場合にはそのままresetは恒等関数になるのに、ひとたび shift を使うと

# reset (fun () -> shift (fun k -> 1) ^ "abc");;
- : int = 1

reset の中が string なのに、 resetの外が int になってしまい、一貫した型がないように感じられてしまうから、のような気がします。これがいわゆる answer type modification なのですが、shift/resetには具体的にどういう型が付いているのか、調べてみます。

準備

まず、OchaCamlを起動して、answer typeを全て表示するように設定します。

$ ochacaml
#answer "all";;

answer type modificationと reset

answer typeとは何でしょう？理論は知らないのですが、継続渡し計算の型 ('a -> 'r) -> 'r の 'r が answer typeと呼ばれます。(この型 'r の値を便宜的に answer と呼ぶことにします。)
では answer type modificationとは。簡単な例として reset の型を見てみましょう

# reset;;
- : (unit / 'a -> 'a / 'b) -> 'b = <fun>

この型 (unit / 'a -> 'a / 'b) は、「 unit -> 'a なんだけど、実行したらanswer typeが 'a から 'b に変わる」という読むらしいです。この「実行したら型が変わる」というのは分かりにくいですが、最後に answer を'aから'bに変換する関数が走る、と思えばよさそうです。

shiftの型

# shift;;
- : (('a -> 'b) / 'c -> 'c / 'd) / 'b -> 'a / 'd = <fun>

ほとんどワケわからないので、引数の中でanswer type mod.が起こらないと仮定しましょう。
さらに '/' も取っ払ってみます。

- : (('a -> 'b) -> 'c) / 'b -> 'a / 'c = <fun>

(('a -> 'b) -> 'c) という(pureな)継続渡し計算を引数に取る
shift (...) そのものは型'aを持っている (継続のスタート地点/文脈の穴の型は'a)
shift全体としては、answer typeを 'b から 'c に変える

つまり、引数は shift がある位置から reset までの、型'a -> 'bの限定継続をもらって、それを 'c の値に変換するってことですね。これがそのまま answer type mod. の /'b -> .. / 'c に現れています。おおっ。

全体として

# reset;;
- : (unit / 'a -> 'a / 'b) -> 'b = <fun>

つきつめると、resetとは限定継続付き計算を実行し、answerを返す計算のようです。
reset の中の計算がpureなら、answer typeは変わらないので、型 unit / 'a -> 'a / 'a を持ちます (pureなunit->'a型の関数 (unit / 'c -> 'a / 'c) と (unit / 'a -> 'a / 'b) を単一化)。

- : (('a -> 'b) -> 'c) / 'b -> 'a / 'c = <fun>

一方、shift は、『限定継続 : 'a -> 'bをもらい、answer : 'cそのものを返す』という計算を使って、実際にanswerを変換する（と同時にresetまで脱出する） という感じでしょうか。

実験

ここまでの話とあまり関連しませんが少し例を書いてみます。
関数

let mydelim = fun f -> reset (fun () -> f () ^ "100") + 1;;

を定義します。 fの中から取れる継続は最終的に ^"100" と文字列を結合するところまでで「限定」されているわけですね。
ところでreset の中と外で型が変わってますね。型は

mydelim : (unit / string -> string / int) -> int = <fun>

で、 mydelim に渡す関数は必ずanswer typeをstringからintに変えなければならないようです。つまりfの中で必ずshift呼べってことですね。

mydelim はどんな値に適用できるでしょうか。

shiftを呼ばないのでanswer typeが変わらない→型エラー

shiftを呼ばないと

Toplevel input:
> mydelim (fun () -> "200");;
>          ^^^^^^^^^^^^^^^
This expression has type unit / string -> string / string,
but is used with type unit / string -> string / int.

などと怒られます。 (fun () -> "200") の型はこの出現位置だと上記の型ですが本来の型は unit / 'a -> string / 'a という「answer typeを変えない関数」ですね。 mydelim には answer type を変える関数を渡さなければならないので型エラーというわけ。

型付けできる例

# mydelim (fun () -> shift (fun k -> int_of_string (k "1234")));;
- : int = 1234101

shiftで resetまでの継続 ( ? ^ "100" ) をkに束縛し(?は穴)、それを "1234"で呼ぶと "1234100" が得られます。 shift は中身が完了するとresetまで大域脱出する(といっていいのか何なのか)ので、あとは int_of_string で整数にすれば、 reset の続き +1 とも型が整合する、と。

まとめ

限定継続のanswer type modificationの基本的なところを調べてみました。
次回以降(あれば)では、限定継続が制御を逆転するさまを調べてみたり、callerとcalleeがより複雑に相互作用する様子が型で表現されるとか、そういう方向の例を作ってみたいと思います。