日本ソフトウェア科学会第 41 回大会 (2024 年度) 講演論文集

代数的エフェクトハンドラを持つ言語のプログラムに対するエフェクト列の静的な見積り
山﨑 陽介

川端 英之

弘中 哲夫

代数的エフェクトは制御の流れに対する様々な操作を抽象化する仕組みの一つで，CPS を用いずにモジュラーに記述できるようにした言語機構である．しかし，その機能を十分に活用するためには，複雑になりがちな制御フローを適切に把握したプログラミングが必要で，簡単ではない．本論文では，代数的エフェクトを用いたプログラミングの支援を目的として，プログラミング中で発生するエフェクト列を静的に見積もりプログラマに提示する手法を提案する．本アルゴリズムは，型検査とは独立しており，型にエフェクト列の情報を組み込むものとは異なる．エフェクトのハンドリング部分を詳細に検査することで，精度の高い見積りを得ることができる．本手法を組み込んだプログラ
ミング支援ツールは，エフェクト発生の順序や，未ハンドルエフェクトの有無などの情報をユーザに提供でき，代数的エフェクトを用いるプログラマの負担を大幅に軽減できることが期待される．

の代数的エフェクトの型システム [6] では，エフェク

1 はじめにトの情報を集合によって表しているため，エフェクト

代数的エフェクトとそのハンドラ [5] は制御の流れの発生順序までは把握することができない．他に，エに対する様々な操作を抽象化する仕組みの一つで，フェクトの情報を集合で扱わない型システムとして，

CPS を用いずにモジュラーに記述できるようにした

川俣ら [8] のものがある．これは，エフェクトの発生言語機構である．プログラム中のエフェクトの発生

順序を型システムに組み込んでいる．しかし，型のを抽象化してハンドラで定義するものである．例外

性質を満たすために，エフェクトの見積りが保守的ハンドラの一般化と見ることもでき，例外ハンドラとになりすぎてしまい，false positive が多くなってし異なる点は，処理がハンドラに移る際に，その地点でまっている．それらに対して，本論文で提案するアルの継続を切り取り，それを再開することができる点でゴリズムでは，型とは独立に扱い，エフェクトのハある．

ンドリング部分を詳細に検査することで，より精度

代数的エフェクトとそのハンドラを十分に活用すの高い，false positive が少ない見積りを得ることがるためには，複雑になりがちな制御フローを適切に把できる．また，川俣ら [8] のシステムでは，シャロー

握したプログラミングが必要で，簡単ではない．

ハンドラ [3] を採用していたが，我々のシステムでは，

本論文では，Pretnar の代数的エフェクトとそのハ

ディープハンドラを採用している．

ンドラの言語体系 [6] を元に，代数的エフェクトを用

本論文の貢献は，代数的エフェクトを持つ言語に対いたプログラミングの支援を目的として，プログラミ

してのエフェクト列の静的な見積もりを実現するア

ング中で発生するエフェクトの発生順序を静的に見積

ルゴリズムの提案と実装である．本アルゴリズムのもりプログラマに提示する手法を提案する．Pretnar

健全性の証明は完成していないが，妥当と予想している．実装は GitHub†1 にて公開している．

Static Estimation of Eﬀect Row for programs in an
Language with Algebraic Eﬀect Handlers.
Yosuke Yamasaki, Hideyuki Kawabata, Hironaka Tetsuo, 広島市立大学, Hiroshima City University.

本論文の構成は次のとおりである．2 節では代数的†1 https://github.com/zaki5m/effect_analyzer

::=x, y, k変数|

true | false

ブール定数

|

fun x 7→ c

関数

|

h

ハンドラ

h

::=

handler { return x 7→ cr , [opi (x; k) 7→ copi ]i∈1...n }

ハンドラ

c

::=

return v

returnv|

op (v; y.c)op 呼び出し|do x ← c1 in c2

逐次実行

|

if v then c1 else c2

条件分岐

|

v1 v2

関数適用

|

with v handle c

ハンドリング
図1

対象言語の構文

エフェクトハンドラの概要について述べる．3 節でdef

c = do name1 ← read() inは，本論文で対象とする言語を定義する．4 節では，

do name2 ← read() inエフェクトの時間的な見積りであるエフェクト列について述べる．5 節では，プログラムからエフェクト

return name1ˆname2

列を見積もるアルゴリズムについて述べる．6 節ではwith h handle c
そ こ で ，with h handle c を 実 行 す る こ と関連研究を述べる．最後に 7 節では，まとめと今後の課題を述べる．

2 代数的エフェクトとそのハンドラ
代数的エフェクトとそのハンドラ [5] を持つ言語では，エフェクトを発生させるとその地点での継続 (その地点での残りの計算) を切り取って，ハンドラへ処理が渡される．ハンドラは，渡された継続を用いて処理を行うことができる．Pretnar の代数的エフェクトとそのハンドラのチュートリアル [6] を元に例を示す．
以下の例の言語は，3 節で定義する．また，以下で出現する記号ˆは文字列の結合を表している．
以下は，read が呼ばれると常に “Bob” を継続に渡すようなハンドラである．

を 考 え る ．こ の プ ロ グ ラ ム は ，read() と い うエ フ ェ ク ト が 発 生 す る と ，ハ ン ド ラ に 捕 捉 さ
れ k "Bob" が 実 行 さ れ る ．継 続 k は fun y 7→

with h handle do name1 ← y in do name2 ←read() in return name1ˆname2 である．
k "Bob" の評価を進めると，with h handle return"Bob"ˆ"Bob" となり，h の return 節に"BobBob"を引数として渡して，最終的には，return "BobBob"となる．
次にハンドラを以下のように変更した例を考える．

h′ = handler{return x 7→ return x,
defread( ; k) 7→
do x ← k "Bob" in

h = handler{return x 7→ return x,

k x}
ハンドラ h と h′ が異なる点は read というエフェ

read( ; k) 7→ k "Bob"}
このハンドラの元で実行するプログラムを以下にクトが発生し，ハンドラが捕捉した時の動作が異な

def

定義する．

る．ハンドラ h は，継続 k に “Bob” を渡す処理のみだったが，ハンドラ h′ は継続 k に “Bob” を渡した
結果 x を，再び継続 k に x を渡している．つまりハンドラ h′ では継続を 2 回再開している．
そこで，with h′ handle c を実行することを考え

る．エフェクト read が 3 回呼び出され，最終的には，

3. 2 操作的意味論

return "BobBobBobBobBobBob" となる．

評価関係の定義を図 2 に示す．Pretnar のもの [6]このように，ハンドラは継続を受け取ることで，制にイベントトレースが加わっており，川俣らのもの

御フローを変化させることが可能である．また，継続[8] のハンドラをシャローハンドラからディープハン

を複数回再開するなどの処理も可能なためより複雑ドラへ変更したものである (E-HANDLINGINOP)．まなシステムの際には，制御フローを正しく認識するこた，川俣らのもの [8] は再帰を許す体系だが，本言語とが難しくなる．

では再帰を許さない．
ディープハンドラとシャローハンドラは表現力が3 対象言語等価なことが知られており，ディープハンドラはシャ

本節では，アルゴリズムの対象とする言語の構文，

ローハンドラを模倣することが可能であり，シャロー

操作的意味論，型システムについて述べる．

ハンドラは再帰を用いてディープハンドラを模倣することが可能である [3]．

3. 1 対象言語の構文評価関係は，コンピュテーション c とイベントト

本論文で用いる言語の構文を図 1 に示す．この構

レース η のペア c, η の二項関係 c, η ⇝ c′ , η ′ となっ

文は Pretnar の体系 [6] と同一のものである．この言ており，これは川俣らのもの [8] と同一である．イベ語は，エフェクトが発生しない値 v とエフェクトがントトレースとは，評価の途中でハンドルしたイベン発生する可能性のあるコンピュテーション c で構成

ト (エフェクト) を記録している，ハンドル済みオペ

される．

レーションの列である．イベントトレース η の構文

プログラムで発生するエフェクトはオペレーションは η ::= ϵ | op✓ | η; η と定義される．ϵ は空のイベンと呼ばれる項で抽象化し，ハンドラにオペレーション

トトレースを表している．op✓ は，ハンドル済みオペに対応する実装を定義する．オペレーション呼び出し

レーションを表している．また，; はイベントトレー(op 呼び出し)，すなわち op(v; y.c) は，v がオペレースの連結を表している．(E-HANDLINGINOP) でオペ

ション op への引数としてハンドラに渡され，y が op

レーションがハンドラに捕捉された際にハンドル済

から継続に渡される値を受け取る変数，c が継続であみオペレーション op✓ が末尾に追加される．例えば，

る．op 呼び出しが起こると，引数 v がハンドラに渡さ✓評価の結果イベントトレースが op✓
1 ; op2 であった場

れ，ハンドラ内で継続が再開されると，変数 y に値が合は，評価の途中で，op1 がハンドルされた後に op2

束縛され，c が実行される．ハンドラは return 節とがハンドルされたことを表している．

op 節を持っており，op 節の [opi (x; k) 7→ copi ]i∈1...nは，op1 (x; k) 7→ cop1 , . . . , opn (x; k) 7→ copn の略記で

3. 3 型システム

ある．with v handle c はハンドラ v のもとで，項型 シ ス テ ム は Pretnar [6] の も の と 同 一 で あ る ．

c を実行する．

Pretnar [6] の型システムの構文を図 3 に示す．値

また，オペレーション呼び出しに明示的な継続とら型 A とコンピュテーション型 C に分かれており，コない generic eﬀect [4] を Pretnar の体系 [6] に合わせ

ンピュテーション型 A!∆ の ∆ はエフェクトの集合て以下のように導入する．

である．このエフェクトの集合 ∆ は，そのコンピュ

def

op = fun x 7→ op(x; y.return y)

テーションが発生させる可能性のあるエフェクトの

generic eﬀect はシンプルに使えるが，表現力は同集合を表している．型付け規則は付録 (図 10) に掲載

じである．

する．

また，本論文内での例の際に，unit や文字列など

また，Pretnar の型システム [6] で示されている性質のブール定数以外の定数の導入はできるものとする．

は全て満たす．つまり，以下の 2 つの性質を満たす．

• 適切に型付けされたプログラムは行き詰まり状

c1 , η1 ⇝ c′1 , η1′(E-SEQ)do x ← c1 in c2 , η ⇝ do x ← c′1 in c2 , η ′do x ← returnv in c, η ⇝ c[v/x], ηdo x ← op(v; y.c1 ) in c2 , η ⇝ op(v; y.do x ← c1 in c2 ), η
if true then c1 else c2 , η ⇝ c1 , η(E-IFTRUE)(E-SEQOP)(E-SEQRET)(fun x → c) v, η ⇝ c[v/x], η

if false then c1 else c2 , η ⇝ c2 , η(E-APP)(E-IFFALSE)

以下では h = handler{return x 7→ cr , [opi (x; k) 7→ copi ]i∈1...n } とする

c, η ⇝ c′ , η ′(E-HANDLING)
with h handle c, η ⇝ with h handle c′ , η ′with h handle (return v), η ⇝ cr [v/x], η(E-HANDLINGRET)

op ∈ {op1 , . . . , opn }with h handle opi (v; y.c), η ⇝ ci [v/x, (fun y 7→ with h handle c)/k], η; op✓iop ∈/ {op1 , . . . , opn }with h handle op(v; y.c), η ⇝ op(v; y.with h handle c), η
図2

A, B

C, D

::=

bool

ブール型

|

A→C

関数型

|

C⇒D

ハンドラ型

::=

A!{op1 , . . . , opn }
図3

型の構文

態にならないことが保証される [1]• 以下に示す型安全性 (定理 3.1)

(E-HANDLINGINOP)(E-HANDLINGOUTOP)

評価規則

4 エフェクト列
エフェクトの見積りアルゴリズムで用いるエフェ
クト列について述べる．エフェクト列は，評価規則で用いたイベントトレースの見積りである．
エフェクト列は，構文的にはイベントトレースを拡張したものであり，イベントトレースで表すことができるものはエフェクト列でも表すことができる．

定理 3.1 ` c : A!∆ ならば，以下のいずれかが成り

4. 1 エフェクト列の構文

立つ．

エフェクト列の構文を図 4 に示す．⊥ は見積りア• c = return v であり，` v : A である．
′

• c = op(v; y.c ) であり，op ∈ ∆ である′′′

ルゴリズムの中で使用されるものであり，見積もったエフェクト列には現れないものである．ϵ は純粋であ• c, η ⇝ c , η であり，` c : A!∆ である．

ること，つまり空のエフェクト列であることを示して

なお，本論文で扱う言語と Pretnar [6] の言語とのいる．opji は未ハンドルのオペレーションを表してお違いとして，評価規則にイベントトレースが含まれり，op✓i はハンドル済みのオペレーションを表してている部分が異なるが，型情報にはイベントトレー

いる．肩の部分についている添え字は，プログラム中

スは含まれないため，対象言語の型システムとして，の op を一意に識別するものであり，エフェクト列のPretnar [6] の型システムを用いる．

見積りアルゴリズムの際に使用する．ここでの一意とは，プログラム中で同名のオペレーション呼び出しがあった場合でも，プログラム中の位置が異なる場合

δ

::=

a, b, c, d

エフェクト変数

|

⊥

ボトム

|

ϵ

純粋

|

opji

未ハンドルオペレーション

|

op✓
i

ハンドル済みオペレーション|

δ1 ;δ2連結|δ1 |δ2

非決定的選択|a→s

エフェクト関数|

opshs ::= (δ1 ,δ2 ,Σ)エフェクト状態⊔
Σ ::= { j : {x ▷ a, k ▷ b → s}}hops ::= {return : (a, s),⊔op∈ops op : ((a, b, c, cd), s)}

ハンドラ
図4

エフェクト列の構文

は，それぞれ明確に区別するという意味である．また，δ;δ ，δ|δ はそれぞれ，連結と非決定的選択を表しており，非決定的選択よりも連結の方が強く結合するδ ≡♠ δ

ϵ; δ ≡♠ δδ; ϵ ≡♠ δ′♠ ′δ1 ≡ δ1δ2 ≡ δ2ものとする．エフェクト関数 a → s は対象言語の関数に対応しており，エフェクト変数 a の中身が具体的なエフェクト列で置き換えられた時に，エフェクト

δ1 ≡ δ1′♠δ1 ; δ2 ≡♠ δ1′ ; δ2′
δ1 ≡♠ δ1′
δ1 ≡ δ1′δ1 ; opji ; δ2 ≡ δ1′

状態 s を返すものである．
エフェクト状態 s は (δ, δ, Σ) の 3 つ組からなる．１

図5

δ1 ≡ δ1′δ1 ; a; δ2 ≡ δ1′

エフェクト列の同値関係

つ目の δ はそのコンピュテーションで発生するエフェ
クト列を表しており，2 つ目の δ は，そのコンピュ

4. 2 エフェクト列の同値関係

テーションでリターンされる値が持っているエフェエフェクト列の同値関係を図 5 に示す．≡ は弱い

クト列を表している．Σ はオペレーションの引数と同値関係であり，≡♠ は強い同値関係である．弱い同

その地点での継続をラベル付けしているレコードで値関係は強い同値関係を含む．エフェクト列中に出jてくる ϵ は，読み飛ばしても強い同値と定義する．まある．ここのラベルは，op の添え時 j に対応する．
ハンドラ hops

は，レコードになっており，キーをた，未ハンドルオペレーション op とエフェクト変数

return，および，ハンドラに含まれる各オペレーショ

a が表れた際には，その直前までのエフェクト列が弱ン op としている．キーに対応する中身は，キーがい同値であれば，弱い同値と定義する．

return の時は，1 個のエフェクト変数とエフェクト✓✓
例えば，δ1 = op✓
1 ; ϵ; op2 ，δ2 = op1 ✓; op2 の時，状態のペアになっており，キーが op の時は，4 個の1✓
δ1 ≡ δ2 である．他に，δ1′ = op✓
1 ; op3 ; op2 とする．

エフェクト変数とエフェクト状態のペアになっていこれは，ハンドル済みエフェクトの中に，op13 というる．また，ops はそのハンドラで補足することのでき

未ハンドルエフェクトが含まれている．δ1′ 6≡ δ2 であるオペレーションの集合である．

′♠✓
り，δ1′ ≡ op✓
1 であるが，δ1 6≡ op1 である．

また，見積りアルゴリズムで対象言語からエフェク
ト列を見積もると，対象言語での値はエフェクト列では δ に対応し，ハンドラは hops，コンピュテーショ

ンは s にそれぞれ対応している．

4. 3 エフェクト列の順序関係
エフェクト列同士の順序関係 v を定義する．この順序関係は，左辺のエフェクト列が，右辺に含まれるかを確かめるものである．この順序関係は op✓ に焦点を当てている．先頭からの op✓ のエフェクト列が左辺と右辺で一致している場合にこの順序関係を満δ ≡♠ δ ′
δ v♠ δ ′′δ ≡♠ δ ′δ v δ′δ≡δ
δ v δ′
δ1 v δ1′(LHS)(δ1 |δ2 ) v δ1′
δ1 v δ1′(RHS)
δ1 v (δ1′ |δ2′ )δ1 v δ1′
δ2 v δ2′(CONCAT)′δ1 ; δ2 v δ1 ; δ2′
図6エフェクト列の順序関係

δ v♠ δ ′diﬀ (δ, δ ′ ) = ϵδ2 v♠ δ2′
diﬀ (δ1 ; δ2 , δ2′ ) = δ1δ2 v♠ δ2′
diﬀ (δ2 , δ1′ ; δ2′ ) = δ1′δ2 v♠ δ2′
diﬀ (δ1 ; δ2 , δ1′ ; δ2′ ) = diﬀ (δ1 , δ1′ )ルールにも当てはまらなかった場合は，δ1 を返す．
例えば，δ1 = op✓
1 ; op2 ; ϵ と δ2 = op2 ; ϵ について，

diﬀ (δ1 , δ2 ) を適用した結果は，op✓1 になる．
4. 5 イベントトレースの見積りにおけるエフェク
ト列の意味
イベントトレースの見積りを行って得られたエフェ
クト列が，それぞれどのような意味を持つのかについて述べる．本節では，直感的な説明を行い，詳細な見積りアルゴリズムについては 5 節で述べる．
例 4.1
def

h = handler{return x 7→ return x
read( ; k) 7→ k ‘Bob‘
write(x; k) 7→ k ()}def

c = do name ← read() indo ← write(name) inreturn name
この定義のもとで，with h handle c のイベントト
レースを見積もったエフェクト列は，read✓ ; write✓

図7

エフェクト列の差分抽出

たす．図 6 はエフェクト列の順序関係の定義である．
順序関係も同値関係と同様，弱い順序関係と強い順序関係が存在する．2 つの違いは，前提の同値関係が弱いか強いかである．
✓✓✓
例えば，δ1 = op✓
1 ; op2 ，δ2 = op1 ; (op2 |ϵ) の時，✓
δ1 v δ2 は成り立つ．また，δ3 = op✓
1 ; (op2 |op3 ) と✓した時，op✓1 v δ3 も成り立つ．なぜなら，op1 6≡
✓
✓
✓
op✓
1 ; op2 であるが，op1 ≡ op1 ; op3 が成り立つためである．
イベントトレースはエフェクト列の部分集合であるため，エフェクト列上の二項関係 v はイベントト
レースとエフェクト列を比較することにも使用することができる．この順序関係は 5. 2 節でのアルゴリ
ズムの健全性を示す際に用いる．

となる．✓ がついているエフェクトはハンドル済みのエフェクトを表している．c で発生したエフェクトがハンドラ h で捕捉されるためである．このエフェ
クト列を見ると，このプログラムが，どのようなエフェクトの発生順序になる可能性があるかを確かめることができる．
一方，ハンドラで包まない c のイベントトレースを見積もったエフェクト列は read; write となる．上述のプログラムとの違いは，c の外側のハンドラの有無である．ハンドラがない c のエフェクト列は，未ハ
ンドルオペレーションの列となる．c を実際に評価した場合はエフェクト read が発生した地点で評価が止まってしまうため，実際のイベントトレースは ϵ となる．しかし，エフェクト列を構築する際には，川俣らの手法 [8] と同様に，ハンドルされないオペレーショ
ンは仮想的にハンドルされると見做す．この時，仮想

4. 4 エフェクト列の差分抽出
エフェクト列の差分抽出関数を図 7 に示す．この関数は，後方から二つのエフェクト列がマッチする部
分を取り除くものである．また，diﬀ (δ1 , δ1′ ) がどの的にハンドルされるとは，ただ継続を再開するハンドラによってハンドルされることを意味する．つまり，ハンドラがない場合にオペレーション呼び出し以降のイベントトレースを見積もらないのではなく，仮想的にハンドルされたと見做して見積る．このように，

opi の肩の部分 i，キーに対応する中身にハンドラに

未ハンドルオペレーションを含むエフェクト列を見渡す引数と，継続の情報を記録する．opi の肩の部分

ると，このプログラム中でハンドルされていないエi は常にフレッシュなものになっている．

フェクトを確認することができる．

次に，handler を見積もる (R-HANDLER) について説明する．handler は return 節とハンドラが持つ

5 見積りアルゴリズム

各 op 節からなる．return 節は，with h handle c の正しく型付けされたプログラムから，イベントトc で return された値を受け取り cr の評価を行う．各レースの見積りであるエフェクト列を生成するアルop 節は，c で発生した op 呼び出しの時の引数と継続

ゴリズムについて述べる．また，本アルゴリズムの健を受け取り cop の評価を行う．hops はレコードであ全性についても議論する．

り，キーを return と各 op とし，キーに対応する中身をハンドラに渡す引数や継続などを一時的にエフェ

5. 1 見積りアルゴリズム

クト変数で置いた時のエフェクト変数と，評価を行う

エフェクト列の見積りアルゴリズムを図 8 に示す．

コンピュテーションのエフェクト状態をペアにした

また，図 9 はハンドラ部分の見積りアルゴリズムを示している．

ものとする．
ハンドラ部分の見積りは，エフェクト列のパターン

エフェクト列の見積りアルゴリズムは，エフェクト

マッチによって処理を変える．エフェクト列が単体

環境 K ，項，エフェクト列の 3 つ組で表される．エ(エフェクト列の末尾) の場合は，return 節の部分のフェクト環境 K は，変数とそれに対応するエフェク

エフェクト列を末尾に加える．エフェクト列が連結ト列のペアの集合である．

の場合に，先頭がハンドルできる op の場合は，ハン

また，ハンドラ部分の見積りアルゴリズムはエフェ

ドラ hops の op 節の部分を取り出しエフェクト列をクト集合 Σ，ハンドラ H ，エフェクト列とリターン

op の直後につける．ハンドルされた際の継続は Σ かエフェクトのペア (δ1 , δ2 )，エフェクト状態 s の 4 つら取り出して利用する．

組からなる．

ハンドラ部分の見積りで出てくる関数 ρ, σ, ι はそ

値のエフェクト列は純粋 ϵ または，エフェクト関数a → s である．コンピュテーションはエフェクト状
態 s，ハンドラはハンドラ hops

れぞれ，return 節の見積り関数，op 節の見積り関数，
レコードのフィールド参照関数である．

である．また，本ア

例えば，例 4.1 の条件のもとで，with h handle c

ルゴリズム中で出てくる ∪ に関しては，レコードのに対して，本アルゴリズムを適用する．アルゴリズ

拡張を意味する．

✓
ムを適用した結果のエフェクト列は op✓
read ; opwrite

op 呼び出しを見積もる，(R-OP) について説明する．

となる．アルゴリズムは，(R-HANDLING) を適用し，(E-HANDLINGINOP) からわかるように，op(v; y.c) のh に対して (R-HANDLER)，c に対して (R-SEQOP)v はハンドラに渡す引数であり，y はハンドラが継続

を 適 用 す る ．h に 対 し て (R-HANDLER) を 適 用を再開するときにハンドラから渡される引数であり，し た 結 果 は ，hops = {return ▷ (ϵ, A, ∅), read ▷c は継続が再開された後に行われる処理である．このKread [ϵ/Bread ], write ▷ Kwrite [ϵ/Bwdrite ]}(ops =コンピュテーションで発生するエフェクト列は，op と{ read, write}) となる．c に対して (R-SEQOP) をc で発生するエフェクト列 Ct を連結させた，opi ; Ct

適用した結果は (op0read ; op1write , ϵ, Σ) となる．尚，となる．これは，ハンドラがない状況では，op 呼び

Σ = {0 : {x ▷ ϵ, k ▷ ϵ → (op1write , ϵ, Σ′ )}} ∪ Σ′

出しは継続を単に再開するだけの仮想的なハンドラ(Σ′ = {1 : {x ▷ ϵ, k ▷ ϵ → (ϵ, ϵ, ∅)}})．こ こ でに捕捉されると見做すためである．また，外側にハン得られたエフェクト列をハンドラ部分の詳細なドラが存在した時，詳細に見積もるための情報を Σエフェクト列の見積り ▶ によって詳細なエフェに記録しておく．記録する情報は，レコードでキーをクト列を算出する．Σ, hops , ((op0read ; op1write , ϵ)) ▶

x▷A∈K(R-VAR)K ` x ▷ A

K ` true ▷ ϵ

K , x ▷ a ` c ▷ (At , Ar , Σ)
(R-FUN)K ` fun x 7→ c ▷ a → (At , Ar , Σ)

(R-TRUE)K ` false ▷ ϵ(R-FALSE)

K ` v ▷ A
(R-RETURN)
K ` return v ▷ (ϵ, A, ϕ)K ` c1 ▷ (At , Ar , Σa )K , x ▷ Ar ` c2 ▷ (Bt , Br , Σb )(R-SEQ)K ` do x ← c1 in c2 ▷ (At ; Bt , Br , Σa ∪ Σb )K ` c1 ▷ (At , Ar , Σa )K ` c2 ▷ (Bt , Br , Σb )(R-IF)K ` if v then c1 else c2 ▷ (At |Bt , Ar |Br , Σa ∪ Σb )K ` op(v; y.do x ← c1 in c2 ) ▷ (At , Ar , Σ)
(R-SEQOP)K ` do x ← op(v; y.c1 ) in c2 ▷ (At , Ar , Σ)K ` v1 ▷ a → (At , Ar , Σ)K ` v2 ▷ B(R-APP)K ` v1 v2 ▷ (At , Ar , Σ)[B/a]K ` v ▷ A

K , y ▷ b ` c ▷ (Ct , Cr , Σ)K ` op(v; y.c) ▷ (op ; Ct , Cr , {i : {x ▷ A, k ▷ b → (Ct , Cr , Σ)}} ∪ Σ))i

K ` v ▷ hops

(R-OP)

K ` c ▷ (At , Ar , Σa )
Σa , hops , (At , Ar ) ▶ (Bt , Br , Σb )(R-HANDLING)
K ` with v handle c ▷ (Bt , Br , Σb )∀op ∈ ops[ K , x ▷ aop , k ▷ bop → (copt , copr , ∅) ` cop ▷ (Copt , Copr , Σop )]K , x ▷ aret ` cr ▷ (Crett , Cretr , Σret )⊔hops = {return : (aret , (Ct , Cr , Σret )), op∈ops op : ((aop , bop , copt , copr ), (Copt , Copr , Σop ))}K ` handler {return x 7→ cr , op1 (x; k) 7→ cop1 , . . . , opn (x; k) 7→ copn } ▷ hops
図8

(R-HANDLER)

エフェクト列の見積り✓(op✓read ; opwrite , ϵ, Σ) となり，with h handle c に対件付きで，付録の補題を組み合わせることで証明がで✓して本アルゴリズムを適用した結果は op✓
read ; opwrite

きると予測している．これらの完全な証明に関してとなる．

は今後の課題とする．

5. 2 アルゴリズムの健全性

定理 5.1 c, η ⇝ c′ , η ′ かつ K ` c ▷ (Ct , Cr , Σ) かつ

本アルゴリズムで見積もられるエフェクト列は，実K ` c′ ▷ (Ct′ , Cr′ , Σ′ ) ならば η ′ v η; diﬀ (Ct , Ct′ )際に評価した時のイベントトレースを包含していることを示すことによって，本アルゴリズムの健全性を示

補題 5.1 c, η ⇝∗ c′ , η ′ かつ K ` c ▷ (Ct , Cr , Σ) かつ

すことができる．また，本アルゴリズムで導出されたK ` c′ ▷ (Ct′ , Cr′ , Σ′ ) ならば Ct′ 6= op✓ ; (∗)

未ハンドルオペレーションの集合は，型システム (エフェクトシステム) の未ハンドルエフェクトの集合の定理 5.2 c, η ⇝∗ c′ , η ′ かつ K ` c ▷ (Ct , Cr , Σ) なら部分集合になっていることを示すことで，エフェクトば η ′ v η; Ct )システムで保証されている性質を本アルゴリズムが出力するエフェクト列が満たすことを示す．

定理 5.1 によって，ワンステップの評価でのエフェ
クト列が正しいことが保証される．また，定理 3.1(型尚，これらの定理の証明については，(E-SEQOP)安全性) から補題 5.1 が導かれる．補題 5.1 は評価がと (E-HANDLINGOUTOP) のルールを適用できない条

停止した時のエフェクト列にハンドル済みエフェク

(δ, A′ , Σret ) = ρ(A, hops , Σ)
Σ, h

ops

(H-EPSILON), (ϵ, A) ▶ (ϵ; δ, A′ , Σ ∪ Σret )(δ, A′ , Σret ) = ρ(A, hops , Σ)Σ, hops , (op✓ , A) ▶ (op✓ ; δ, A′ , Σ ∪ Σret ))(δ, A′ , Σret ) = ρ(A, hops , Σ)
Σ, h

ops

(op ∈
/ ops)′, (op, A) ▶ (op; δ, A , Σ ∪ Σret )((copt , copr ), (δ, A′ , Σop ), (Ct , Cr )) = σ(op, hops , Σ)
Σ, h

ops

✓

′

′′

ops

(op ∈
/ ops)′, (op; δ, A) ▶ (op; δ , A′ , Σ′ )((copt , copr ), (δ ′ , A′ , Σop ), (Ct , Cr )) = σ(op, hops , Σ)
✓

Σ, h

′

(H-OPI)(H-SEQOPO)

Σ, hops , (Ct , Cr ) ▶ (δ ′′ , A′′ , Σ′ )(op ∈ ops)

, (op; δ, A) ▶ (op ; δ , A , Σ ∪ Σop )[δ ′′ /copt , A′′ /copr ]Σ, hops , (δ1 , A1 ) ▶ (δ1′ , A′1 , Σ′1 )ops(op ∈ ops)′′

, (op, A) ▶ (op ; δ, A , Σ ∪ Σop )[(δ /copt , A /copr ]

Σ, h

Σ, h

(H-OPO)Σ, hops , (Ct , Cr ) ▶ (δ ′ , A′′ , Σ′ )Σ, hops , (δ, A) ▶ (δ ′ , A′ , Σ′ )ops

(H-OPCHECK)′Σ, hops , (δ2 , A2 ) ▶ (δ2′ , A′2 , Σ′2 ), (δ1 |δ2 , A1 |A2 ) ▶ (δ1′ |δ2′ , A′1 |A′2 , Σ′1 ∪ Σ′2 )Σ, hops , (δ1 , ⊥) ▶ (δ1′ , ⊥, Σ′1 )
Σ, h

ops

Σ, hops , (δ2 , A) ▶ (δ2′ , A′ , Σ′2 ), (δ1 ; δ2 , A) ▶

(H-SEQOPI)(H-NONDTERMINISTIC)(δ1 6= op)(δ1′ ; δ2′ , A′ , Σ′1 ∪ Σ′2 )(H-SEQ)

ρ(A, hops , Σ) =if A = ⊥ then ⊥else let (aret , (Crett , Cretr , Σret )) = ι(return, hops ) in
(Crett , Cretr , Σret )[A/aret ]σ(opi , hops , Σ) =let ((aop , bop , copt , copr ), (Copt , Copr , Σop )) = ι(op, hops ) in
let {x ▷ A, k ▷ b → (Ct , Cr , Σ′op )} = ι(i, Σ) in((copt , copr ), (Copt , Copr , Σop )[A/aop ], (Ct , Cr )[bop /b])ι(ΓΓ, S) = let {key : body} ∪ S ′ = S ′ inbody
図9

ハンドラ部分の見積り

トから始まるエフェクト列が現れないことが保証さ

また，型情報に含まれるエフェクトの集合 K に対れる．そのため，定理 5.1 と補題 5.1 から定理 5.2 がして，エフェクト列の中の未ハンドルエフェクトの集示され，健全性が証明される．

合が K の部分集合になっていることを示す．なお，
関数 unHandleOp はエフェクト列から，そこに含ま定理 5.3 ` c : A!∆ かつ K ` c ▷ (At , Ar , Σ) ならば，れる未ハンドルエフェクトの集合を取り出す関数でunHandleOp(At ) ⊆ ∆ある．これは，発生し得ないエフェクトが記録されてベントトレースを見積る †2 と，川俣らの手法 [8] 特いることはないことを示している．

有の opdum を除いて，12 パターン出現することとな
り，本アルゴリズムよりも false positive が多くなる．

5. 3 アルゴリズムの実装と評価
本アルゴリズムの実装は OCaml にて行なっている．また，対象言語のインタープリタに関しても実装

6 関連研究を行なっており，いずれも GitHub 上で公開してい本論文では，Pretnar の代数的エフェクトの体系 [6]る．本アルゴリズムを実際に実行した例を 2 節の例をもとにしている．これは，実行時に発生しうるエを用いて示す．

フェクトの情報を型情報に集合として定義したものである．型情報に含まれた集合は未ハンドルオペレー

h′ = handler{return x 7→ return x,
def

ションで評価が停止した際に，その集合にその未ハン

read( ; k) 7→

ドルオペレーションが必ず含まれていることを型安

do x ← k "Bob" in

全性として保証している．

k x}

川俣ら [8] の手法も同じく大いに参考にしたもので

def

c = do name1 ← read() in

ある．この手法は本論文と同じく Pretnar の代数的

do name2 ← read() inエフェクトの体系 [6] をもとにしているが，ディープ

return name1ˆname2
本アルゴリズムで with h′ handle c のエフェハンドラではなくシャローハンドラを採用しており，

ク ト 列 を 見 積 る と read✓ ; read✓ ; read✓ と な る ．

with h′ handle c, ϵ から始め，評価が停止した時の実際のイベントトレースも read✓ ; read✓ ; read✓となり，見積もったエフェクト列と一致する．

再帰関数が扱える点が異なる．また，イベントトレー
スを用いた評価規則も同じである．この手法では，型情報にエフェクトの時間的情報をトレースエフェク
トとして埋め込んでいる．エフェクトの時間的な情報をトレースエフェクトの集合で表している．本論

他にも以下のような例を考える．

文の手法では，エフェクトをグラフとして表している
ため，その部分が異なる．また，ハンドラにエフェク′ def

c = if v thendo name1 ← read() inトがハンドルされた際の false positive が多くなるの

do name2 ← read() inに対して，本論文の手法ではハンドラ部分を詳細に見return name1ˆname2

積もることで false positive を少なくしている．
他に継続などを用いてコントロールフローを変else

えるものに対して時間的な情報を扱う手法として

do ← write("Bob") in

Gordon の sequential eﬀects [2] や，Sekiyama らの

do name ← read() inreturn name
本アルゴリズムで with h′ handle c′ のエフェク
✓

✓

✓

✓

ト列を見積ると read ; read ; read |write; read′

AEW(Answer Eﬀect Modiﬁcation) に対応した時間的情報を扱えるエフェクトシステム [7] がある．前者は，タグ付き限定継続演算子を持つ体系における′となる．with h handle c , ϵ から始め，評価が停止

エフェクトの順序の見積りを行っている．後者は，した時の実際のイベントトレースは，v が true の時，shift0/reset0 の体系において依存型を用いて ﬂow

read✓ ; read✓ ; read✓ となり，v が false の時，write

sensitive なエフェクトの順序の見積りを行っている．

の部分で評価が停止するが，write がただ継続を再開

また，エフェクトの順序を無限と有限を分けて管理し✓すると考えると，write; readとなり，見積もったエフェクト列と一致する．
川俣らの手法 [8] で，同等なプログラムに対してイている．
†2 川俣らの手法 [8] はディープハンドラを扱えないので，
ハンドラ h′ を 3 重にネストさせるようにエンコード
して見積もっている．

7 まとめと今後の課題
本論文では，代数的エフェクトハンドラを持つ言語のプログラムに対して，エフェクトの発生の時間的な見積りを静的に行うアルゴリズムを提案した．ハン
ドラ部分の見積りをより正確に行うことによって，既存手法よりも，false positive の少ない見積りを行う
ことを可能にした．また，提案したアルゴリズムの実
装は GitHub†3 にて公開している．
今後の課題としては，本論文で示した定理の証明がtronic notes in theoretical computer science,Vol. 319(2015), pp. 19–35.
[7] Sekiyama, T. and Unno, H.: Temporal Veriﬁcation with Answer-Eﬀect Modiﬁcation: Dependent Temporal Type-and-Eﬀect System with Delimited Continuations, Proceedings of the ACM on
Programming Languages, Vol. 7, No. POPL(2023),
pp. 2079–2110.
[8] 川俣楓河, 寺内多智弘: 代数的エフェクトハンドラを持つ言語のためのトレースエフェクト, コンピュータ ソ
フトウェア, Vol. 40, No. 2(2023), pp. 19–48.

付録ある．また，対象言語をディープハンドラだけでなく定理 5.1 c, η ⇝ c′ , η ′ かつ K ` c ▷ (Ct , Cr , Σ) かつ

シャローハンドラも含む体系に対しても見積りを行K ` c′ ▷ (Ct′ , Cr′ , Σ′ ) ならば η ′ v η; diﬀ (Ct , Ct′ )えるアルゴリズムを構築すること，再帰を含む体系に証明. 評価規則の構造に関する帰納法．

対しても見積りを行えるアルゴリズムを構築するこ(E-SEQRET の時)とがある．特に，再帰を含む体型に関しては，無限のR-SEQ より，以下が成り立つ．

エフェクト列をどのように表すかという問題がある．

1. c1 = return v

無限の扱いに関しては，有限と無限を分けて管理する

2. K ` v ▷ Ar

方法や，エフェクトの列に対して再帰的な構文を追加

3. K ` c1 ▷ (ϵ, Ar , Σa )する方法などがある．

4. K, x ▷ Ar ` c2 ▷ (Bt , Br , Σb )また，このアルゴリズムを用いた代数的エフェクト
ハンドラを持つ体系に対してのプログラミング支援の応用に関しても今後の課題である．

5. K ` do x ← c1 inc2 ▷ (ϵ; Bt , Br , Σa ∪Σb )また，補題 5.2 より K ` c2 [v/x] ▷Bt である．
さらに，diﬀ (ϵ; Bt , Bt ) = ϵ である．よって，

参 考 文 献[1] Bauer, A. and Pretnar, M.: An eﬀect system foralgebraic eﬀects and handlers, Logical methods incomputer science, Vol. 10(2014).
[2] Gordon, C. S.: Lifting sequential eﬀects to control
operators, 34th European Conference on ObjectOriented Programming (ECOOP 2020), Schloss
Dagstuhl-Leibniz-Zentrum für Informatik, 2020.
[3] Hillerström, D. and Lindley, S.: Shallow eﬀect
handlers, Programming Languages and Systems:
16th Asian Symposium, APLAS 2018, Wellington,
New Zealand, December 2–6, 2018, Proceedings 16,
Springer, 2018, pp. 415–435.
[4] Plotkin, G. and Power, J.: Algebraic operations
and generic eﬀects, Applied categorical structures,Vol. 11(2003), pp. 69–94.
[5] Plotkin, G. and Pretnar, M.: Handlers of algebraic eﬀects, European Symposium on Programming, Springer, 2009, pp. 80–94.
[6] Pretnar, M.: An introduction to algebraic effects and handlers. invited tutorial paper, Elec-η v η; ϵ となり成り立つ．
(E-APP)(E-IFTRUE)(E-IFFALSE) も同様に成り立つ．
(E-SEQ の時)
R-SEQ より，以下が成り立つ．
1. K ` c1 ▷ (At , Ar , Σa )2. K, x ▷ Ar ` c2 ▷ (Bt , Br , Σb )3. K ` do x ← c1 inc2 ▷(At ; Bt , Br , Σa ∪Σb )1. K ` c′1 ▷ (A′t , A′r , Σ′a )2. K, x ▷ A′r ` c2 ▷ (Bt′ , Br′ , Σb )3. K ` do x ← c1 inc2 ▷(A′t ; Bt , Br , Σ′a ∪Σb )補 題 5.5，補 題 5.6 よ り diﬀ (Bt , Bt′ ) = ϵ
で あ る ．ま た 帰 納 法 の 仮 定 よ り ，η ′ v

η; diﬀ (At , A′t ) が成り立つ．よって，η ′ v
η; diﬀ (At ; Bt , A′t ; Bt′ ) が成り立つ．

†3 https://github.com/zaki5m/effect_analyzer

図 10型システム ( [6] の Fig.6)

8. Σc , H, (opi ; Ct′ ; , Cr′ ) ▶ (op✓ ; Copt , Copr , Σc ∪(E-HANDLING) も同様に成り立つ．

Σop )[A/Aop , (δ ′′ , A′′ , Σ′′ )/Kop ](E-HANDLINGRET の時)
R-HANDLING より，以下が成り立つ．

9. K

`

with

h

handlec ▷✓1. c = return v(op ; Copt , Copr , Σa ∪Σop )[Ar /A, Bop /B,

2. K ` v ▷ Ar

(δ ′′ , A′′ , Σ′′ )/Kop ]3. K ` c ▷ (ϵ, Ar , Σa )また，
K ` cj [v/x, fun y 7→ handle h with c]▷

4. Σa , H, (ϵ, Ar ) ▶ (ϵ; Crett , Cretr , Σa ∪(Copt , Copr , Σret )[Ar /A, Bop /B, (δ ′′ , A′′ , Σ′′ )/Kop ]で あ る ．さ ら に ，diﬀ (op✓ ; Copt , Copt ) =Σr et)[Ar /A]
5. K

`

with

h

handlec ▷(Crett , Cretr , Σa ∪ Σr et)[Ar /A]

op✓ である．よって，η; op✓ v η; op✓ となり成り立つ．

また，K ` cr [v/x]▷(Crett , Cretr , Σr et)[Ar /A]
である．さらに，
diﬀ (ϵ; Crett [Ar /A], Crett [Ar /A]) =ϵ である．よって，η v η; ϵ となり成り立つ．
(E-HANDLINGINOP の時)(c = return v の時)

1. c = op(v; y.c′ )R-RETURN より，K ` return v ▷ (ϵ, A, Σ)．

2. K ` v ▷ A
3. K ` c

unHandleOp(ϵ) = ∅ である．∅ ⊆ ∆ よっ

▷ (Ct′ , Cr′ , Σc′ )て満たす．

4. K, y ▷ B ` c ▷ (Ct′ ; , Cr′ , Σc′ )
5. Σc

=

{i

unHandleOp(At ) ⊆ ∆証明. 型の構造に関する帰納法．

R-HANDLING より，以下が成り立つ．

′

定理 5.2 ` c : A!∆ かつ K ` c ▷ (At , Ar , Σ) ならば，:{x ▷ A, k ▷ B(Ct′ ; , Cr′ , Σc′ )}} ∪ Σc′
6. K ` c ▷ (opi ; Ct′ ; , Cr′ , Σc )7. Σc′ , H, (Ct′ , Cr′ ) ▶ (δ ′′ , A′′ , Σ′′ )→(c = op(v; y.c′ ) の時)
R-OP より，K ` op(v; y.c′ ) ▷ (op; Ct , Cr , Σ)
か つ K ` c′ ▷ (Ct , Cr , Σ) で あ る ．仮 定
よ り ，Γ ` c′ : A!∆ か つ op ∈ ∆ か つば K ` c[v/x] ▷ (Ct , Cr , Σ)

unHandleOp(Ct ) ⊆ ∆ で あ る ．な の で ，unHandleOp(op; Ct ) ⊆ ∆ よって満たす．
(c = handle h with c′ ) の時)
R-HANDLING より，K ` c′ ▷ (Ct′ , Cr′ , Σ) かつ Γ ` c′ ▷ A!∆ かつ unHandleOp(Ct′ ) ⊆ ∆である．なので，unHandleOp(op; Ct ) ⊆ ∆証明. アルゴリズムの構造に関する帰納法．
補題 5.3 K, x ▷ A ` c : (Ct , Cr , Σ) かつ K, x ▷ A′ `c : (Ct , Cr , Σ) かつ A′ v♠ A ならば Cr′ v♠ Cr
未解決

よって満たす．
補題 5.4 c, η ⇝ c′ , η ′ かつ K ` c ▷ (Ct , Cr , Σ) かつ
補題 5.1 c, η ⇝∗ c′ , η ′ かつ K ` c ▷ (Ct , Cr , Σ) かつ

K ` c′ ▷ (Ct′ , Cr′ , Σ′ ) ならば Ct′ 6= op✓ ; (∗)
証明. 型 安 全 性 よ り ，c の 評 価 が 停 止 す る と きK ` c′ ▷ (Ct′ , Cr′ , Σ′ ) ならば Cr′ v♠ Cr である．
証明. 補題 5.3 を用いて，評価規則の構造に関する帰納法．

c = return v または，c = op(v; y.c′ ) のいずれか

補題 5.5 K, x ▷ A ` c ▷ (Ct , Cr , Σ) かつ K, x ▷ A′ `である．(c = return v のとき)c ▷ (Ct′ , Cr′ , Σ′ ) かつ A′ v♠ A ならば Ct′ v♠ Ct で

R-RETURN より，K ` return v ▷ (ϵ, A, Σ)
ϵ 6= op✓ ; (∗) である．よって成り立つ．
(c = op(v; y.c′ ) のとき)K ` op(v; y.c′ ) ▷ (op; At , Ar , Σ)
op; At 6= op✓ ; (∗) である．よって成り立つ．
補題 5.2• K, x ▷ A ` u ▷ B か つ K ` v ▷ A な ら ばK ` u[v/x] ▷ B• K, x ▷ A ` c ▷ (Ct , Cr , Σ) かつ K ` v ▷ A ならある．
証明. アルゴリズムの構造に関する帰納法．
補 題 5.6 Σ, hops , (δ, A)
′

Σ ,h

ops

′

′

, (δ , A ) ▶

▶

(Ct , Cr , Σa ) か つ(Ct′ , Cr′ , Σ′a ) かつ δ ′v♠ δ かつA′ v♠ A ならば，Ct′ v♠ Ct かつ Cr′ v♠ Cr である．
証明. δ ′ v♠ δ ，A′ v♠ A に関する構造帰納法