代数的エフェクトとハンドラのための

CPS インタプリタと型システム
藤井 舞花, 浅井 健一
お茶の水女子大学
fujii.maika@is.ocha.ac.jp, asai@is.ocha.ac.jp
概 要
例外処理を一般化し継続を明示的に扱える代数的エフェクトとハンドラは様々な言語に導入されている。他にも、代数的エフェクトとハンドラと継続の扱い方が近しいとされる 4 種類の限定継続演算子が存在するが、両者はこれまで全く別の定式化で議論されてきた。これらを統一的に議論するための土台として、代数的エフェクトとハン
ドラを 4 種類の限定継続演算子と同じ枠組みで CPS インタプリタを再定義し、両者を繋ぐ足掛かりを作る。さらに、4 種類の限定継続演算子ではインタプリタから機械的に抽象機械や型システムが導けており、それらとインタプリタとの間に規則的な繋がりがある。本稿でも新たに定義した代数的エフェクトとハンドラの CPS インタプリタから、別途証明を与えずとも正当性が保証された、型システムや抽象機械を導出する。

はじめに

1

継続とは、プログラムの実行中のある時点における残りの計算のことである。例えば 1 + 2 * 3という計算があり「2 と 3 をかける」の時点での残りの計算は「その結果に 1 を足す」である。この「1 を足す」のような残りの計算を継続と呼ぶ。
本稿ではこの継続を明示的に扱える言語機構である代数的エフェクトとハンドラ [1, 20] を取り上げる。代数的エフェクトとハンドラは例外処理を一般化したものとなっている。従来の例外処理は副作用を発生するとハンドラに事後処理を任せ、オペレーションが発生した時点での継続は捨てられる。一方で代数的エフェクトとハンドラはオペレーションが発生した時点における限定された範囲
までの継続 (限定継続) も用いて処理を行うことができる。つまりユーザー自身が自由に定義できる
大域ジャンプが可能となる。代数的エフェクトとハンドラのハンドラには深いもの (deep handler)と浅いもの (shallow handler) [16] が存在する。この 2 種類のハンドラは限定継続の扱い方に違いがあるため、同じプログラムでも異なる場所に移動することが可能となる。
他にも継続を扱う演算子として shift/reset [6, 7]、control/prompt [10]、shift0/reset0 [18]、control0/prompt0 [13] の 4 種類の限定継続演算子なども存在する。この 4 つの限定継続演算子の中で
shift0/reset0 は deep handler と、control0/prompt0 は shallow handler と限定継続の扱い方に関してとても近い関係性がある [11, 19]。しかし代数的エフェクトとハンドラと 4 種類の限定継続演
算子は全く異なる定式化でそれぞれが議論されてきた。これまでの研究では、4 種類の限定継続演
算子は、trail [2] とメタ継続 [6] があれば各種の演算子のインタプリタが表現できている [23]。そのため本稿では代数的エフェクトとハンドラのためのインタプリタも、trail やメタ継続を用いて再定義することで、両者を同じ枠組みで統合するための第一歩としていく。また trail をリストではなく高階関数を用いて実装することによって、高階関数の形で shallow handler のインタプリタを定義することを可能にした。高階関数の形で定義できたことによって、trail の型が変化するようなプログラムの例でも型をつけることができるようになる。今回は 4 種類の限定継続演算子1 に合わ
1

マルチプロンプトや [8, 9] 多段の CPS 階層 [15] を扱わない基本的なものの場合1

せたため、例外に名前を付けることができないという制約を設けているが、条件文さえ追加すればdeep handler については名前付きオペレーションが模倣可能となる。
4 種類の限定継続演算子は正当性が保証された非関数化などの変換を施せば、インタプリタから抽象機械や仮想機械 [12] が導出できている。正当性が保証された変換を使うことで、別途証明を与えることなく抽象機械や仮想機械が正しいことが保証されている。さらに型システム [24] もインタ
プリタから機械的に導けており、停止性や健全性が示された。それをもとにして 代数的エフェクトとハンドラも 4 種類の限定継続演算子と同じ枠組みでインタプリタで定義することで、同様にしてインタプリタから機械的に仮想機械や型システムを導出し別途証明を与えずとも正当性が保証された代数的エフェクトとハンドラの直接実装への先駆けとしていく。
本稿の貢献は以下のようにまとめられる。

• 代数的エフェクトとハンドラのための新たな CPS インタプリタを定義する。これを 4 種類の限定継続演算子の実装に必要となる trail とメタ継続の概念のみで実現する。そのため代数的エフェクトとハンドラと 4 種類の限定継続演算子を統一的に議論できる土台を提供する。
• CPS インタプリタから代数的エフェクトとハンドラのための型システムを導出する。この型システムに基づく言語と、それに対する CPS インタプリタを定理証明系言語 Agda で実装
し、停止性や健全性も示している。
• CPS インタプリタから半機械的に導出した抽象機械を示す。
Agda で実装したコードは http://pllab.is.ocha.ac.jp/~asai/jpapers/ppl/ppl22.agda で入手可能である。
論文の構成
次節で代数的エフェクトとハンドラについて紹介をした後、3 節でインタプリタを紹介する。4 節
では新たに定義したインタプリタとこれまでに提唱されたインタプリタを比較する。そして本研究のインタプリタから導出できた抽象機械を 5 節で、型システムを 6 節で示す。最後に 7 節で関連研究について議論し、8 節で結論を述べる。

2

代数的エフェクトとハンドラ

代数的エフェクトとハンドラは副作用を起こす演算子とそれを処理する演算子からなる。通常の例外処理とは異なり、オペレーションを起こした時点におけるハンドラで限定された継続を副作用時に扱うことができる。本稿では try ... with をハンドラとし、call とすることでオペレーション
呼び出しをする。具体的に try e1 with (x; k) -> e2 と記述した式は、もし e1 で call(a) とオペレーション呼び出しが行われると、a が x に、オペレーション呼び出しをした地点から try とwith で囲まれた部分までの継続が k に代入され、e2 を実行する。
代数的エフェクトとハンドラには deep と shallow の 2 種類のハンドラが存在するが、両者の違いが出る例として以下の式について考える。なお、本稿では計算の評価を値呼び、かつ左から行う
ものとする。

1 + try (try 10 + call(3) * call(4)with (x; k) -> k x - 2)
- 5with (y; g) -> y * 2
この式では、外側のハンドラの中でオペレーション呼び出しが起きると、これまでの継続 (g) を捨て引数を 2 倍する作用が、内側のハンドラの中でオペレーション呼び出しが起きると、これまでの2

継続 (k) を呼び出してから 2 を引く作用が施される。この内側のハンドラのようにオペレーションの処理に k を用いることで残りの継続を扱うことができている。この式を用いた 2 種類のハンドラの詳細については 2.1 節 (deep) と 2.2 節 (shallow) で述べる。

2.1

deep handler

はじめに上記の式のハンドラが deep なハンドラであった場合を説明する。まず内側のハンドラ内にある call(3) でオペレーションが呼び出され、x には 3 が、k には内側のハンドラで限定された継続 try 10 + [.] * call(4) with (x; k) -> k x - 2 が代入される。deep なハンドラで捕捉されたため限定継続に同じハンドラが入る。そして計算が内側のハンドラの制御部分 k x 2 へ移り、以下のように計算が進む。

1 + try ((try 10 + 3 * call(4) with (x; k) -> k x - 2)
- 2)
- 5
with (y; g) -> y * 2
次にまた内側のハンドラ内にある call(4) でオペレーション呼び出しが行われる。同様にして、xには 4 が、k には deep なハンドラで限定された継続 try 10 + 3 * [.] with (x; k) -> k x 2 が代入される。計算も下記の式へと評価される。

1 + try (((try 10 + 3 * 4 with (x; k) -> k x - 2)
- 2)
- 2)
- 5
with (y; g) -> y * 2
すると内側のハンドラ内の計算 10 + 3 * 4 ではオペレーションが呼び出されずに正常終了するた
めハンドラ外の計算へと進み、外側にあったハンドラ内でもオペレーションが呼び出されることな
く正常終了し、結果として 14 と評価される。

2.2

shallow handler

次にハンドラが shallow なハンドラであった場合について考える。deep な場合と同様にして内側のハンドラ内にある call(3) でオペレーション呼び出しが行われる。x に 3 が、k には内側のハンドラで限定された継続が代入されるが、shallow なハンドラで限定された継続はハンドラ自分
自身は囲まれないため 10 + [.] * call(4) となる。そして計算は下記のようになる。

1 + try ((10 + 3 * call(4))- 2)- 5with (y; g) -> y * 2
ここで限定継続 k が呼び出されたときの継続 ([.] - 2) - 5 に注目する。この継続は「呼び出し文脈 (invocation context)」と呼ばれている。次に call(4) が呼び出されているが、deep の場合とは違って外側にあったハンドラ内で起こっている。そのため y に 4 が、g にハンドラで限定された継続 ((10 + 3 * [.]) - 2) - 5 が代入される。このように deep なハンドラとは違い shallow
なハンドラは k の呼び出し文脈であった ([.] - 2) - 5 まで限定継続として g に代入する。そしてハンドラの制御部分 y * 2 へ移り、以下のように計算が評価される。

3

1 + 4 * 2
よって計算結果は 9 と評価される。
ハンドラの中で一度しかオペレーションが呼ばれないなら deep と shallow なハンドラで計算結果に違いは現れないが、このように同じハンドラの中で 2 度以上オペレーションが呼び出されていると違いが現れる。

2.3

オペレーションに名前を付ける

本稿では 4 種類の限定継続演算子に合わせたため、上記で紹介した代数的エフェクトとハンドラ
はオペレーションが呼び出されたら直近のハンドラで処理を担う構文となっているが、より一般的にはオペレーションに名前を与え複数のハンドラが存在する際にどこのハンドラにあるオペレーションを用いるか自由に定義できるようにする。例えば以下の式を考える。

1 + try (try 10 + call2(4) with {call1(x; k) -> k x - 2})- 5with {call2(y; g) -> g y + 2;
call3(y; g) -> y * 2}
どのオペレーションをハンドルするかを示すために with 以下では引数と限定継続の変数だけでなくオペレーション名も指定する。外側のハンドラのように 2 つ以上のオペレーションを定義することも可能である。この式の計算は、まず内側のハンドラの中でオペレーション call2 が呼び出されているが、内側のハンドラには call2 は定義されていない。しかし外側のハンドラを見てみると
call2 の作用が定義されているため、外側のハンドラの処理に飛ぶことができる。このとき y に 4が、g には外側のハンドラ内の限定継続が代入される。つまり deep handler の場合は

g = try (try 10 + [.] with {call1(x; k) -> k x - 2})- 5with {call2(y; g) -> g y + 2;
call3(y; g) -> y * 2}となり、 shallow handler の場合は

g = (try 10 + [.] with {call1(x; k) -> k x - 2})- 5と限定継続が切り取られる。どちらの場合も内側のハンドラは外側のハンドラ内の限定継続の一部として残っている。そして式は以下のように計算が進み、限定継続を呼び出し 2 を足す作用を施すことができる。

1 + (g y + 2)
このようにオペレーションに名前を与えると直近ではないそれよりも外側のハンドラにあるオペレー
ションを呼び出すことも可能にする。
本稿ではハンドラが限定継続を切り取る際の挙動における基本的な体系を示したいため名前付きオペレーションに対応しない仕様としたが、deep handler であればオペレーションに名前を与える代わりに条件文を使って模倣できることを紹介する。手法として、ハンドラの処理を if x = athen ... else k call(x) と記述する。ここで x はオペレーション呼び出しの引数が、k には限定継続が代入されており、a は任意の値となる。x = a が真であればオペレーションの名前が一致したこととし、このハンドラで行いたい処理を記述する。目的のハンドラでなければ (オペレーショ

4ンの名前が一致しなければ) else 部分を行う。else 部分では限定継続 k の引数として call(x) を渡すことで、これまでの限定継続を保持したまま一つ外側のハンドラに飛ぶようになっている。先程例に出した式の場合は以下のように模倣する。

1 + try (try 10 + call(4) with (x; k) -> if x = a1 then k x - 2 else k call(x))- 5with (y; g) -> if y = 4 then g y + 2
else if y = a2 then y * 2else g call(y)ここで a1 と a2 は 4 ではない任意の値とする。計算の進め方として、まず内側のハンドラでオペ
レーションが呼び出されているため

x = 4
k = try 10 + [.] with (x; k) -> if x = a1 then k x - 2 else k call(x)としてハンドラの処理に移り、式は以下のように進む。

1 + try (if x = a1 then k x - 2 else k call(x))- 5with (y; g) -> if y = 4 then g y + 2
else if y = a2 then y * 2 else g call(y)条件分岐において x = a1 は偽であるため else 部分を評価する。するとまた call(x) が起こり外側にあったハンドラの処理に移る。このとき

y = x = 4g = try (k [.]) - 5 with (y; g) -> if y = 4 then g y + 2
else if y = a2 then y * 2 else g call(y)となり、式は以下のようになる。

1 + (if y = 4 then g y + 2 else if y = a2 then y * 2 else g call(y))
よって y = 4 であるためその then 部分の計算 g y + 2 を行うことができる。そして呼び出された限定継続 g は、中の k も呼び出せば

g = try (try 10 + [.] with (x; k) -> if x = a1 then k x - 2 else k call(x))- 5with (y; g) -> if y = 4 then g y + 2
else if y = a2 then y * 2 else g call(y)となり、名前付きオペレーションに対応した場合の限定継続と本質的に同じになっている。
shallow handler の場合でも条件文を用いて名前付きオペレーションを模倣することを試みたが、shallow handler は限定継続を元々囲んでいたハンドラがなくなるという性質があるため、k call(a)としても残るべきハンドラが消えてしまい上記の方法では上手くいかない。

5

項

e

::=

x | λx. e | e1 @ e2 | try e1 with (x; k). e2 | call (e)

値
継続
trail
ハンドラ
メタ継続

v
c
t
h
m

=
=
=
=
=

(v → c → t → m → v)
v→t→m→v• + (v → t → m → v)
(v → v → c → t → m → v)
(c × t × h) list

初期継続

初期 trail

id c v id t []id c v id t ((c, t, h) :: m)id c v c m
id t

=
=
=
=

v
cvtm
c v id t m
Bullet(::) : c → t
c :: id t
c :: c′→==t
cλv. λt′ . c v (c′ :: t′ )(@) : t → t
id t @ t
c@t

→
=
=

t
t
c :: t

図 1. 構文、インタプリタで使用する型や初期継続、初期 trail、trail の合成のための関数

3

代数的エフェクトとハンドラの CPS インタプリタ

先述の通り本稿のインタプリタは 4 種類の限定継続演算子のインタプリタ [23, 12] を参考にしており、評価関数の引数に trail やメタ継続というデータも渡す形式として CPS インタプリタを定義している。trail は呼び出し文脈の追跡 [2] をするために、メタ継続 [6] はハンドラの内側と外側の継続 (計算) を区切るために使用する。trail は control や control0 で用いられていた概念であり、今回は shallow handler のインタプリタで用いられる。
項やインタプリタで使用する値の型は図 1 に定義する。この言語は λ 計算にハンドラとオペレーション呼び出しを追加したものである。値の型 v は再帰型となる。継続の型 c やハンドラ h の型は関数型として定義される。trail t の型は空であることを表す • 型であるか、継続 (呼び出し文脈) を関数合成したものを表す関数型 (再帰型) のいずれかになる。そしてメタ継続 m は 継続 c と trailt、ハンドラ h を要素に持つリスト型として定義する。初期継続は id c として定義され、継続が空になったら trail、メタ継続の順番に中身の実行に移る関数となっている。初期 trail id t は • 型の値を Bullet として空の trail を表す。また (::) は継続 c と trail t の、(@) は trail t 同士の関数合成を行う。
図 2 に代数的エフェクトとハンドラの CPS インタプリタを示す。継続 c に加え、trail t とメタ
継続 m も引数として受け取る。呼び出し文脈を扱うために trail を、CPS インタプリタにさらにもう一度 CPS 変換を施した 2CPS となるためメタ継続を使用する。そのため trail やメタ継続は代数的エフェクトとハンドラを実装するためのデータである。まず λ 項の解釈は、trail t とメタ継続 m を η-簡約すれば通常の CPS インタプリタと変わらない。trail やメタ継続は λ 計算の評価時にはただそのまま引き渡すだけになっている。また 2.3 節で説明した通り以降の節で条件文項が必要になる場合があるが、λ 項同様 trail とメタ継続を η-簡約すれば従来のインタプリタと変わらないため本稿では条件文の CPS インタプリタは示さない。
ハンドラ try e1 with (x; k). e2 はまず e1 を評価する。その際、継続と trail は空のものをセットし、メタ継続に現在の継続 c、trail t、ハンドラ h を新たに追加する。メタ継続に try with の外側

6

E [[x]] ρ c
E [[λx. e]] ρ c
E [[e1 @ e2 ]] ρ c===λt. λm. c ρ(x) t m
λt. λm. c (λv. λc′ . λt′ . λm′ . E [[e]] ρ[v/x] c′ t′ m′ ) t m
λt. λm.
E [[e1 ]] ρ (λv1 . λt1 . λm1 .
E [[e2 ]] ρ (λv2 . λt2 . λm2 . v1 v2 c t2 m2 ) t1 m1 ) t m

E [[try e1 with (x; k). e2 ]] ρ c=

E [[call (e)]] ρ cdeep handler のとき=

λt. λm. E [[e1 ]] ρ id c id t ((c, t, h) :: m)where h = λv. λvc . λc′ . λt′ . λm′ . E [[e2 ]] ρ[v/x][vc /k] c′ t′ m′
λt. λm. E [[e]] ρ (λv. λt′′ . λ((c0 , t0 , h) :: m0 ). h v vc c0 t0 m0 ) t m
where vc = λv ′ . λc′ . λt′ . λm′ . c v ′ t′′ ((c′ , t′ , h) :: m′ )shallow handler のとき

where vc = λv ′ . λc′ . λt′ . λm′ . c v ′ (t′′ @ c′ :: t′ ) m′

図 2. 代数的エフェクトとハンドラのための CPS インタプリタの継続 c を保持することで、e1 の評価中にオペレーション呼び出しが現れても try with の内側の継続のみが扱えるようになっている。つまりメタ継続に要素を追加することが、ハンドラで限定する範囲の区切りとなっている。そのため try with を評価するたびにメタ継続の要素が増えていくことになる。そしてメタ継続に追加されるハンドラ h は高階関数として定義している。「値 v (引数値)、限定継続を表す値 vc 、継続 c′ 、trail t′ 、メタ継続 m′ を受け取り、そのもとで e2 を実行する」というハンドラの処理を表す関数となる。ここで e2 を評価する際の環境 ρ に x が v 、k が vcである情報が追加され、引数値 x と切り取られた限定継続 k を使うことが可能となる。
次に call (e) は、「まず e を評価しその後ハンドラの処理に移る」という評価になる。そのため実際のインタプリタでは e の評価時の継続が「ハンドラの処理に移る」となっている。具体的に、この継続の定義は e を評価して得られた値 v 、評価後の trail t′′ 、メタ継続が渡される。このときのメタ継続は (c0 , t0 , h) :: m0 と必ず要素が一つ入ったリストとなる。これはオペレーション呼び出しは必ずハンドラの中で行われるという仮定に対応し、メタ継続の最初の要素を取得することで直近のハンドラにアクセスしている。そしてハンドラ h に引数値 v 、オペレーション呼び出しが行われた時点における限定継続を表す関数 vc 、ハンドラの外側の継続 c0 、trail t0 、メタ継続 m0 を渡す。
ここで vc は限定継続に渡す値 v ′ とこの限定継続が呼び出されたときの継続 (呼び出し文脈) c′ 、t′ 、m′ を受け取り、call (e) が評価された時点での継続 c 及び trail t′′ を実行する高階関数である。つ
まり限定継続 vc は現在の継続 c と trail t′′ のみ捕捉し、そのときのメタ継続 (c0 , t0 , h) :: m0 は含まないため、ハンドラの内側の継続のみが限定継続として扱えるようになっている。そしてこの vcの関数の本体部分に deep handler と shallow handler の違いが現れている。実際に、c を実行する
ときの trail とメタ継続 (図のハイライトされた部分) に注目してみよう。

• deep handler の場合
c は引数として v ′ 、trail として t′′ 、メタ継続として m′ に (c′ , t′ , h) を新たに追加したものを受け取ったもとで実行される。メタ継続 m′ に要素が追加されることで継続 c と c′ が区切られているため、継続 c の計算にハンドラが入っていることを表している。
• shallow handler の場合
c は引数として v ′ 、trail として t′′ と c′ 、t′ が合成されたもの、メタ継続として要素の追加なしに m′ のみを受け取ったもとで実行される。このように呼び出し文脈を trail に保持することで、c の中でオペレーション呼び出しが現れた際に呼び出し文脈 (trail) も限定継続として捕捉されるようになり、shallow handler によって限定された継続にはハンドラが囲まれないことを表現している。
trail は shallow handler の場合のみ合成されており、deep handler の場合では trail は実質的には
7

E [[try e1 with D (x; k). e2 ]] ρ c = λt. λm. E [[e1 ]] ρ id c id t ((c, t, h) :: m)where h = λv. λc1 . λt1 . λ((c0 , t0 , h) :: m0 ). E [[e2 ]] ρ[v/x][vc /k] c0 t0 m0
where vc = λv2 . λc2 . λt2 . λm2 . c1 v2 t1 ((c2 , t2 , h) :: m2 )E [[try e1 with S (x; k). e2 ]] ρ c = λt. λm. E [[e1 ]] ρ id c id t ((c, t, h) :: m)where h = λv. λc1 . λt1 . λ((c0 , t0 , h) :: m0 ). E [[e2 ]] ρ[v/x][vc /k] c0 t0 m0
where vc = λv2 . λc2 . λt2 . λm2 . c1 v2 (t1 @ c2 :: t2 ) m2
E [[call (e)]] ρ c=λt. λm.
E [[e]] ρ (λv. λt′ . λ((c0 , t0 , h) :: m0 ). h v c t′ ((c0 , t0 , h) :: m0 ) )t m

図 3. ハンドラで deep/shallow を区別するインタプリタ

使われず常に同じ値を引き渡すだけになっている。つまり trail は shallow なハンドラの挙動を表現するためだけに使われる。
4 種類の限定継続演算子のインタプリタとは、メタ継続にハンドラ h が追加されていること、
call (e) の引数 e を評価した後に限定継続を切り取る操作をすることが異なるだけで、本質的な継続の扱い方は同様の挙動で定義することができている。

3.1

ハンドラで deep/shallow を区別するインタプリタ

上記で説明したインタプリタは 4 種類の限定継続演算子の CPS インタプリタを参考に作成したため、オペレーション呼び出しを評価するタイミングで限定継続の意味を与えるようになっている。
つまり囲んでいたハンドラが deep か shallow なのかは call (e) の評価時に分かるということである。一方で、ハンドラ側でも切り取られる限定継続の意味を与えるインタプリタも提唱したい。提唱するインタプリタは前節のものと独立であり、片方がより表現力が高いという訳ではない。
新たなインタプリタを図 3 に示す。図 2 のインタプリタとの違いは、e2 の実行環境に追加する
k の値 vc をどこで実際に定義するかである。図 2 のインタプリタでは try e1 with (x; k). e2 の評価時に現れる vc はただ単に何らかの値であるだけで、call (e) の評価時にそれぞれの限定継続 vc を定めていた。一方で図 3 では try with に D が付いているのものを deep handler の項、S が shallow
handler の項として、ハンドラ h の中で vc の意味も与えることにした。
図 3 のインタプリタを詳しく見てみる。deep と shallow どちらのハンドラであっても e1 の評価
で空の継続と trail をセットし、メタ継続に要素を追加していることはこれまでと同様であり、ハンドラ h の定義が少し変わる。まず関数の引数として値 v と call (e) が評価された時点での継続
c1 、trail t1 、メタ継続を受け取る。そのときのメタ継続は (c0 , t0 , h) :: m0 の形になっている (オペレーション呼び出しは必ずハンドラで囲まれた状態で起こるため)。そして e2 はメタ継続に積まれていた一つ外側の継続 c0 、trail t0 、メタ継続 m0 のもとで実行される。さらに e2 の環境として持つ k に対応する値 vc も定義する。vc の定義は、図 2 の deep の場合と shallow の場合のそれぞれと同様の定義を与えれば良い。call (e) の評価は、e を評価後直近のハンドラ h にアクセスをし、h にそのときの継続 c と trail t、メタ継続を渡すだけで良くなっている。ここで限定継続に自分自身と同じハンドラが入るという deep handler の性質上ハンドラ h に同じ h を渡しており、再帰的になっている。この再帰が型システムを導出する際に関係してくるが詳しくは 6 節で述べる。

3.2

ハンドラの非関数化

図 2 と図 3 のインタプリタが同等の挙動をすることを確かめるため、高階関数として定義されているハンドラの処理 h を非関数化 [21, 22] する。非関数化とは関数の body 部分で自由変数となっ8

E [[try e1 with (x; k). e2 ]] ρ c
E [[call (e)]] ρ cdeep handler のとき
shallow handler のとき
E [[try e1 with D (x; k). e2 ]] ρ c
E [[try e1 with S (x; k). e2 ]] ρ c
E [[call (e)]] ρ c==λt. λm. E [[e1 ]] ρ id c id t ((c, t, (x, k, e2 , ρ)) :: m)λt. λm. E [[e]] ρ (λv. λt′′ . λ((c0 , t0 , (x, k, e0 , ρ0 )) :: m0 ).
E [[e0 ]] ρ0 [v/x][vc /k] c0 t0 m0 ) t m′′′′
where vc = λv . λc . λt . λm . c v ′ t′′ ((c′ , t′ , (x, k, e0 , ρ0 )) :: m′ )where vc = λv ′ . λc′ . λt′ . λm′ . c v ′ (t′′ @ c′ :: t′ ) m′===

λt. λm. E [[e1 ]] ρ id c id t ((c, t, (x, k, e2 , ρ)D ) :: m)λt. λm. E [[e1 ]] ρ id c id t ((c, t, (x, k, e2 , ρ)S ) :: m)λt. λm. E [[e]] ρ (λv. λt′′ . λ((c0 , t0 , h) :: m0 ).
E [[e0 ]] ρ0 [v/x][vc /k] c0 t0 m0 ) t m
if h = (x, k, e0 , ρ0 )D
where vc = λv ′ . λc′ . λt′ . λm′ . c v ′ t′′ ((c′ , t′ , h) :: m′ )if h = (x, k, e0 , ρ0 )S
where vc = λv ′ . λc′ . λt′ . λm′ . c v ′ (t′′ @ c′ :: t′ ) m′

図 4. 図 2 と 図 3 の型 h を非関数化したインタプリタているものを保持するコンストラクタを定義し、関数の代わりにそのコンストラクタが必要になったタイミングで元々関数の本体部分で行っていた挙動をするような変換である。
非関数化を行ったインタプリタを図 4 に示す。上段は図 2 のインタプリタを下段は図 3 のインタプリタを非関数化したものである。try e1 with (x; k). e2 では、ハンドラ内の式 e1 の評価でメタ継続に追加するハンドラは関数ではなく、ハンドラの処理に必要な情報を保持したコンストラクタ(x, k, e2 , ρ) となる。下段は構文として deep handler と shallow handler を分けているためこのコンストラクタに deep か shallow の区別をつけているが、本質的には上下段の挙動は同じである。
そして call (e) では e を評価した後の継続として、そのときのメタ継続 (c0 , t0 , h) :: m0 を展開し、ハンドラ h の情報 (x, k, e0 , ρ0 ) を使う。上段の場合は e0 を c0 、t0 、m0 のもとで評価するようにし、そのときの環境に追加する限定継続の関数は deep か shallow かの場合によってそれぞれ定義する。下段の場合も e0 を c0 、t0 、m0 のもとで評価するようにし、そのときの限定継続はハンドラのコンストラクタに付随された D か S かによって適当な限定継続の関数を定義している。ゆえに、deep handler だった場合の上段の挙動と、下段の try with D の挙動は同じとみなせ、shallow
handler の場合も同様である。
したがって 3.1 節の議論の結論を以下にまとめる。

• 限定継続の具体的な定義を try with と call のどちらのタイミングで行っても実装できる。
• 同じインタプリタで deep handler と shallow handler を共にサポートしたい場合は図 3 のような意味論になるが、ハンドラの定義が再帰的となる。

4

既存のインタプリタとの比較

本節では Hillerström らの既存の CPS インタプリタ [14] と本稿のインタプリタが同様の挙動をすることをインフォーマルな形で議論する。代数的エフェクトとハンドラのインタプリタの要となる限定継続を表す関数の定義について、本稿のインタプリタは高階関数で定義したのに対し、Hillerströmらの既存のインタプリタはリストの構造を用いて定義している。正しくは deep handler についてはHillerström らも高階関数でも定義しているが、deep handler と shallow handler の両方を実装する
ものはリスト構造でのみ示しているため本節ではリスト構造を用いたインタプリタで詳しい比較を行う。

9

Hillerström らのインタプリタでは正常終了したときの継続 (pure continuations) c とハンドラ hのペアを要素としたリストをメタ継続 m としている。本稿では継続 c が正常終了したときの継続に相当する。そのため後の説明ではどちらのインタプリタであってもこれらの記号を c、h、m に統一する。ここで Hillerström らのインタプリタのメタ継続は (c, h) :: m と定義されているが、先頭の要素が現在の継続とハンドラを表しており、ペア同士の c を h で囲むこととしている。対して本稿のインタプリタは継続 c とメタ継続 m を別々の引数としてインタプリタに渡している。そのため現在の継続はインタプリタの引数である c で、そのときのメタ継続が (c′ , h) :: m であった場合、h は c を囲むハンドラ、c′ は h の一つ外側の継続であることに注意する。
Hillerström らの CPS インタプリタではハンドラ try e with H (H にはオペレーションが連なっている。) は、そのときのメタ継続 m に初期継続を表す空リストと H を評価して得られたハンドラ
h のペアを追加した新しいメタ継続 ([], h) :: m のもとで e を評価する。Hillerström らのインタプリ
タもハンドラが評価されるごとに継続とハンドラをメタ継続に追加していき、ハンドラで限定される継続の範囲を区切っている。オペレーション呼び出しの評価では、そのときのメタ継続 (c, h) :: m
を rk = (c, h) :: [] と残りのリスト m で分ける。これはオペレーション呼び出しが起こった時点における直近のハンドラ h 内の継続 c とその外側の継続を分けているということである。そして hに引数の値やオペレーションの名前、rk 、m を渡してハンドラの処理に移る。h に渡った後 rk を用いて限定継続を表す関数が作られるが、本稿と Hillerström らのインタプリタではこの関数の定義の仕方が異なる。そのためこの関数の定義に着目し、deep handler と shallow handler に分けて二つのインタプリタの挙動を確認していく。

4.1

deep handler の場合

Hillerström らのインタプリタは名前付きオペレーションに対応しているが、本稿のインタプリタ
はオペレーション呼び出しが起きたら必ず直近のハンドラで処理を行う仕様になっている。しかし
2.3 節で示した通り deep handler は名前付きオペレーションを模倣することが可能であるため、直近のハンドラで処理する場合と名前付きオペレーションの場合に分けて説明する。
4.1.1

オペレーション呼び出しが起こったとき、直近のハンドラで処理する場合

まず直近のハンドラにあるオペレーションの名前が目的のオペレーションと一致した場合を考える。Hillerström らのインタプリタは rk = (c, h) :: [] を用いて限定継続を表す関数が以下のように定義される。
λ v ((c′ , h′ ) :: m′ ). app ((c, h) :: (c′ , h′ ) :: m′ ) v
この関数の v は限定継続に渡される引数、((c′ , h′ ) :: m′ ) は限定継続が呼び出されたときのメタ継続である。app は Hillerström らの CPS インタプリタ特有の計算構文であるが、メタ継続の最初の要素から順に継続を適用していくものであり、この限定継続の関数は「継続 c から実行し、この継続 c をハンドラ h が囲んでいること」を表している。本稿で定義される deep handler の限定継続の関数はλv. λc′ . λt′ . λm′ . c v t ((c′ , t′ , h) :: m′ )となっているが、これも「継続 c を実行し、このときハンドラ h が囲んでいること」を意味しており、これら二つの限定継続を表す関数が同等の挙動であることが確認できる。

4.1.2

オペレーション呼び出しが起こったとき、直近のハンドラで処理する場合(名前付きオペレーションの場合)

次に目的のオペレーションが存在するハンドラは内側から n 個目のハンドラで、目的のハンドラ
までに別の n − 1 個のハンドラにも囲まれていると言う状況を考える。内側から i 番目のハンドラの中の継続を ci 、ハンドラでの処理を hi とする。

10

Hillerström らの CPS インタプリタは名前付きのオペレーションに対応しているため、この状況を考慮したインタプリタとして定義されている。前節と同様にして rk と m を用いるが、ここでrk の中身を rk = (c1 , h1 ) :: [] と置き換える。また n 個以上のハンドラで囲まれている状況である
ため m も (c2 , h2 ) :: ... :: (cn−1 , hn−1 ) :: (cn , hn ) :: mout とする。h1 には名前が一致するオペレーションが定義されていないため限定継続の関数は作らず、m の先頭の要素である (c2 , h2 ) を rk の先頭に追加して一つ外側のハンドラ h2 を見ていくようにする。そのため目的のハンドラ n に達す
るまでにこの動作を繰り返していき rk = (cn , hn ) :: (cn−1 , hn−1 ) :: ... :: (c2 , h2 ) :: (c1 , h1 ) :: [] と増幅する。そして hn には目的のオペレーションがあるため rk を用いて限定継続を表す関数を作る。しかし c1 から処理するような関数にしたいため、リスト rk の順番を反転させ
λ v ((c′ , h′ ) :: m′ ). app ((c1 , h1 ) :: (c2 , h2 ) :: ... :: (cn−1 , hn−1 ) :: (cn , hn ) :: (c′ , h′ ) :: m′ ) v
として限定継続の関数を定義する。
本稿のインタプリタでは 2.3 節で示したように、ハンドラの処理部分を if x = a then ...
else k call(x) として模倣した場合で考える。最初にオペレーション呼び出しが起こったときの継続が c1 、メタ継続 m は (c2 , h1 ) :: (c3 , h2 ) :: ... :: (cn , hn−1 ) :: (cout , hn ) :: mout 2 となっている状況から説明する。まずメタ継続の最初の要素 (c2 , h1 ) にアクセスし、h1 を実行するがそのとき限定継続の関数 vc1 や一つ外側の継続 c2 、残りのメタ継続を渡す。ここで vc1 = λv ′ . λc′ . λm′ . c1 v ′ ((c′ , h1 ) :: m′ )である。そして h1 ではオペレーションの名前が一致ないこととなるため else 部分を行い一つ外側のハンドラ h2 に飛ぶ。このとき切り取られる限定継続は c′2 = λv. λm. vc1 v c2 m (継続 c2 のもとで関数vc1 に適用する。) となる。そして h2 にはこの限定継続を実行するための関数 vc′2 が渡され処理していく。これを目的の n 番目のハンドラに達するまで繰り返していくため、内側から i 番目 (2 ≤ i ≤ n) のハンドラ hi には、限定継続 c′n = λv. λm. vcn−1 v cn m の関数 vc′n = λv ′ . λc′ . λm′ . c′n v ′ ((c′ , hn ) :: m′ )が渡されることになる。そして目的のハンドラ hn ではオペレーションの名前が一致したこととして処理を行うようになり、ここで限定継続 vc′n が使われたとする。すると関数を展開していくことになり、最終的に

λv. λc′ . λm′ . c1 v ((c2 , h1 ) :: (c3 , h2 ) :: ... :: (cn , hn−1 ) :: (c′ , hn ) :: m′ )となる。
まとめると、Hillerström らの CPS インタプリタはリストの要素を増やして最後に要素を反転するのに対し、我々のインタプリタは関数の合成を行って後に展開していくという違いであり、同等の挙動をしていることが見て取れる。
また、deep handler のみ Hillerström らもリスト構造を使わず高階関数の形でのインタプリタも定義している。こちらとの比較としては、メタ継続の定義が多少異なるものの、我々と Hillerström
らのインタプリタは本質的に同等のものとなっている。

4.2

shallow handler の場合

2.3 節の通り shallow handler の場合は名前付きオペレーションが模倣できなかったため、直近のハンドラで処理する場合でのみ限定継続を表す関数を比較する。
4.1.1 節と同様に Hillerström らの CPS インタプリタは rk = (c, h) :: [] を用いて限定継続を表す関数が定義される。
λ v ((c′ , h′ ) :: m′ ). app ((c @ c′ , h′ ) :: m′ ) v(c @ c′ ) の部分は実際のものとは厳密には異なるが、「元々囲んでいたハンドラ h は捨てて、その外側の pure continuations c′ と c が合わさった下で c を実行すること」を表している。本稿で定義される shallow handler の限定継続の関数は
λv. λc′ . λt′ . λm′ . c v (t @ c′ :: t′ ) m′2

deep handler では実質的には trail を使用しないため今回は省略している。

11ehx, ρ, c, t, mihλx. e, ρ, c, t, mi
he1 @ e2 , ρ, c, t, mihtry e1 with (x; k). e2 , ρ, c, t, mihcall (e), ρ, c, t, mih[], v, id t , []ih[], v, id t , (c, t, h) :: mih[], v, c, mihCApp1 (e, ρ) :: c, v, t, mihCApp2 (VFun(e, x, ρ)) :: c, v, t, mihCApp2 (VContD(c′ , t′ , h)) :: c, v, t, mihCApp2 (VContS (c′ , t′ )) :: c, v, t, mi
hCCall :: c, v, t, (c0 , t0 , h) :: m0 i
where h = (x, k, e0 , ρ0 )

⇒
⇒
⇒
⇒
⇒
⇒
⇒
⇒
⇒
⇒
⇒
⇒
⇒
⇒

he, [], [], id t , []ihc, ρ(x), t, mi
hc, VFun(e, x, ρ), t, mi
he1 , ρ, CApp1 (e2 , ρ) :: c, t, mi
he1 , ρ, [], id t , (c, t, (x, k, e2 , ρ)) :: mihe, ρ, CCall :: c, t, miv
hc, v, t, mi
hc, v, id t , mihe, ρ, CApp2 (v) :: c, t, mihe, ρ[x 7→ v], c, t, mi
hc′ , v, t′ , (c, t, h) :: mihc′ , v, t′ @(λv2 . λt2 . λm2 . c v2 t2 m2 ) :: t, mi
deep handler の場合
he0 , ρ0 [x 7→ v][k 7→ VContD(c, t, h)], c0 , t0 , m0 i
shallow handler の場合
he0 , ρ0 [x 7→ v][k 7→ VContS (c, t)], c0 , t0 , m0 i

図 5. 代数的エフェクトとハンドラのための抽象機械となっていて、継続 c と c′ が合わさるのではなく c′ を trail に保持し、その下で c を実行している。そしてハンドラ h は c を囲まずに捨てられている。よって shallow handler の場合でも二つのインタプリタが同等の挙動であることが確認できる。

5

代数的エフェクトとハンドラのための抽象機械

代数的エフェクトとハンドラの機械語での実装の先駆けとして、本節では図 2 のインタプリタから導出した抽象機械を示す。抽象機械の導出には 4 種類の限定継続演算子のインタプリタに施した手法 [12] を用いている。代数的エフェクトとハンドラのための抽象機械もこの手法で問題なく導出することができた。手法の詳細としては、はじめに、高階関数として表現されている継続 c と ハン
ドラ h、クロージャを非関数化する。そして非関数化された継続 c は初期継続と関数適用の二つの継続、オペレーション呼び出しでの継続に対応するデータ構造が得られるが、ここで初期継続を空リスト、他の三つの継続の形はリストの cons とみなすことができる。そのため継続をリスト構造に変換する。継続のリストの要素は、関数適用 e1 @ e2 の関数部分 e1 を評価した後の継続 (CApp1 )と引数部分 e2 を評価後の継続 (CApp2 )、call (e) で e を評価後のハンドラの処理に移るための継続 (CCall ) をそれぞれ表すデータとなっている。以上の変換を施すとインタプリタの関数はすべて
末尾呼び出しとなり、関数の引数を状態とみなすだけで抽象機械を導出することができる。
代数的エフェクトとハンドラの抽象機械は図 5 に示す。この抽象機械は式 e を he, [], [], Bullet, []iとして空の環境、継続、trail (Bullet) そしてメタ継続のもとではじめる。λ 計算は従来のもの [2, 9, 23]と変わらないためここでは割愛する。ハンドラ try e1 with (x; k). e2 は e1 を実行するが、そのときの継続と trail は空のもので新たにセットされ、現在の継続と trail はメタ継続に追加される。また一緒に (x, k, e2 , ρ) として例外処理に必要なハンドラ情報も追加する。次に call (e) のときは引数 eを実行し、その後ハンドラの処理に移るために CCall を継続に追加する。そして CCall が呼び出されたとき、メタ継続の最初の要素 (c0 , t0 , h) にアクセスし、h は (x, k, e0 , ρ0 ) となっている。する
と式 e0 を環境 ρ0 、継続 c0 、trail t0 、メタ継続 m0 の下で実行してハンドラの処理に移る。このとき環境 ρ0 には x が v 、k が限定継続である情報が追加されるが、deep handler のときは VContDとして現在の継続と trail、同様のハンドラを保持するようにし、shallow handler のときは VContSとして現在の継続と trail のみを持つようにする。ここで deep handler のみハンドラの情報を持つのは限定継続にハンドラが囲まれるため必要となる。さらに、CApp2 として VContD(c′ , t′ , h) や

12

項の型
trail の型
メタ継続の型
ハンドラの型

τ
µ
σ
η

:=
:=
:=
:=

int | τ1 → τ2 hµα , σα i α hµβ , σβ i β• | τ1 → hµ, σi τ2[] | (τ → hµ, σi τ ) × µ′ × η :: σ ′τv → τvc → τ hµα , σα i α hµβ , σβ i β
τvc := τ1 → τ2 hµ2 , σ2 i τ3 hµ3 , σ3 i τ4

図 6. 型システム用の型定義

VContS (c′ , t′ ) が呼び出されたときは、それぞれ c′ を実行するようにすることで限定継続を呼び出すようになっている。そして、その時点での継続 c、trail t は、VContD (deep handler) のときは
h と一緒にメタ継続 m に追加してハンドラを囲むことを表現する。VContS (shallow handler) のときは 関数合成で t′ に追加する。関数合成するために継続 c は η expand されている。trail に入れることによって c′ の中で再び CCall が呼び出されると (オペレーション呼び出しが起こると) この増幅された trail ごと限定継続となりキャプチャされることとなる。
Hillerström らの既存の抽象機械 [14] と比較すると、CPS インタプリタと同様に、直近のハンドラで処理するときは deep と shallow の場合で同等の挙動をすることが確認できており、名前付きオペレーションの対応は deep handler のみ確認している。本稿の抽象機械はインタプリタから導出されたものであるため、抽象機械同士の比較も 4 節で説明した挙動を対応するコンストラクタで置き換えれば同様にして示される。

6

代数的エフェクトとハンドラのための型システム

本稿で提唱したインタプリタは継続 c やハンドラ h など全てを高階関数として定義している。
高階関数で定義すると、特定のデータ構造を要求せずとも挙動を規定しており汎用性の高いものになっている。そのため、高階関数で定義されたインタプリタから自然に型システムを導くことが可能となる。具体的な手法としては Danvy と Filinski [5] や Cong ら [4] の方針に従い、インタプリ
タに型を割り振ることで導出していく。ハンドラが再帰的になる図 3 のインタプリタは再帰型が必要になるため、本稿では base type で型を付けられる図 2 のインタプリタから導いた型システムを提唱する。この型付き言語を定義し、それに対するインタプリタは定理証明支援言語 Agda で実装できており、停止性や健全性を証明した。
型システムのための型定義を図 6 に示す。型判定は Γ ` e : τ hµα , σα i α hµβ , σβ i β という形になる。answer type に trail とメタ継続の型が付随している。これで「型環境 Γ のもとで式 e は τ 型を持ち、e を「τ 型の値と µα 型の trail、σα 型のメタ継続のもとで answer type が α になる継続」と µβ 型の trail、σβ 型のメタ継続のもとで実行すると answer type が β 型になる」と読む。
代数的エフェクトとハンドラのための型規則を図 7 に示す。λ 計算の三つの規則は trail とメタ
継続を無視すれば一般的な型規則と同様となる。(OperationCall −Deep) は deep handler で処理されるときの、(OperationCall −Shallow ) は shallow handler で処理されるときのオペレーション呼び出しの型規則となっている。(Handler ) の規則で使われる id-cont-type は初期継続に伴う制約で、(OperationCall −Shallow ) に出てくる compatible は trail を関数合成する際に必要な制約となっており、それぞれ図 8 に詳細を示す。≡ の両辺の型は同じ型であることを定義する。

7

関連研究

代数的エフェクトとハンドラと、4 種類の限定継続演算子の関係性は提唱されている。Forster ら[11] は型なし言語での deep handler と shift0/reset0 間の意味論とその同値性を証明している。Piróg13

Γ(x) = τ(Var )Γ ` x : τ hµα , σα i α hµα , σα i αΓ, x : τ2 ` e : τ1 hµβ , σβ i β hµγ , σγ i γ(Fun)Γ ` λx. e : (τ2 → τ1 hµβ , σβ i β hµγ , σγ i γ) hµα , σα i α hµα , σα i αΓ ` e1 : (τ2 → τ1 hµα , σα i α hµ2 , σ2 i β) hµ1 , σ1 i γ hµβ , σβ i δ Γ ` e2 : τ2 hµ2 , σ2 i β hµ1 , σ1 i γ(App)Γ ` e1 @ e2 : τ1 hµα , σα i α hµβ , σβ i δη = τ ′ → τvc → τ3 hµ3 , σ3 i τ4 hµ4 , σ4 i τ5
id-cont-type(γ, µid , σid , γ ′ )Γ ` e1 : γ hµid , σid i γ ′ h•, (τ → hµα , σα i α) × µβ × η :: σβ i βΓ, x : τ ′ , k : τvc ` e2 : τ3 hµ3 , σ3 i τ4 hµ4 , σ4 i τ5
(Handler )Γ ` try e1 with (x; k). e2 : τ hµα , σα i α hµβ , σβ i βη = τ ′ → τvc → τ0 hµ0 , σ0 i τ0′ hµ′0 , σ0′ i γ
τvc = τ → τ1 hµ1 , σ1 i τ2 hµ2 , σ2 i αΓ ` e : τ ′ hµα , (τ0 → hµ0 , σ0 i τ0′ ) × µ′0 × η :: σ0′ i γ hµβ , σβ i β(OperationCall −Deep)Γ ` calld (e) : τ hµα , (τ1 → hµ1 , σ1 i τ2 ) × µ2 × η :: σ2 i α hµβ , σβ i βη = τ ′ → τvc → τ0 hµ0 , σ0 i τ0′ hµ′0 , σ0′ i γ
τvc = τ → τ1 hµ1 , σ1 i τ2 hµ2 , σα i αcompatible((τ1 → hµ1 , σ1 i τ2 ), µ2 , µ′2 )compatible(µ′ , µ′2 , µα )Γ ` e : τ ′ hµ′ , (τ0 → hµ0 , σ0 i τ0′ ) × µ′0 × η :: σ0′ i γ hµβ , σβ i β(OperationCall −Shallow )Γ ` calls (e) : τ hµα , σα i α hµβ , σβ i β
図 7. 代数的エフェクトとハンドラのための型システム

id-cont-type(τ, •, [], τ ′ )id-cont-type(τ, •, (τ1 → hµ1 , σ1 i τ1′ ) × µ2 × η :: σ, τ ′ )==id-cont-type(τ, (τ1 → hµ1 , σ1 i τ1′ ), σ, τ ′ )=compatible(•, µ2 , µ3 )compatible((τ1 → hµ1 , σ1 i τ1′ ), •, µ3 )compatible((τ1 → hµ1 , σ1 i τ1′ ), (τ2 → hµ2 , σ2 i τ2′ ), •)compatible(τ1 → hµ1 , σ1 i τ1′ ,τ2 → hµ2 , σ2 i τ2′ , τ3 → hµ3 , σ3 i τ3′

=
=
=
=

τ ≡ τ′(τ1 ≡ τ ) ∧ (µ1 ≡ µ2 )∧(σ1 ≡ σ2 ) ∧ (τ1′ ≡ τ ′ )(τ1 ≡ τ ) ∧ (µ1 ≡ •) ∧ (σ1 ≡ σ) ∧ (τ1′ ≡ τ ′ )µ2 ≡ µ3(τ1 → hµ1 , σ1 i τ1′ ) ≡ µ3⊥
(τ1 ≡ τ3 ) ∧ (σ1 ≡ σ3 ) ∧ (τ1′ ≡ τ3′ )∧ compatible(τ2 → hµ2 , σ2 i τ2′ , µ2 , µ3 ))図 8. 初期継続と、trail の合成に伴う型システムの制約

14

ら [19] は型付き言語での deep handler と shift0/reset0 および shallow handler と control0/prompt0
が意味論的に同値であることを示している。本稿の代数的エフェクトとハンドラのインタプリタでも Piróg らの変換方法を用いて 4 種類の限定継続演算子を模倣できることを型なしで確認している。
Kammar [16] らは Haskell のモナドを用いて eﬀect handlers を実装している。この論文では deep
handler だけでなく shallow handler が紹介されている。そして deep handler と shallow handler
それぞれの型システムが示されており、deep と shallow の場合とで、限定継続を表す変数の型に違いが現れている。また継続モナドや自由モナドによって実装されているため CPS インタプリタに非常に近いものと考えられるが、本研究との対応関係については未確認のため今後の課題となる。
Leijen [17] は Koka 言語の row-type を用いて eﬀect polymorphism を実現している。eﬀect polymorphism によって名前付きオペレーションに対応した 代数的エフェクトとハンドラのための型システムが示されたもとで、Koka 言語での実装がされている。
Biernacki ら [3] は代数的エフェクトとハンドラにさらに lift と呼ばれるコンストラクタを追加している。複数のハンドラに同じ名前のオペレーションが定義されている状況でその名前のオペレーションを呼び出すとき、リフトでオペレーションを囲むことで直近のハンドラよりも外側にあるハンドラでの処理を指定することが可能となる。この計算の型規則は eﬀect polymorphism に基づきlift の規則も追加されて示されている。
これらの型システムと本研究の型システムとの対応関係を確認することも今後の課題となる。

8

まとめと今後の課題

本稿では trail やメタ継続を用いた新たな代数的エフェクトとハンドラのための CPS インタプリタを提唱した。インタプリタの設計として、ハンドラが deep/shallow の意味を持たせるタイミン
グをオペレーション呼び出しの評価時に行うものと、ハンドラの評価時に行うものの 2 種類を取り上げた。そしてインタプリタから抽象機械や型システムを機械的に導出した。また構文として名前付きオペレーションに対応していなかったが、deep handler であれば条件文を追加して模倣すれば従来のインタプリタと同様の挙動であることも示した。
今後は、shallow handler の名前付きオペレーションの模倣を可能にすることが課題となる。そして我々の型システムとこれまでに提唱された型システムとの等価性を確かめたい。また、4 種類の限定継続演算子のインタプリタに対して示した手法 [12] を本稿のインタプリタにも用いて、仮想機
械を導出し代数的エフェクトとハンドラのための低レベルな直接実装に向けた基盤を提供したい。

謝辞
有益なコメントをくださった査読者の皆様に感謝申し上げます。本研究は一部 JSPS 科研費
18H03218 の助成を受けたものです。

参考文献[1] Andrej Bauer and Matija Pretnar. Programming with algebraic eﬀects and handlers. J. Log. Algebraic
Methods Program., Vol. 84, No. 1, pp. 108–123, 2015.
[2] Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A dynamic continuation-passing style fordynamic delimited continuations. ACM Transactions on Programming Languages and Systems(TOPLAS), Vol. 38, No. 1, pp. 1–25, 2015.
[3] Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Handle with care: relational
interpretation of algebraic eﬀects and handlers. Proceedings of the ACM on Programming Languages,Vol. 2, No. POPL, pp. 1–30, 2017.

15

[4] Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai. A functional abstraction of typed invocation contexts. In 6th International Conference on Formal Structures for Computation and Deduction(FSCD 2021), pp. 12:1–12:18, 2021.
[5] Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. BRICS 89/12, 1989.
[6] Olivier Danvy and Andrzej Filinski. Abstracting control. In Proceedings of the 1990 ACM Conferenceon LISP and Functional Programming, pp. 151–160, 1990.
[7] Olivier Danvy and Andrzej Filinski. Representing Control: a Study of the CPS Transformation.
Mathematical Structures in Computer Science, Vol. 2, No. 4, pp. pp. 361–391, 1992.
[8] Paul Downen and Zena M Ariola. A systematic approach to delimited control with multiple prompts.
In European Symposium on Programming, pp. 234–253. Springer, 2012.
[9] R. Kent Dybvig, Simon L. Peyton Jones, and Amr Sabry. A monadic framework for delimited continuations. J. Funct. Program., Vol. 17, No. 6, pp. 687–730, 2007.
[10] Mattias Felleisen. The theory and practice of ﬁrst-class prompts. In Proceedings of the 15th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’88, pp. 180–190,
New York, NY, USA, 1988. ACM.
[11] Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of userdeﬁned eﬀects: Eﬀect handlers, monadic reﬂection, delimited control. Proc. ACM Program. Lang.,
Vol. 1, No. ICFP, pp. 13:1–13:29, August 2017.
[12] Maika Fujii and Kenichi Asai. Derivation of a virtual machine for four variants of delimited-control
operators. In 6th International Conference on Formal Structures for Computation and Deduction(FSCD 2021), pp. 16:1–16:19, 2021.
[13] Carl A. Gunter, Didier Rémy, and Jon G. Riecke. A Generalization of Exceptions and Control in MLlike Languages. In Proceedings of the Seventh International Conference on Functional Programming
Languages and Computer Architecture, FPCA ’95, pp. 12–23, New York, NY, USA, 1995. ACM.
[14] Daniel Hillerström, Sam Lindley, and Robert Atkey. Eﬀect Handlers via Generalised Continuations.
Journal of Functional Programming, Vol. 30, No. e5, 2020.
[15] Yukiyoshi Kameyama. Axioms for control operators in the cps hierarchy. Higher-Order and Symbolic
Computation, Vol. 20, No. 4, pp. 339–369, 2007.
[16] Ohad Kammar, Sam Lindley, and Nicolas Oury. Handlers in action. In Proceedings of the 18th ACM
SIGPLAN International Conference on Functional Programming, ICFP ’13, pp. 145–158, New York,NY, USA, 2013. ACM.
[17] Daan Leijen. Type directed compilation of row-typed algebraic eﬀects. In Proceedings of the 44th
ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 486–499, 2017.
[18] Marek Materzok and Dariusz Biernacki. Subtyping Delimited Continuations. In Proceedings of the
16th ACM SIGPLAN International Conference on Functional Programming, ICFP ’11, pp. 81–93,
New York, NY, USA, 2011. ACM.
[19] Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Typed equivalence of eﬀect handlers and delimited
control. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD
2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019.
[20] Gordon D. Plotkin and Matija Pretnar. Handlers of algebraic eﬀects. In Giuseppe Castagna, editor,
Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Heldas Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York,UK, March 22-29, 2009. Proceedings, Vol. 5502 of Lecture Notes in Computer Science, pp. 80–94.
Springer, 2009.
[21] John C Reynolds. Deﬁnitional interpreters for higher-order programming languages. In Proceedingsof the ACM annual conference-Volume 2, pp. 717–740, 1972.
[22] John C Reynolds. Deﬁnitional interpreters for higher-order programming languages. Higher-orderand symbolic computation, Vol. 11, No. 4, pp. 363–397, 1998.
[23] Chung-chieh Shan. A static simulation of dynamic delimited control. Higher-Order and Symbolic
Computation, Vol. 20, No. 4, pp. 371–401, 2007.
[24] 石尾千晶, 浅井健一. 4 種類の限定継続演算子のための型システム. 第 24 回プログラミングおよびプロ
グラミング言語ワークショップ論文集, 2022.

16