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

エフェクトハンドラを用いた型安全なコード生成
礒田 華成

亀山 幸義

代数的エフェクトおよびエフェクトハンドラは，様々な計算効果を統一的かつモジュラーに扱うための言語機能であり，コード生成の文脈においても，let-insertion などを表現することができ，有用であると考えられる．先行研究において，可変セルなどのある種の言語機能は，コード生成と組み合わせたとき，生成されるコード中の変数がスコープ逸脱を起こす場合があることが知られており，エフェクトハンドラにおいても同様の問題が発生し得る．本研究では，エフェクトハンドラを利用したコード生成のための 2 段階の計算体系と型システムを提案する．Kiselyov らが提案した，生成されるコードに含まれる自由変数の集合を追跡するための手法である reﬁned environment classiﬁerに基づき，ハンドラを未来のステージの変数の束縛子として取り扱う．型システムの健全性に加え，生成されたコードがスコープ逸脱を起こすことがないことを示した．

let のような下線つきの構文は，評価されると対応

1 研究の背景と目的するコードを生成する演算子である．生成された式

代数的エフェクトとエフェクトハンドラ [4] は，プ

M のコードは hM i と書く．この例では，生成されログラムにおける様々な計算効果を統一的かつモジュたコードに式 M が重複して出現することを防ぐためラーに扱うための言語機能であり，コード生成においに，ins というオペレーションによって M を一度変ても有用な利用例が考えられる．図 1 に示すのは，生数 y に束縛するというコードを生成している．

成されるコードの重複を防ぐための let-insertion とよばれる手法を表現する例である．

他方で，可変セル [2] や限定継続演算子 [3] のように，式の位置を自由に移動させることのできる言語機
能は，コード生成と組み合わせたとき，変数のスコー

Hid := {return x 7→ return x}

プ逸脱を引き起こすことが知られており，図 2 に示す

Hins := {ins x k 7→ let y ← return x in throw k y}

ように，エフェクトハンドラにおいても同様の問題が発生し得る．

with Hid ] Hins handle
let x ← do ins hM i in x + x

λx. with Hid ] Hins handle∗⇝ hlet y ← M in y + yi

let z ← do ins hreturn xi in return z∗⇝ hlet y ← return x′ in return λx′ . return yi
図1

エフェクトハンドラによる let-insertion の例
図2

エフェクトハンドラによるスコープ逸脱の例∗ Type-Safe Code Generation with Eﬀect Handlers.

This is an unrefereed paper. Copyrights belong tothe Authors.
Kanaru Isoda, Yukiyoshi Kameyama, 筑波大学 情報理
工学位プログラム, Department of Computer Science,
University of Tsukuba.

オペレーション ins の呼び出しの引数 hreturn xi は，with-handle 式の外側で束縛された変数 x を含んでいる．オペレーション呼び出しによって with-handle式の直前の位置に let が挿入されるため，生成されたを追加し，REC に，classiﬁer 同士の join をとることコードでスコープ逸脱が起きている．
本研究では，エフェクトハンドラを用いて型安全なのできる構造を導入した型システムを提案した [3]．

コード生成を実現できるようにすることを目的とし，エフェクトハンドラを含む型安全な多段階計算の体系

3 提案する計算体系と型システムを提案する．

本研究で提案する，エフェクトハンドラを含む 2 段

本稿は，GPCE 2024 で発表予定の内容 [1] を日本

階の計算体系の型システムの概観を述べる．計算体系に関しては，およそ <NJ> にエフェクトハンドラを加語でまとめたものである．

えた体系になっており，型システムに関しては，先述

2 先行研究した大石と亀山の先行研究 [3] に基づいている．ただTaha と Nielsen は，environment classiﬁers とよし，エフェクトハンドラの取り扱いに関しては特記す

ばれる手法に基づき，生成されたコードを実行するるべき点があるため，以下で議論する．

演算子である run を含む型安全な多段階計算体系 λα3. 1 エフェクトハンドラの取り扱いを提案した [5]．

Kiselyov らによる，可変セルを含む型安全な 2 段

オペレーションの呼び出し，および対応するハン階の計算体系 <NJ> [2] では，この手法を元にしたドラの実行によって，図 4 に示すように with-handle

reﬁned environment classiﬁers (REC) とよばれる新式の外側に未来のステージの変数の新しい束縛が生たな手法を提案し，生成されるコードに含まれ得るじる場合がある．

自由変数の集合を型システムで追跡することで，スコープ逸脱が起きないことを静的に保証している．

with Hid ] Hins handle do ins h1i<NJ> では，型 τ のコードを表す型は hτ iγ と書かれ，⇝ let y ← return h1i in throw k y

式に含まれ得る未来のステージの変数の集合を表す

where k = κz. with Hid ] Hins handle return zclassiﬁer γ の注釈がついている．図 3 に示すのは，ラムダ抽象を生成する式 λx. M の型付け規則である (構図4with-handle 式が束縛子として振る舞う例

文は提案体系と合わせているため一部異なっている部分がある)．

そのため，型システムにおいて with-handle 式は未来のステージの変数の束縛子と同様の扱いを受ける．

γ ∈∆]Γ

図 5 に示すのは with-handle 式の型付け規則である．

γ1 ∈/ ∆]Γ1 γ11 γ1∆; Γ, γ1 , (γ1  γ), (x : hA i ) ` M : hB i∆; Γ ` λx. M : hA1 → B 1 i
図3γ<NJ> における式 λx. M の型付け規則γ ∈∆]Γγ1 ∈/ ∆]Γ∆; Γ ` H : ∀υ. hA i ! E ⇒ hB 1 i ! E ′1 υυ

1 γ1∆; Γ, γ1 , (γ1  γ) ` M : hA i! E[γ1 /υ]∆; Γ ` with H handle M : hB i ! E ′ [γ/υ]1 γ

この式は，評価されると未来のステージの新しい変数を導入するため，型付けの際に，型環境に新しい

図5

with-handle 式の型付け規則

classiﬁer γ1 と，γ1 が現在の classiﬁer γ より深いスコープで導入されたことを表す，classiﬁer 同士の部

図 3 で見た，未来のステージの変数を新しく導入

分型関係 γ1  γ を追加する．この仕組みによって，する式である λx. M と同様に，with-handle 式の型スコープ逸脱を起こし得るコードの型付けを試みる

付けの際に，新しい classiﬁer γ1 を導入し型環境に追と，classiﬁer の不整合によってそれが検出される．

加している．

大石と亀山は，<NJ> に限定継続演算子 shift0/reset0

ハンドラの型は，図 6 に示すように classiﬁer に関する多相性をもち，図 5 で示した with-handle 式の型• 体系や型システムの拡張・変更．生成されたコー付けの際に具体的な classiﬁer によってインスタンスドを実行する演算子 run を追加したり，コード化される．これは，ハンドラが実際に利用されるとき型以外をもつハンドラを書けるような拡張が可能

までハンドラ本体に含まれる式がもつべき classiﬁerであるかどうか，また，classiﬁer に関する多相を決定することができないことに起因している．

性をどの程度導入することができるか検討する．

• 型推論アルゴリズム．Classiﬁer を明示しなけれH = {return x 7→ M } ] {op i x k 7→ Ni }i
E = {op i : Aiop ↠ hBiop i }i ] E ′ ,υ

op1′
Γi′ = (x : Aopi ), (k : hBi i ↣ hB i ! E )υυ1 υ∆; Γ, υ, (x : hA i ) ` M : hB i ! E[]υ∆; Γ, υ, Γi′ ` Ni : hB 1 i ! E ′ i′∆; Γ ` H : ∀υ. hA1 i ! E ⇒ hB 1 i ! E ′υ

図6としてみると煩雑である．これを避けるために型推論がどの程度可能であるか検討する．

参 考 文 献υ∈/ ∆]Γ1 υばならない体系は，実用的なプログラミング言語

υハンドラの型付け規則

3. 2 型システムの健全性提案する型システムが健全であることを，以下の 2つの定理を証明することによって示した．ただし，Γ
は classiﬁer とそれらの部分型関係のみを含む型環境を表す．
定理 1 (進行). ∆; Γ ` M : C ならば，M は正規形
または M ⇝ N ．
定理 2 (主部簡約). ∆; Γ ` M : C かつ M ⇝ N ならば，∆, ∆′ ; Γ ` N : C ．
また，重要な帰結として，生成されたコードがスコープ逸脱を起こさないことを表す以下の系を示した．
系 3. γ; ` M : hA1 i かつ M ⇝∗ return V ならば，γV = hN 1 i かつ γ; `γ N 1 : A1 ．

4 まとめと今後の展望
本研究では，エフェクトハンドラを用いた型安全なコード生成の実現を目的として，エフェクトハンドラを含む型安全な 2 段階の計算体系を提案し，型システムの健全性を証明した．今後の展望を以下に述べる．

[1] Isoda, K., Yokoyama, A., and Kameyama, Y.:
Type-Safe Code Generation with Algebraic Effects and Handlers, Proceedings of the 23rd ACM
SIGPLAN International Conference on Generative
Programming: Concepts and Experiences, GPCE
2024, Pasadena, California, United States, October 21-22, 2024, to appear.
[2] Kiselyov, O., Kameyama, Y., and Sudo, Y.: Reﬁned Environment Classiﬁers - Type- and ScopeSafe Code Generation with Mutable Cells, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, Igarashi, A.(ed.), Lecture Notes in Computer Science, Vol. 10017, 2016,
pp. 271–291.
[3] Oishi, J. and Kameyama, Y.: Staging withcontrol: type-safe multi-stage programming withcontrol operators, Proceedings of the 16th ACM
SIGPLAN International Conference on Generative
Programming: Concepts and Experiences, GPCE
2017, Vancouver, BC, Canada, October 23-24,
2017, Flatt, M. and Erdweg, S.(eds.), ACM, 2017,
pp. 29–40.
[4] Plotkin, G. D. and Pretnar, M.: Handlers of Algebraic Eﬀects, Programming Languages and Systems, 18th European Symposium on Programming,ESOP 2009, Held as Part of the Joint EuropeanConferences on Theory and Practice of Software,ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, Castagna, G.(ed.), Lecture Notes in Computer Science, Vol. 5502, Springer, 2009, pp. 80–94.
[5] Taha, W. and Nielsen, M. F.: Environment classiﬁers, Conference Record of POPL 2003: The 30thSIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, New Orleans, Louisisana,USA, January 15-17, 2003, Aiken, A. and Morrisett, G.(eds.), ACM, 2003, pp. 26–37.