こんにちは、びしょ〜じょです。 これは言語実装Advent Calendar 2018の9日目の記事です。 最初は "変数が全部箱の言語の設計と実装" と題して全部optionにくるまれてる参照とかそういう感じの何かを作ろうとしたけど多分面白くなくなって筆者の熱も醒めると思ったのでやめた。 またそうこうしてるうちに良い感じのものが作れたので、論理的背景を整理するためにも内容を再考して今回のような内容となりました。 ほならね早速いってみましょう。

1. はじめに

Algebraic effects and handlers(以降 "algebraic effects" と省略)は、いわば限定継続を取れる例外である。 try節をdelimiterとし、例外発生位置から残りの計算を限定継続として受け取り、継続をもちいて例外から復帰したり、単に継続を捨てて例外として扱うこともできる。 最近各所で注目されており、組み込みの言語機能やライブラリとしていくつか提供されている。 しかし、強力なコントロールオペレータとしての様々な使用が期待される一方、実装はそれほど多くないのが難点である。

Asymmetric coroutinesは、コントロール抽象化機構の一つであり、ノンプリエンプティブなマルチタスクをおこなうことができる。 Lua、Rubyなどの言語機能またはライブラリとして提供されており、様々な場面で使うことができる。 一方コントロールオペレータとして扱うには操作が低級であり、スパゲッティコードになりがちである。

本稿では、oneshot algebraic effectsからasymmetric coroutinesへの変換、つまり、asymmetric coroutinesによる、継続の使用をワンショットに制限したalgebraic effectsの実装を考える。 これによりalgebraic effectsをよりカジュアルにあつかえるようになり、さらにasymmetric coroutinesよりも高級なコントロールの操作により、コードを簡潔に書くことが期待される。

コントロールオペレータとしてのasymmetric coroutinesについて述べ、asymmetric coroutinesとoneshot algebraic effectsとの関係について述べる。 余力があれば実際に変換を考え、変換を元にした実装を眺める。 変換の正しさについては証明はないため、読者への課題、あるいは筆者の研究の一環とする。

本稿の実装はLuaのモジュールとして公開してある。 お手元にご用意したりして本稿をお楽しみください。

2. algebraic effects

これについては直近でそこそこ話したので、あれとかこれとかそれとかをご参照ください。

2-1. Core Eff

今回は1つのハンドラでハンドルできるエフェクトは1つというCore Effという言語を考える(図2.1)。 [1]を参考にした。

\\[ \begin{array}{rrl} x & \in & \text{\textit{Variables}}\\\\ \text{\textit{eff}} & \in & \text{\textit{Effects}}\\\\ v & ::= & x \mid h \mid \lambda x. e \mid \mathtt{perform}\ \text{\textit{eff}}\ v \\\\ e & ::= & v \mid v\ v \mid \mathtt{let}\ x=e\ \mathtt{in}\ e\\\\ &\mid & \mathtt{inst}\ \left(\right) \mid \mathtt{with}\ h\ \mathtt{handle}\ e \\\\ h & ::= & \mathtt{handler}\ v\ \left(\mathtt{val}\ x \rightarrow e\right)\ \left(\left(x, k\right)\rightarrow e\right) \end{array} \\] 図2.1. the syntax of Core Eff

ラムダ計算にletが付いて、あとはalgebraic effects関連の項が追加されている。 inst ()でエフェクトインスタンスを生成する。 エフェクトインスタンスは任意のエフェクト定義に対応する。 例えばStateモナドっぽいStateエフェクトを定義するとなどきに、ハンドラと対応するエフェクトを一意に定められるという点とか各所メリットがある。 perform eff eは引数eを渡しエフェクトeffを発生する。 handler eff vh effhでエフェクトeffのハンドラを定義する。 vhはvalue handlerとなり、ハンドラがエフェクトをハンドルしきって値を返すときにvalue handlerによりハンドルした値を返す。 effhはエフェクトの引数と継続を取る。

ハンドルできるエフェクトが少ないため一見して弱くなったか? と思うがそんなことはない。 [1]ではエフェクトにADTを渡してハンドラ内でさらにパターンマッチする方法で事実上n個のエフェクトをハンルするようにしている。

意味論に関してはっきりと示せる自信がない(面倒くさいとも言う)のと、後述のように継続の使用回数を制限するので省略します。 [2]にあるような、よくあるcall by valueの体系を想定している。 次の例題で雰囲気を掴んでもらいたい。

2-2. 例題

let choose = inst () in (* instantiate *)
let lh = handler choose
          (val x -> x)
          (((l, r), k) -> k l) (* choose left *)
in
with lh handle (perform choose (3, 10)) + 5 (* returns `8` *)

突然tupleが出てきましたが、純真な心で呼んでみてください。 inst ()が返す値はeffect instancesの中でuniqueならなんでもいい。 ハンドラlhを定義する。 エフェクトハンドラ((l, r), k) -> k lを見ると、(l, r)というtupleを受け取って継続kにlだけ渡してrは捨てる。

2-3. oneshot algebraic effects

今回はさらに、継続の使用を高々1回に制限する。 マイナーな言語機能でさらに制限を加えてしまっているが、例えばMulticore OCamlは原則的に継続の使用は1回に制限されている3。 例えば次のような例(コード2.2)はNGにしたい。 continuationを2回使ってはいけない(戒め)。

ocamlコード2.2. NG: using k twice
let p = inst E in
with (handler p
  (val x  -> x)
  ((x, k) -> print (k (k x)))) (* NG!!! 2回使うな!!! *)
handle 3 + perform (E 3)

Affine typesなどにより継続を2回使う箇所を検出したいが、それはまたいつかお話しましょう。 高級な型システムでなくても、継続に適当な型を付けてdef-use chainを使えばヒューリスティックに解決できそうですね。

今回は継続を2回以上使ってはいけないお約束しかないので誰も注意してくれない。 そのため我々が注意するしかない。

継続が1回しか使えないのはmultishot(ノーマルな) algebraic effectsと比較すると真にパワーが弱くなっている。 とはいえ継続を2回も使う必要のない場面[4]が多く、継続がワンショットであることを前提にするとパフォーマンスの良い実装ができる[5][6]。

3. asymmetric coroutines

3-1. asymmetric?

非常に簡単に説明すると、みなさんがお使いのコルーチンは概ねasymmetric coroutineです。 Asymmetric coroutineがあるのでsymmetric coroutineももちろん存在する。 Asymmetric coroutinesは対象のコルーチンへ飛ぶ操作resumeと操作してるコルーチンから戻る操作yieldの2つを持つ。 一方symmetric coroutinesはコントロールを移すという唯一の操作controlのみを持ちます(表3.1)。

表3.1. the comparision of a?symmetric coroutines
asymmetric coroutines symmetric coroutines
control manipuration resume, yield conttrol

Asymmetric coroutinesはresumeで呼び出す呼び出し側と、呼び出される側という呼ぶ呼ばれるの関係がコルーチン(とメインスレッド)間にあるのが特徴となっている。

luaexample.lua
local co, co2
co = coroutine.create(function()
  coroutine.yield(print("a"))
  coroutine.resume(co2)
  coroutine.yield(print("c"))
  coroutine.resume(co2)
end)

co2 = coroutine.create(function()
  coroutine.yield(print("b"))
  coroutine.resume(co)
  coroutine.yield(print("d"))
end)

coroutine.resume(co)
print(" 1")
coroutine.resume(co)
print(" 2")
coroutine.resume(co)
print(" 3")

--[[ prints
a
 1
b
c
 2
d
 3
--]]

なるほど、完全に理解した。

3-2. λcor

Luaだとちょっと大きすぎるし扱いづらいため、変換のための小さな計算体系として\(\lambda_{\text{\textit{cor}}}\)を考える(図3.2)。

\\[ \begin{array}{rrl} x & \in & \text{\textit{Variables}}\\\\ K & \in & \{\text{\textit{Eff}}, \text{\textit{Val}}, \text{\textit{UncaughtEff}}\} \text{ // constructors} \\\\ \text{\textit{eff}} & \in & \text{\textit{Effects}}\\\\ v & ::= & x \mid \lambda x. e\\\\ e & ::= & v \mid e\ e \mid \mathtt{let}\ x = e\ \mathtt{in}\ e \mid \mathtt{inst}\ \left(\right) \\\\ & \mid& \mathtt{match}\ e\ \mathtt{with}\ \overrightarrow{case} \\\\ & \mid& \mathtt{create}\ e \mid \mathtt{resume}\ e\ e \mid \mathtt{yield}\ e \text{ // coroutine manipurations} \\\\ case & ::= & K\ x \rightarrow e \mid K\ x\ \textit{when}\ e = e \rightarrow e \\\\ letrec & ::= & \mathtt{let}\ \mathtt{rec}\ f\ x = e\ mutrec\\\\ mutrec & ::= & \mathtt{and}\ f\ x = e \mid \mathtt{in}\ e \end{array} \\] 図3.2. the syntax of \\(\lambda_{\text{\textit{cor}}}\\)

こちらも筆者が疲れたので意味論はフィーリングで行く。 すまんが[7]を参照されたし。 ランタイムにラベルストアなどを用意してがちゃがちゃやっていく感じ。

構成員としては、ラムダ計算にくわえ、let式、(相互)再帰、ADTとパターンマッチに加え、コルーチンの操作create resume yieldがある。 各エフェクトを一意にするためにinst ()もそのまま持ってきている。 小さくなるよう努力したものの、依然としてゴタゴタしているのはひとえに筆者の力不足である。

ところで上記のプログラムは書けるのだろうか?

変換のターゲットとしてコルーチンが出てくるため、上記のようなプログラムは\(\lambda_{\text{\textit{cor}}}\)では書けなくても問題はないので問題ない。

3-3. asymmetric coroutines and oneshot continuation

Asymmetric coroutinesは強力なコントロールオペレータであり、まずsymmetric coroutinesを模倣することができ、のみならずcall/1ccもasymmetric coroutinesにより実装することができる[7]。 call/1ccとは、継続の実行が高々1回に制限されているcall/ccである。

オッoneshotnessが出てきた。 これはcontinuationがコルーチンに対応し、コルーチンは状態を複製する操作が基本的に提供されてないためである。 したがってコルーチンの状態を複製する操作が追加されない限りは、コルーチンで継続をエミュレーションするときは基本的にワンショットである(表3.3)。

表3.3. the correspondence between continuations and asymmetric coroutines
continuations asymmetric coroutines
continuation object function coroutine thread
run continuation call function resume
suspend waste continuation yield

コラム: JavaScriptのgenerator

ES2015からgeneratorというものが追加された。

function* gen() {
  yield 3;
  yield 5;
  return 0;
}

const c = gen()
console.log(c.next()); // { value: 3, done: false }
console.log(c.next()); // { value: 5, done: false }
console.log(c.next()); // { value: 0, done: true }
console.log(c.next()); // { value: undefined, done: true }

おっこれはasymmetric coroutineか? と一瞬錯覚するが、実はasymmetric coroutinesよりも表現力が低い。 理由は簡単、yieldはgenerator リテラルの直下にしか書けないためである。 つまり以下のようなことがsyntacticに書けない。

const yieldf = x => yield x;

function* gen() {
  yieldf(3);
  yieldf(5);
  return 0;
}

/*
const yieldf = x => yield x;
                          ^

SyntaxError: Unexpected identifier
*/

筆者の推理としては、(おそらく)asymmetric coroutinesをCPSで表現するのは難しいが、 JSのgeneratorなら多分CPS変換できるので、babelなどによるES2015以前のJSへのコンパイルが可能になるからではないかと考えられる。

ところで、generatorも(おそらく)状態を複製する操作が用意されてないので、変換先のCPSの継続はワンショットになるはずである。

4. oneshot algebraic effects → asymmetric coroutines

Core Effから\(\lambda_{\text{\textit{cor}}}\)への変換、つまり言語Aから言語Bへの変換なのでコンパイルですね。本稿の変換の実装はすなわちコンパイラになります。 言語実装アドベントカレンダーにふさわしいですね。 本稿では変換の実装はしないので読者の課題あるいは筆者の研究の一環です。

4-1. 直感的な対応

筆者は直観で実装してしまったので、とりあえず直感的なところからかためていく。 方針としてはこんな感じになるだろうか(表4.1).

表4.1. the intuitional correspondence between (oneshot ) algebraic effects and asymmetric coroutines
(oneshot) algebraic effects asymmetric coroutines
handler (create & resume)
perform yield
continuation coroutine thread
run continuation resume

ハンドラは対応が取りづらいので曖昧になっている。 ハンドラの動作を思い出そう。 エフェクトインスタンス、value handler, effect handlerを受け取ったらthunkを取ってそのthunkをハンドラでハンドルする、という動作である。 thunk内でエフェクトを発生(yield)すると一時停止してハンドラに操作が移ってほしい、とするとthunkをコルーチンでencapsulateして即実行、という流れになる。 なのでとりあえずcreate & resumeとしてある。

4-2. 変換

追記20181209

投稿即バグが見つかり泣きました。 まずは修正前をご覧ください。

最新はこちら 追記suspend

\\[ \begin{array}{c} \left[\left[e_{ce}\right]\right]\eta = e_{\lambda \textit{cor}}\\\\ \ \\\\ \text{ // $c$ is anything to run coroutine at first, like \textit{nil}, $\left(\right)$, etc.}\\\\ \begin{aligned} \left[\left[x\right]\right]\eta &= \eta(x) \\\\ \left[\left[\textit{eff}\right]\right]\eta &= \textit{eff}\\\\ \left[\left[\lambda x. e\right]\right]\eta &= \lambda x'. \left[\left[e\right]\right]\eta\left[x\mapsto x'\right] \\\\ \left[\left[\mathtt{let}\ x = e\ \mathtt{in}\ e'\right]\right]\eta &= \mathtt{let}\ x' = \left[\left[e\right]\right]\eta\ \mathtt{in}\ \left[\left[e'\right]\right]\eta\left[x\mapsto x'\right]\\\\ \left[\left[v_1\ v_2\right]\right]\eta &= \left(\left[\left[v_1\right]\right]\eta\right) \ \left(\left[\left[v_2\right]\right]\eta\right) \\\\ \left[\left[\mathtt{inst}\ \left(\right)\right]\right]\eta &= \mathtt{inst}\ \left(\right)\\\\ \left[\left[\mathtt{perform}\ \text{\textit{eff}}\ v\right]\right]\eta &= \mathtt{yield}\ \left(\text{\textit{Eff}}\left(\left[\left[\textit{eff}\right]\right]\eta, \left[\left[v\right]\right]\eta\right)\right)\\\\ \left[\left[\mathtt{with}\ h\ \mathtt{handle}\ e\right]\right]\eta &= \left[\left[h\right]\right]\eta\ \left(\lambda c. \left[\left[e\right]\right]\eta\right)\\\\ \left[\left[\mathtt{handler}\ \textit{eff}\ (\mathtt{val}\ x\rightarrow e_v) \ \left(\left(x, k\right) \rightarrow e_{\textit{eff}}\right) \right]\right]\eta% &= \\\\ & \mathtt{let}\ \textit{eff} = \left[\left[\textit{eff}\right]\right]\eta\ \mathtt{in}\\\\ & \mathtt{let}\ \textit{vh} = \lambda x'. \left[\left[e_v\right]\right]\eta\left[x \mapsto x'\right] \ \mathtt{in}\\\\ & \mathtt{let}\ \textit{effh} = \lambda x'\ k'. \left[\left[e_{\textit{eff}}\right]\right]\eta\left[x \mapsto x', k \mapsto k'\right]\ \mathtt{in}\\\\ & \lambda \textit{th}.\\\\ & \quad \mathtt{let}\ \textit{co} = \mathtt{create}\ \textit{th}\ \mathtt{in} \\\\ & \quad \mathtt{let\ rec}\ \textit{handle}\ r =\\\\ & \qquad \mathtt{match}\ r\ \mathtt{with}\\\\ & \qquad \mid \textit{Eff}\ \left(\textit{eff'}, v\right)\ \textit{when}\ \textit{eff'} = \textit{eff} \rightarrow\\\\ & \qquad \quad \textit{effh}\ v\ (\lambda \textit{arg}.\\\\ & \qquad \quad \mathtt{let}\ \textit{ret} =\textit{continue}\ \textit{arg}\ \mathtt{in}\\\\ & \qquad \quad (\mathtt{match}\ \textit{ret}\ \mathtt{with}\\\\ & \qquad \quad \mid \textit{Val}\ \text{\textunderscore} \rightarrow \textit{ret}\\\\ & \qquad \quad \mid \text{\textunderscore} \rightarrow \textit{Val}\ \textit{ret}))\\\\ & \qquad \mid \textit{Eff}\ \left(\text{\textunderscore}, \text{\textunderscore}\right)\rightarrow \mathtt{yield}\ \left(\textit{UncaughtEff}\ \left(r, \textit{continue}\right)\right)\\\\ & \qquad \mid \textit{UncaughtEff}\ \left(\textit{Eff}\ \left(\textit{eff'}, v\right) , k\right) \ \textit{when}\ \textit{eff'} = \textit{eff} \rightarrow \\\\ & \qquad \quad \textit{effh}\ v\ (\lambda \textit{arg}.\\\\ & \qquad \qquad \mathtt{let}\ \textit{ret} = k\ \textit{arg} \ \mathtt{in}\\\\ & \qquad \qquad \textit{continue}\ (\mathtt{match}\ \textit{ret} \ \mathtt{with}\\\\ & \qquad \qquad \mid \textit{Val}\ \text{\textunderscore} \rightarrow \textit{ret}\\\\ & \qquad \qquad \mid \text{\textunderscore} \rightarrow \textit{Val}\ \textit{ret}))\\\\ & \qquad \mid \textit{UncaughtEff}\ (\textit{effv'}, k') \rightarrow\\\\ & \qquad \qquad \mathtt{yield}\ (\textit{UncaughtEff}\ (\textit{effv'}, \lambda \textit{arg}.\\\\ & \qquad \qquad \quad \mathtt{let}\ \textit{ret} = k'\ \textit{arg} \ \mathtt{in}\\\\ & \qquad \qquad \quad \textit{continue}\ (\mathtt{match}\ \textit{ret} \ \mathtt{with}\\\\ & \qquad \qquad \quad \mid \textit{Val}\ \text{\textunderscore} \rightarrow \textit{ret}\\\\ & \qquad \qquad \quad \mid \text{\textunderscore} \rightarrow \textit{Val}\ \textit{ret}))) \\\\ & \qquad \mid \text{\textunderscore} \rightarrow \textit{Val}\ \left(\textit{vh}\ r\right)\\\\ & \quad \mathtt{and}\ \textit{continue}\ \textit{arg} =\\\\ & \qquad \text{ // 追記20181209 resumeにcoを渡し忘れてたのを修正 } \\\\ & \qquad \mathtt{let}\ r = \mathtt{resume}\ \textit{co}\ \textit{arg}\ \mathtt{in}\\\\ & \qquad \mathtt{match}\ r\ \mathtt{with}\\\\ & \qquad \mid \textit{Val}\ v \rightarrow v\\\\ & \qquad \mid \text{\textunderscore} \rightarrow \textit{handle}\ r\\\\ & \quad \mathtt{in}\\\\ & \quad \mathtt{match}\ \textit{continue}\ c\ \mathtt{with} \\\\ & \quad \mid \textit{Val}\ v \rightarrow v\\\\ & \quad \mid r \rightarrow r\\\\ \end{aligned} \end{array} \\] 図4.2. the conversion \\(\left[\left[e_{ce}\right]\right] = e_{\lambda_{\textit{cor}}}\\)

handler長すぎんじゃボケー!!! ただの実装やろがい!!! 散々引っ張っておいて大変申し訳無いが、今の所スッキリできそうにないので勘弁してもらいたい。 さらに見返してみるとなんだか洗練されてない。 もう少しCPSっぽく書ける部分がたしかにあり、そうすれば末尾呼び出しになって良いことがありそうだが、筆者はCPSで実装を試みたところバグバグになって一回諦めているため、読者への課題としたい。 CPSにすればvalue handlerを複数使ってしまうのを防ぐためのValコンストラクタが不要になるだろう。

メタの話はこの程度にして、内容を見てみよう。 handler以外はだいたいふ〜んて感じで、performも表4.1でぼんやりと考えたとおりにyieldに対応している。

問題は爆発しているhandlerである。 thunkを受け取ってコルーチンを作り、resumeのラッパーとなっているcontinueを走らせてるので、なるほどcreate & resumeである。

handlerの内部のhandleが一番仕事してる雰囲気を出している。 handleはcontiueからのみ呼ばれており、呼び出し時にresumeの戻り値、つまりyieldに渡された引数かコルーチンでencapsulateされた関数の戻り値である。 Val以外でコルーチンから戻ってくるものとなると、yieldはperformだからEffだな。

そしてEff(eff', v)のeff'がハンドルすべきエフェクトeffの場合はeffhによって処理をおこなっている。 effhに渡される第2引数は限定継続であるが、ここではcontinueをさらにラップしてValタグを剥がしている。 ハンドルしないエフェクトの場合はUncaughtEffにエフェクトと継続を渡してyieldしている。 これによって一つ外側のハンドラにエフェクトを飛ばしているのである。 だからさっき述べたcontinue内のresumeが返すのは関数の戻り値とEffだけでなくUncaughtEffもある。

ではhandle内でUncaughtEffをハンドルしてる部分を見る。 だいたい同じ要領だが、effhに渡している継続は様子がちょっとちがう。 UncaughtEffは継続を一緒にもってくるので、まずこれを走らせる。 そして継続の戻り値をさらに現在の継続に渡して現在の継続を走らせる。 ハンドルできないUncaughtEffの場合も面白い。 さらに外側のハンドラにエフェクトの処理をまかせたいので同様にUncaughtEffをyieldで飛ばしている。 ただしUncaughtEffに渡している継続は、渡ってきた継続の結果をさらに現在の継続に渡している。 つまりこれは継続をネストさせている。 ますますCPSで実装したくなりますね。 実装に自信ニキはよろしくお願いします。 脳が発光しますね。

最後にValが来た場合、中身を剥がしてvalue handlerに突っ込んでいる。 型がない世界でよかったですね。

追記20181209 resume

多分これが一番正しいと思います。

\\[ \begin{array}{c} \left[\left[e_{ce}\right]\right]\eta = e_{\lambda \textit{cor}}\\\\ \ \\\\ \begin{aligned} &\left[\left[\mathtt{handler}\ \textit{eff}\ (\mathtt{val}\ x\rightarrow e_v) \ \left(\left(x, k\right) \rightarrow e_{\textit{eff}}\right) \right]\right]\eta% = \\\\ &\qquad \mathtt{let}\ \textit{eff} = \left[\left[\textit{eff}\right]\right]\eta\ \mathtt{in}\\\\ &\qquad \mathtt{let}\ \textit{vh} = \lambda x'. \left[\left[e_v\right]\right]\eta\left[x \mapsto x'\right] \ \mathtt{in}\\\\ &\qquad \mathtt{let}\ \textit{effh} = \lambda x'\ k'. \left[\left[e_{\textit{eff}}\right]\right]\eta\left[x \mapsto x', k \mapsto k'\right]\ \mathtt{in}\\\\ &\qquad \lambda \textit{th}.\\\\ &\qquad \quad \mathtt{let}\ \textit{co} = \mathtt{create}\ \textit{th}\ \mathtt{in} \\\\ &\qquad \quad \mathtt{let\ rec}\ \textit{handle}\ r =\\\\ &\qquad \qquad \mathtt{match}\ r\ \mathtt{with}\\\\ &\qquad \qquad \mid \textit{Eff}\ \left(\textit{eff'}, v\right)\ \textit{when}\ \textit{eff'} = \textit{eff} \rightarrow \textit{effh}\ v\ \textit{continue}\\\\ &\qquad \qquad \mid \textit{Eff}\ \left(\text{\textunderscore}, \text{\textunderscore}\right)\rightarrow \mathtt{yield}\ \left(\textit{UncaughtEff}\ \left(r, \textit{continue}\right)\right)\\\\ &\qquad \qquad \mid \textit{UncaughtEff}\ \left(\textit{Eff}\ \left(\textit{eff'}, v\right) , k\right) \ \textit{when}\ \textit{eff'} = \textit{eff} \rightarrow \\\\ &\qquad \qquad \quad \textit{effh}\ v\ \left(\lambda \textit{arg}. \textit{handle}\ \left(\mathtt{resume}\ \left(\mathtt{create}\ k\right)\ \mathtt{arg}\right)\right)\\\\ &\qquad \qquad \mid \textit{UncaughtEff}\ \left(\textit{effv'}, k\right) \rightarrow\\\\ &\qquad \qquad \qquad \mathtt{yield}\ \left(\textit{UncaughtEff}\ \left(\textit{effv'}, \lambda \textit{arg}. \textit{handle}\ \left(\mathtt{resume}\ \left(\mathtt{create}\ k\right)\ \mathtt{arg}\right)\right)\right)\\\\ &\qquad \qquad \mid \text{\textunderscore\ /* ANY value */} \rightarrow \textit{vh}\ r\\\\ &\qquad \quad \mathtt{and}\ \textit{continue}\ \textit{arg} = \textit{handle}\ \left(\mathtt{resume}\ \textit{co}\ \textit{arg}\right)\\\\ &\qquad \quad \mathtt{in}\\\\ &\qquad \quad \textit{continue}\ c \end{aligned} \end{array} \\] 図4.3. the revision of the conversion

handlerだけの変更だが、だいぶダイエットに成功した。 Valタグはそもそも不要だったことがわかった。 UncaughtEffをハンドルしてる部分も様子が変わっている。 UncaughtEffが持ってきた継続をコルーチンでencapsulateして即走らせ、その値をhandleに渡す、という関数をeffhに継続として渡している。 continueを見るとだいたい同じことをやっており、encapsulateしない場合コルーチンを突き抜けてyieldしてしまうパターンがあった。 また現在の継続はhandleが内部でcontinueを呼んでくれるため、わざわざcontinueを引っ張る必要はなく、走らせる継続の戻り値はhandleでハンドルするという元からの考えを使えばいいだけだった。 操作を継続の中に押し込んでいく感じが、なんとなくFunctor Freeを思わせる。

追記おわり

追記20181216

さらに大学のゼミ発表などを経てコンパクトになりました。

\\[ \begin{aligned} &\left[\left[\mathrm{handler}\ \textit{eff}\ \left(\mathtt{val}\ x \rightarrow e_v\right)\ \left(\left(x, k\right) \rightarrow e_\textit{eff}\right)\right]\right]\eta = \\\\ & \qquad \mathtt{let}\ \textit{eff} = \left[\left[\textit{eff}\right]\right]\eta\ \mathtt{in}\\\\ & \qquad \mathtt{let}\ \textit{vh} = \lambda x'. \left[\left[e_v\right]\right]\eta \left[x \mapsto x'\right]\ \mathtt{in}\\\\ & \qquad \mathtt{let}\ \textit{effh} = \lambda x'\, k'. \left[\left[e_\textit{eff}\right]\right]\eta \left[x\mapsto x', k \mapsto k'\right] \mathtt{in}\\\\ & \qquad \lambda \textit{th}.\\\\ & \qquad \quad \mathtt{let}\ \textit{co} = \mathtt{create}\ \textit{th}\ \mathtt{in}\\\\ & \qquad \quad \mathtt{let}\ \mathtt{rec}\ \textit{handle}\ r =\\\\ & \qquad \qquad \mathtt{match}\ r\ \mathtt{with}\\\\ & \qquad \qquad \mid \textit{Eff}\left(\textit{eff'}, v\right)\ \mathtt{when}\ \textit{eff'} = \textit{eff} \rightarrow \textit{effh}\ v\ \left(\textit{continue}\ \textit{co}\right)\\\\ & \qquad \qquad \mid \textit{Eff}\left(\text{\textunderscore}, \text{\textunderscore}\right) \rightarrow \mathtt{yield}\ \left(\textit{UncaughtEff}\left(r, \left(\textit{continue}\ \textit{co}\right)\right)\right)\\\\ & \qquad \qquad \mid \textit{UncaughtEff}\left(\textit{Eff}\left(\textit{eff'}, v\right), k\right)\ \mathtt{when}\ \textit{eff'} = \textit{eff} \rightarrow \textit{effh}\ v\ \left(\textit{continue}\ \left(\mathtt{create}\ k\right)\right)\\\\ & \qquad \qquad \mid \textit{UncaughtEff}(\textit{effv}, k) \rightarrow \mathtt{yield}\ (\textit{UncaughtEff}\left(\textit{effv}, \left(\textit{continue}\ \left(\mathtt{create}\ k\right)\right)\right))\\\\ & \qquad \qquad \mid \text{\textunderscore} \rightarrow \textit{vh}\ r\\\\ & \qquad \quad \mathtt{and}\ \textit{conrtinue}\ \textit{co}\ \textit{arg} = \textit{handle}\ \left(\mathtt{resume}\ \textit{co}\ \textit{arg}\right)\\\\ & \qquad \quad \mathtt{in}\ \textit{continue}\ \textit{co}\ \textit{c} \end{aligned} \\] 図4.4. the conversion v3.

4.3とは本質的に何も変わってません。 continueを汎用的なものにした。 これにより、処理がどうなってるかがより簡潔になったんじゃないでしょうか。 handleを連れ回すことで現在のハンドラによるハンドル処理を続けることができる。 UncaughtEffに渡す継続をコルーチンでencapsulateするのは、エフェクトの発生(yield)を再びキャッチするためである。

追記20190127

バグってました。

$$ \begin{aligned} &\left[\left[\mathrm{handler}\ \textit{eff}\ \left(\mathtt{val}\ x \rightarrow e_v\right)\ \left(\left(x, k\right) \rightarrow e_\textit{eff}\right)\right]\right]\eta = \\\\ & \qquad \mathtt{let}\ \textit{eff} = \left[\left[\textit{eff}\right]\right]\eta\ \mathtt{in}\\\\ & \qquad \mathtt{let}\ \textit{vh} = \lambda x'. \left[\left[e_v\right]\right]\eta \left[x \mapsto x'\right]\ \mathtt{in}\\\\ & \qquad \mathtt{let}\ \textit{effh} = \lambda x'\, k'. \left[\left[e_\textit{eff}\right]\right]\eta \left[x\mapsto x', k \mapsto k'\right] \mathtt{in}\\\\ & \qquad \lambda \textit{th}.\\\\ & \qquad \quad \mathtt{let}\ \textit{co} = \mathtt{create}\ \textit{th}\ \mathtt{in}\\\\ & \qquad \quad \mathtt{let}\ \mathtt{rec}\ \textit{handle}\ r =\\\\ & \qquad \qquad \mathtt{match}\ r\ \mathtt{with}\\\\ & \qquad \qquad \mid \textit{Eff}\left(\textit{eff'}, v\right)\ \mathtt{when}\ \textit{eff'} = \textit{eff} \rightarrow \textit{effh}\ v\ \left(\textit{continue}\ \textit{co}\right)\\\\ & \qquad \qquad \mid \textit{Eff}\left(\text{\textunderscore}, \text{\textunderscore}\right) \rightarrow \mathtt{yield}\ \left(\textit{UncaughtEff}\left(r, \left(\textit{continue}\ \textit{co}\right)\right)\right)\\\\ & \qquad \qquad \mid \textit{UncaughtEff}\left(\textit{Eff}\left(\textit{eff'}, v\right), k\right)\ \mathtt{when}\ \textit{eff'} = \textit{eff} \rightarrow \textit{effh}\ v\ \left(\textit{rehandle}\ k \right)\\\\ & \qquad \qquad \mid \textit{UncaughtEff}(\textit{effv}, k) \rightarrow \mathtt{yield}\ \left(\textit{UncaughtEff}\left(\textit{effv}, \textit{rehandle}\ k \right)\right)\\\\ & \qquad \qquad \mid \text{\textunderscore} \rightarrow \textit{vh}\ r\\\\ & \qquad \quad \mathtt{and}\ \textit{conrtinue}\ \textit{co}\ \textit{arg} = \textit{handle}\ \left(\mathtt{resume}\ \textit{co}\ \textit{arg}\right)\\\\ & \qquad \quad \mathtt{and}\ \textit{rehhandle}\ \textit{k}\ \textit{arg} = \textit{handler}\ \textit{eff}\ \left(\textit{continue}\ \textit{co}\right)\ \textit{effh}\ \left(\lambda c. k\ \textit{arg}\right) \\\\ & \qquad \quad \mathtt{in}\ \textit{continue}\ \textit{co}\ \textit{c} \end{aligned} $$ 図4.5. the conversion v4.

$\textit{Eff}$のハンドルはv2やv3と変わりない。 $\textit{rehandle}$という関数が追加され、$\textit{UncaughtEff}$に渡す、あるいは使う継続を$\textit{reandle}$に渡している。 では$\textit{rehandle}$は何をしてるんですか? 新しくハンドラを作り、2つの引数を実行するサンクを作ってハンドラに渡すことで、サンクの中身をハンドルして実行する。

我々の実現したいdeep handlerを考えれば確かにこのような実装になる。 deep handlerとは、ハンドラの取り出した継続も同じハンドラによってハンドルされる。 逆となる概念はshallow handlerであり、取り出された継続は同ハンドラからのハンドルを逃れる。

ハンドルされる$\textit{UncaughtEff}$を見てみる。

$\mid \textit{UncaughtEff}\left(\textit{Eff}\left(\textit{eff'}, v\right), k\right)\ \mathtt{when}\ \textit{eff'} = \textit{eff} \rightarrow \textit{effh}\ v\ \left(\textit{rehandle}\ k \right)$

この矢印の右辺を展開すると、

$$ \begin{array}{l} \textit{effh}\ v \left(\lambda \textit{arg}.\right.\\\\ \quad \textit{handler}\ \textit{eff}\ \left(\textit{continue}\ \textit{co}\right)\ \textit{effh}\ \left( \lambda c. k\ \textit{arg} \right)\left.\right) \end{array} $$

特にポイントとなるのが、新しく作るハンドラのvalue handlerが、現在のハンドラが持ってるencapsulateしたサンクを$\textit{continue}$する、いわばハンドラが持ってる継続にハンドルの結果を渡しているCPSのような構造になる。 ハンドラによって$\textit{UncaughtEff}$が持ってきた$k$をハンドラによってハンドルすることで、晴れて現在のハンドラでもeffectをハンドルできるようになる。

これまでの変換では、渡ってきた継続のeffectをハンドルできてるようでできてなかった。 今回の変換により、なんとか解決したんじゃないでしょうか。 実装も更新しているので、よかったら使ってみてバグを発見してください。

5. 実装

それでは改めてリポジトリの方を見てみよう。 Asymmetric coroutinesと非常に縁の深いLuaにより実装した。 本稿で変換を改めて考えるにあたり、バグが複数発見、修正された。 フィーリングの脆さと簡単なモデルに落として内容をしっかり検討することの重要さを再確認した。

実装は図4.2とほとんど同じである。 なんといっても順番が逆で、実装が先にあり、図4.2は実装をもとに書き下したためである。 しかしLuaはclassもADTもないし関数リテラルが冗長、文志向なのでreturn必須といろいろしんどいところがあった。

本稿の変換と異なる点は、ハンドラが多値に対応している点である。 …というのは半分ウソというか、Multicore OCamlではtupleで表現するところを、tableでガッとやるのではなく可変長引数や多値などといったLuaの持ち味を活かすための細工をおこなった。 多値を引き回すのは面倒なので、ハンドラに渡ってきた多値をtableに押し込み、実際に使われるタイミングでunpackによって多値に戻している。 この操作のため、effect handlerの引数の順序が(value, continuation)から(continuation, value...)と逆になっている。 多値についてはこちらを参照…とおもったけど多値を返す関数の呼び出しをそのまま関数の引数の位置に書いた場合についてはあまりふれられてませんね。 Lua VM的な説明をすると、引数の末尾位置に多値を返す関数の呼び出しを書かないと、1引数分、つまり1レジスタしか関数の戻り値を受けるレジスタが用意されないためである。

最初期からフィーリングで突っ走っており、UncaughtEff相当のことを、赤ちゃんでも思いつくような、例外処理機によって実装していた。 OCamlのように代数的な例外がないのも相まって散々な目にあったが、部分的にはalgebraic effectsを実装していた。 例外のハンドリングは一般にコストフル8であり、Luaもご多分に漏れず遅い。 コントロールを全てコルーチンの操作だけでおこなった場合と例外でぴょんぴょんする場合のパフォーマンスを比較してみたいが、まぁ半分ナンセンスだし半分は筆者のやる気不足なので、多分速くなってるだろうということで終わる。

5-1. デモ

皆さん大好きmultiprompt shift/resetが実装できる。 ただしエフェクトハンドラの継続をそのままつかっているので、継続の使用は高々1回に制限されている。

local eff = require("eff")
local Eff, perform, handler = eff.Eff, eff.perform, eff.handler

local sr0
do
  local new_prompt = function()
    local Shift0 = Eff("Shift0")

    return {
      take = function(f) return perform(Shift0(f)) end,
      push = handler(Shift0,
        function(v) return v end,
        function(k, f)
          return f(k)
        end)
    }
  end

  local reset_at = function(p, th)
    return p.push(th)
  end

  local shift0_at = function(p, f)
    return p.take(function(k) return f(k) end)
  end

  sr0 = {
    new_prompt = new_prompt,
    reset_at = reset_at,
    shift0_at = shift0_at
  }
end

プロンプトごとにShift0エフェクトインスタンスを作っている。 handlerがそのまんまdelimiterになってるのがいいよね。

local p = sr0.new_prompt()

sr0.reset_at(p, function()
  print(sr0.shift0_at(p, function(k)
     k("Hello")
     print("?")
  end))

  io.write("World")
end)

--[[ prints
Hello
World?
--]]

だいぶ自然に書けているんじゃないでしょうか。

エフェクトの抽象化、実装の分離…型クラスか?

local Map = Eff("Map")

local map = function(f, fa)
  return perform(Map(f, fa))
end

-- list map
local lmaph = handler(Map,
  function(v) return v end,
  function(k, f, fa)
    local newt = {}

    for i, x in ipairs(fa) do
      newt[i] = f(x)
    end

    return k(newt)
  end)

lmaph(function()
  local t = map(function(x) return x * x end, {1, 2, 3, 4, 5})

  for i = 1, #t do
    print(t[i])
  end
end)

-- string map
local smaph = handler(Map,
  function(v) return v end,
  function(k, f, s)
    local news = ""

    for c in s:gmatch(".") do
      news = news .. f(c)
    end

    return k(news)
  end)

smaph(function()
  print(map(function(c) return c .. c end, "hello"))
end)

Functorっぽいものを書いてるなと思ったがsmaphをみると全然そんなことなく、自分でも困惑した。 Luaは残念ながら型のない世界なのでなんでもアリである。

6. 関連研究

Koka言語などをやっていってるDaan氏によりC言語によるalgebraic effectsの実装[9]がおこなわれている。 本稿と比較すると1ハンドラ1エフェクトや継続がワンショットなどの制限ががない一方、非常にユーザーアンフレンドリーな構文となっている。 そのためP言語などのコンパイラのターゲットという位置づけがなされている。 本稿では式指向の言語での変換をおこなっており、\(\lambda_{\textit{cor}}\)相当をサブセットとして持つ言語ならばsyntacticな辛さはない、と思う。

7. おわりに

本稿ではoneshot algebraic effectsからasymmetric coroutinesへの変換を提示した。 この変換を用いることで、asymmetric coroutinesを持つ言語でoneshot algebraic effectsを使用することが可能になる。 本稿ではすでにLuaによる実装を与えており、Luaはalgebraic effects-readyな状態となっている。

ただし本稿の変換の正しさについては証明されていない。 いまのところ "なんとなくうごいてる" 状態であり、とりあえずテストにMulticore OCamlのチュートリアルを実装することで正しく動いてそうなことを確認している。 未来のボクや、読者のみなさんに託されています。 2019年には本稿の変換の証明、あるいは間違った部分の指摘などが湧き出ることを願っている。


  1. Kiselyov, Oleg, and Kc Sivaramakrishnan. "Eff directly in OCaml.(2016)." ACM SIGPLAN Workshop on ML. 2016. ↩

  2. Bauer, Andrej, and Matija Pretnar. "Programming with algebraic effects and handlers." Journal of Logical and Algebraic Methods in Programming 84.1 (2015): 108-123. ↩

  3. むしろ他に継続がワンショットのalgebraic effectsを知りませんが…。あとMulticore OCamlにはObj.clone_continuationという継続を複製する関数が用意されており、ランタイムにコストを支払うことで継続を2回以上使うことができる。 ↩

  4. Dolan, Stephen, et al. "Concurrent system programming with effect handlers." International Symposium on Trends in Functional Programming. Springer, Cham, 2017. ↩

  5. Bruggeman, Carl, Oscar Waddell, and R. Kent Dybvig. "Representing control in the presence of one-shot continuations." ACM SIGPLAN Notices. Vol. 31. No. 5. ACM, 1996. ↩

  6. Dolan, Stephen, et al. "Effective concurrency through algebraic effects." OCaml Workshop. 2015. ↩

  7. Moura, Ana Lúcia De, and Roberto Ierusalimschy. "Revisiting coroutines." ACM Transactions on Programming Languages and Systems (TOPLAS) 31.2 (2009): 6. ↩

  8. 例外処理のある言語は概ねモダンであり、モダンな言語は比較的親切であり、親切な言語はエラーを吐くとスタックトレースを出してくれる。 この新設のためにスタックトレースを記録するので遅くなる。gotoとしての例外おおいに結構しかしパフォーマンスとしっかり勘案すること。 ↩

  9. Leijen, Daan. "Implementing Algebraic Effects in C." Asian Symposium on Programming Languages and Systems. Springer, Cham, 2017. ↩