こんにちは､びしょ〜じょです｡
修士中間発表終わったのでもう研究しなくてOK!!!!!!!!
1. はじめに
突然ですがみなさんエフェクトを発生させていますか｡ ところでエフェクトはどこで発生するのでしょうか｡ あ! とりあえずcall-by-valueでいいですか｡はい｡
エフェクトは値でないexpression､つまり関数呼び出しで発生する､というのはなんとなく分かるんじゃないでしょうか｡ 値を使ったり変数を参照したり1するだけでなんかよくわからんことが起きては困る｡
let comp () = (print_endline "hello"; 3);;
let f x = x + 5;;
let v = comp () in (* ここで発生 *)
f v
ところで計算エフェクトの発生に印を付けたいのですがOCamlでは…｡
2. notion of computation
effect-and-type systemを思い出してみましょう｡
なにかt型の値を返すが､途中に計算エフェクトTが発生する場合､T tと書いたりします｡
高カインド型は今回あまり触れないかもしれないですが､念の為Haskellでいきましょう｡
Scalaもあるがエフェクトがどこでも発生させられるので今回はやめておこう｡
自分､ -XStrict いいっすか
2-1. 値の取り出しと継続
T tからtを取り出したいときはどうするんでしょうか｡
そうだね､bind((>>=) :: T t -> (t -> T u) -> T u)だね(プログラム2.1)｡
comp () >>= (\v -> f v) -- わかりやすくeta expansion
左辺で計算エフェクトが発生しつつ値が出てきて(T t)､値を取り出して(t)処理をおこなって値を返す(T u)｡
ところでHaskellならdoがありますねえ(プログラム2.2)
do
v <- comp (); -- 手続き感を出すためにケツセミコロン
f v
2.1から2.2への変換はみたまんまで､do(の一部)は>>=の糖衣構文である｡
ところでこの変換により､bindの右辺がdo記法における残りの計算部分､つまり継続になることが分かる｡
>>=でチェインしまくるのがCPSを手で書くことにあたるのに対し､doによる書き方はCPSをうまく隠蔽しています｡
3. A-Normal Form､あるいはMonadic Normal Form
ところでOCamlはエフェクト発生させ放題プランに加入してるのでどこでもエフェクトが発生します(プログラム3.1)｡
let comp () = (print_endline "hello"; 3);;
let f x = x + 5;;
print_int @@ f @@ comp () + comp () (* prints "hello\nhello\n11" *)
計算エフェクトがどこで起きるのかよくわかんね〜〜
e1 e2のような場合､先にe2で発生しうるエフェクトを解消してから､つまり評価をおこなって出てきた値を､e1を評価して出てきた関数に渡したい｡
ではexpressionがネストしないような形にしよう(プログラム3.2)｡
let v1 = comp () in
let v2 = comp () in
let v3 = v1 + v2 in
let v4 = f v3 in
print_int v4
このような形式はA-Normal Form(略してANF)と呼ばれ､letの右辺はredexが一つしか無い状態に制限されている｡
それにしてもこれは2.2に近いですねえ｡
MoggiがHaskellのモナドのコンセプトとなる論文[2]で計算エフェクトを扱う計算体系として提案しているものは､let (x : t) <= (e1 : T t) in (e2 : T u)のように非常にANFに似た形の構文を持っている｡
そしてANFはMonadic Normal Formともよばれている[3]｡
>>=のシグネチャを思い出してみると､letをラムダ抽象でエイヤッできることと合わせれば言いたいことが分かる｡
4. 受け継がれるdo､そして継続はなぜ現れるのか
時は令和､現在計算エフェクトを扱う機能として代数的効果が爆流行りである[要出展]｡ いや令和は関係ないんですが､代数的効果という概念の初出が2003年なので､計算機科学においては非常に新しいものである｡ 代数的効果とは､計算エフェクトを代数的に扱うような言語機能である｡ 代数的に､というのはソレ自体には意味がなく､ただ構造があるだけで…なんたらかんたら…｡ では意味はどこで付くかというと､ハンドラというものによって与えられる｡ 代数的や例外というキーワードから､とりあえずOCamlの例外機構を思い出してもらえるとなんとなく分かってもらえるかもしれない｡
Eff[4] [5]という言語で例を見てみよう(プログラム4.1)｡
[4]との構文的な差分として､エフェクトの発生にはわかりやすさのため､慣習的に使われる#をつけるようにした｡
do n <- #get () in
if n < 0 then
#print "B"
return -n^2
else
return n + 1
handle
#get((); n.
if n < 0 then
#print("B"; _.
return -n^2)
else
return n + 1)
with
| #get((); k) -> k 10
| #print(v; k) -> write_stdout v; k ()
このdesugaringを見てみると､エフェクトが>>=の左辺､継続が右辺に対応しそうだ｡
Haskellにおける型クラスのようにimplicitに実装が与えられるのではなく､例外発生箇所をハンドラでexplicitにハンドルするというところが異なりますね｡
エフェクトが発生するとハンドラにコントロールが移り､エフェクトの引数がパターンマッチ風に渡る｡ ハンドラでは継続がファーストクラスで使える｡ 継続はつまりハンドルされている式の残りの部分なので､継続を実行するとコントロールがハンドラから元の式に戻る｡
エフェクトを扱いたい場合に継続はなぜ現れるのか､分かってきたかもしれません｡
エフェクトに意味を与えるもの(Monadのインスタンス､エフェクトハンドラ)にコントロールが移ったあと､元の式に復帰するためには継続をハンドラに渡して呼んでもらうのがシンプルである｡
そして､Listモナドとか､非決定計算など､継続が複数回(あるいは末尾位置以外で)呼び出されるのがそもそも計算エフェクトに織り込まれている場合もあり､継続がファーストクラスであることがそもそもエフェクトシステムには必要なのである｡
5. 継続からエフェクトへ
5-1. OCaml4.08のbinding operator
OCaml4.08で新たな構文拡張が生まれました｡ 詳細はこちらに書いた｡
簡単にいうと､ただならぬletが定義できる(プログラム5.1)｡
(* val ( let* ) : 'a option -> ('a -> 'b option) -> 'b option *)
let (let*) x k =
match x with
| Some v -> k v
| none -> none
let return x = Some x
let* x = Some 5 in
return (x + 10)
継続が使えるようになったのでeffectfulな計算を手続き的に書けるようになった､という逆の流れである｡
流れは逆であるが､やりたかったのは上記のようにmonadicなletである｡
=< 4.07まではppxによる拡張もあり､非常に期待されていた機能である｡
5-2. ContT
継続があれば計算エフェクトを手続き的に書けるのか! ということでcontinuationモナドになんでも突っ込めばいいんじゃないか｡
そこでContT monad transformerです｡
という話を読みました!!!
6. おわりに
継続はつよい
エフェクトフルコンピュテーションはおもしろい
DSLの組み立てにも継続がめっちゃ使えるやんみたいな話を書こうと思ったけど別の機会に｡
この記事はHERP労働時間に書かれた｡ HERPは本物のcontinuationプログラマーも募集しています｡
-
変数の参照もエフェクトとして考えることができるがここでは割愛 ↩
-
Moggi, Eugenio. "Notions of computation and monads." Information and computation 93.1 (1991): 55-92. ↩
-
Danvy, Olivier. "A new one-pass transformation into monadic normal form." International Conference on Compiler Construction. Springer, Berlin, Heidelberg, 2003. ↩
-
Pretnar, Matija. "An introduction to algebraic effects and handlers. invited tutorial paper." Electronic Notes in Theoretical Computer Science 319 (2015): 19-35. ↩
-
Eff Programming Language - https://www.eff-lang.org/ こちらの実際のプログラム言語はMLっぽい構文になっているので本文では[4] に従う｡ ↩