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

代数的エフェクトを持つ 2 段階計算言語の型システム
横山 彪人 亀山 幸義

プログラムを処理対象のデータと見なしてプログラム生成等を行うプログラムをメタプログラムという．メタプログ
ラムの中でも，プログラム生成と生成されたプログラムの実行の段階が明確にわかれ，型システムによりある種の安全性を保証するものに多段階計算言語がある．多段階計算言語では，体系が計算エフェクトを持つ場合の型安全性が大きな課題であり多くの研究がなされてきた．本研究は，さまざまな計算エフェクトを統一的に表現できる，代数的エフェクトを持つ 2 段階計算言語の型システムを構築する．従来研究ではカバーされなかったスコープ逸脱を起こすプログラム例を精密に分析し，エフェクトを扱うハンドラの消去規則が疑似的なスコープを生み出すという考えに基づいて型付け規則を提案した．

えた 2 段階計算言語の型システムの設計を行う．代

1 はじめに数的エフェクト（algebraic eﬀects and handlers ）[6]

プログラム自体をデータとして扱えるようなプロは，計算エフェクト一般を統一的なインターフェース

グラミング技法を一般にメタプログラミングといい，で扱うことのできる言語機構である．代数的エフェ

例えばコード生成分野などで数多くの応用例が存在

クトは近年盛んに研究が行われている研究テーマでする．メタプログラミングの中でも特に多段階計算

あり，OCaml 等の実用言語の新機能としてサポート（multi-stage programming ）は，生成されるコードのされることも発表されている [4]．

型についても詳細な情報をもつ型システムを備えて多段階計算言語の構文は，生成の対象となる言語の

おり，コード生成器のみならず，生成されたコード

構文に，コード生成のためのわずかな構築子を追加しの安全性までも静的に保証することを目指している．

ただけのものであることが多い．これにより，両者の多段階計算言語の初期の型システムが純粋な言語を構文的な違いをさほど意識することなくコード生成器

対象としていたのに対し，近年は、制御エフェクトやを記述することができる．これは多段階計算言語の魅

破壊的代入などの計算エフェクトを持つ言語を対象

力の 1 つである．従って，代数的エフェクトがその有にした研究が行われている．計算エフェクトを持つ

用性によって対象言語にサポートされるならば，メタ

多段階計算体系の設計は，理論的な困難さが増大する言語でもサポートできる体系があることが望ましい．

が，コード複製問題などを回避するコード生成を実現

多段階計算と代数的エフェクトは，それぞれが独できるなど実用性が高い．
本研究では代数的エフェクトという言語機構を備立した体系としてならば型安全な形式化が存在する[2] [7] [8] [9] が，両者を組み合わせた体系として型安全なものは未だ存在しない．これを実現するためには，∗ Typesytem for two-stage programming languagewith algebraic eﬀects and handlers
This is an unrefereed paper. Copyrights belong to
the Authors.
Ayato Yokoyama, Yukiyoshi Kameyama, 筑波大学情報理工学位プログラム, Department of Computer Science, University of Tsukuba.

簡約の途中で変数の束縛関係が崩れてしまうスコー
プ逸脱（scope extrusion ）の問題に対処する必要がある．この問題への対処が本研究のほとんどすべての仕事を占めており，それは代数的エフェクト由来の項であるハンドル式の型付け規則における工夫として

2. 2 多段階計算
x, y, k ∈ Var

本体系の多段階計算の部分のうち，本論文においs, r ∈ ∆て重要な部分について説明する．再び図 1 において，S, R ::= ε | s

N, M は項である．その中で多段階計算のための項は::= {return x 7→ Mr , opi (x; k) 7→ Mi }1≤i≤n▶s M, ◀s M, Λs.M, x s, run x の 5 つである．こN, M ::= x | λx.M | x y | ▶s M | ◀s M | Λs.Mのうち Λs.M, x s, run x はコードの実行とそれを安h| x s | run x | true | false| let x = M in N | if x then N else N| h | with N handle M | op M | throw(k, x)
図1

構文の定義

全に行うための構築子である．
残りの ▶ M, ◀ M †1 について説明する．まずss▶s M の ▶s はブラケット（bracket ）と呼ばれる構築子であり，M のコード †2 を表している．さらにM のステージを 1 つ上げるという意味もつ．一方で表現される．

◀s M の ◀s はエスケイプ（escape ）と呼ばれる構築子であり，M を別のコードに埋め込む †3 ために使わ

2 構文

れる．さらに M のステージを 1 つ下げるという意味

本節では，まず提案する言語の構文を導入する．そを持つ．多段階計算では，このブラケットとエスケイの後，特徴的な構築子に関しては具体例を用いながらプを用いて小さなコード断片から，より大きなコード

その直観や操作的意味を述べる．

を生成する．
具体例を通じて操作的な意味を説明する．まず前提

2. 1 提案言語の構文として，計算体系にはステージという概念があり，項提案言語の構文の定義を図 1 に記す．対象言語の基のステージはブラケット ▶ で 1 上がり，エスケイプ

礎となるのは単純型付きラムダ計算で，それに bool

◀ で 1 下がる．そして，ステージ 0 では通常の β 簡

値や if 式などの単純な拡張と，多段階計算と代数的約等の計算が行われ，ステージ 1 では ◀▶ M −→ M

エフェクトのための構築子がある．このうち多段階計の簡約のみが行われる．例えば
def

算の部分は Tsukada と Igarashi による λ [9] に，代a = ▶ (1 + 2)

数的エフェクトの部分は Kammar らの体系 [2] に基とすると，右辺の項はそれ以上計算が進まない値でづいている．評価規則は値呼び戦略で，エフェクトのある．(1 + 2) はブラケット ▶ の中にあるのでそのス

ハンドラは深いハンドラ（deep handler ）である．

テージは 1 であり，ステージ 1 では ◀▶ M −→ M

構文の定義について説明する．まず最初の x, y, kの計算しか行われないからである．次にエスケイプ▷

は変数である．代数的エフェクトは継続を明示的にを使った計算例を見てみると，例えば
defb = ▶ (◀ a+ ◀ a)扱うので，それを表す変数として k がある．続いて

s, r はステージ変数である．ステージの名前を扱うたとするとめの変数であり，2 段階計算の体系である本体系にお()
b =▶ (◀▶ (1 + 2)) + (◀▶ (1 + 2))

いてはステージのレベルが 1 であることを表す．こである．この時，◀▶ (1 + 2) はステージ 1 にあるの

れらはコードを安全に実行するために必要な変数で，で，◀▶ の解消が行われ，最終的に b は代数的エフェクトによる拡張がなくても必要な要素▶ ((1 + 2) + (1 + 2))である．S, R はステージ変数または ε を表すメタ変という値に計算される．この例には，a という小さな数である．ε はステージ 0 を表す．
†1 それぞれの構築子の添字のステージ変数は，特に記載の必要がない場合は適宜省略する．
†2 MetaOCaml 言語では.<M>. と表される．
†3 MetaOCaml 言語では.~M と表される．

コード断片から b というより大きなコードを生成す

コープ逸脱とは、多段階計算と代数的エフェクトを組る過程が表れている．

み合わせた時にしばしば起こる問題であり，簡約により変数の束縛関係が崩れてしまうことを指す．型シ2. 3 代数的エフェクト

ステムの目的は、このような問題が実行時に起きない

代数的エフェクトについて，本論文において重要なことを静的に保証することである．

部分の説明を行う．代数的エフェクトが実現していまず，スコープ逸脱を起こさない，エフェクトを使っることを非形式的に言えば，限定継続が使える例外処

たコード生成の有用な例を見る．次のような insert

理ということになる．これは次の 3 つにより実現さハンドラを定義する．

れる．すなわちエフェクトの呼び出し，ハンドラ，ハh = { insert(x; k) 7→

def▶ (let y =◀ x in ◀ (k(▶ y))) }ンドル式である．
エフェクトの呼び出し（op M ）は，ユーザーが定義したエフェクト op とその引数からなる．ハンドラ（h）

これは let insertion によってコード共有を可能にするハンドラである．例えば
defはエフェクトが発生した時の振る舞いを定義したもの

sqrS = ▶ (◀ x ∗ ◀ x)である．例えばハンドラの opi (x; k) 7→ Mi は，このというコード生成の関数は，x というコードを複製しハンドラの下でエフェクト opi が発生した場合には，てしまうので生成されたコードの実行性能が悪くなっその引数 x と自身までの限定継続 k を用いて Mi といてしまう．

う計算を行うということを表している．return 節はsqrS (▶ BIG) −→∗ ▶ (BIG ∗ BIG)

エフェクトが発生せずに計算が x で終わった時の振る

ここで BIG は、時間のかかる計算を行うコードある．

舞いを示している．ハンドル式（with N handle M ）insert ハンドラを使うことによって以下のように重複は，ハンドラ N の下で M の評価を行うことを表し，がないコード生成が可能になる．

M の評価中に発生したエフェクトの振る舞いがハン
ドラ N に記されていれば，それに従って評価が進む．
具体的な計算例を示す．今，decide というエフェ
クトに対して次のようなハンドラを定義する．

with h handle sqrS (insert (▶ BIG)))(→∗ ▶ let y =◀▶ BIG in ◀ (with h handle sqrS ▶ y)()∗→ ▶ let y =◀▶ BIG in ◀ (with h handle ▶ (y ∗ y))()∗→ ▶ let y =◀▶ BIG in ◀▶ (y ∗ y)→∗ ▶ (let y = BIG in y ∗ y)def

pickTrue = {decide(x; k) 7→ k true}
このハンドラはエフェクト decide が発生したら，限エフェクトは有用な一方で，スコープ逸脱を容易に

定継続 k に true を渡す単純なものである．なお，エ引き起こす．

フェクト以外の計算結果に対する定義である return
節は，その値をそのまま返す自明なもの，つまりwith {raise(x; k) 7→ x} handle ▶ (λy. ◀ (raise ▶ y))−→∗ ▶ yreturn x 7→ x であるときは表記を省略する．これら

この raise ハンドラはエフェクト発生時の引数をそを with handle 式で組み合わせれば，エフェクトを扱のまま返す．多段階計算言語ではコード生成のためうプログラムが実現される．

にステージレベルが 1 の部分に ◀▶ M −→ M の簡with pickTrue handle if decide() then 10 else 0約ができるところがないか探しに行き，さらに途中−→ with pickTrue handle if true then 10 else 0でステージレベルが 0 になったところの計算も行う．

−→ with pickTrue handle 10

従ってこの計算例では y に具体的な値が束縛される−→ 10前にステージレベルが 0 である raise ▶ y が評価されることになる．これによって λy.M の M の部分での3 スコープ逸脱の問題

み意味をもつ y がそのスコープを飛び越えて，最終

本節では，型システムを設計する際に考慮すべき課的に意味がない計算結果になってしまう．

題であるスコープ逸脱の問題について説明する．ス

raise ハンドラの例は単純なものだったが，insert

ハンドラを用いたもう少し複雑な例もある．準備として，insert ハンドラとエフェクトの名前だけが違う

γ ∈ ScVar

2 つのハンドラを次のように定義する．

α ∈ TVardefh1 = { insert1(x; k) 7→▶ (let y1 =◀ x in ◀ (k(▶ y1 ))) }def

h2 = { insert2(x; k) 7→▶ (let y2 =◀ x in ◀ (k(▶ y2 ))) }τ, σ ::= α | bool | τ → τ | H γ. τ ⇒ σ | ▷(s,γ) τ | ∀s.ττ , σ ::= τ ! Σκ ::= τ ; τξ ::= τ | ∀α. ξ

このとき次のプログラムはスコープ逸脱を引き起

ψ ::= τ | ∀γ ′ ≥ γ. ξ | κこす．

Σ ::= {op1 : τ1 → σ1 @S1 , . . . , opn : τn → σn @Sn }Θ ::= {α1 , . . . , αn }with {insert1(x; k) 7→ · · · } handle

Γ ::= ϕ | Γ, x : ψ@(S, γ) | Γ, γ < γ ′ | Γ, γ ≤ γ ′with {insert2(x; k) 7→ · · · } handle
insert1 (insert2 ▶ 10)

図2型，環境の定義∗−→ ▶ let y1 = y2 in let y2 = 10 in y1
しかし，エフェクトの発生順番を入れ替えた次のプロ数の集合，TVar は型変数の集合を表す．スコープ変グラムではスコープ逸脱は起こらない．

数 γ は，型システムにおいて変数スコープを抽象的にwith {insert1(x; k) 7→ · · · } handle

表現するものである．型 τ の定義における H γ.τ ⇒ σwith {insert2(x; k) 7→ · · · } handle

はハンドラに対する型であり，ここで，H γ はスコー

insert2 (insert1 ▶ 10)∗

プ変数 γ に対する束縛を表す．この役割は後述する．

−→ ▶ let y1 = 10 in let y2 = y1 in y2

τ は，型 τ にシグネチャ Σ を加えたものである．（エ似たような例で，insert エフェクトが複数回呼び出さフェクト）シグネチャとはエフェクトの名前，型，それるプログラムも安全である．

れが発生するステージの 3 つ組の要素からなる集合

with {insert(x; k) 7→ · · · } handle

であり，τ ! Σ は，計算が終了して最終的に τ 型の値

insert (insert ▶ 10)∗−→ ▶ let y1 = 10 in let y2 = y1 in y2が得られる前に，途中で Σ に含まれるエフェクトが発生する可能性があることを表現している．κ は代数

本体系の型システムは，スコープ逸脱を起こすかど

的エフェクトが捕捉する限定継続に対する型であり，

うかを (保守的近似により) 識別し、スコープ逸脱を

本体系では通常の関数型と区別した特別な型として起こす可能性があるプログラムには、型をつけないよいる．

うにする必要がある．

4. 2 スコープの扱い

4 スコープ逸脱を防ぐための型システム
本節では，型システムの中でも特にスコープに関わる部分に焦点を当てて設計のポイントを述べる．

スコープ逸脱は，変数が，本来の場所からあってはならない場所に移動することで起きる問題であるから，これを型システムで防ぐには，変数が使える場
所，すなわちスコープを追跡する必要がある．以降

4. 1 定義の導入

は，型システムのスコープに関わる部分の説明をす型システムで扱う型や環境の定義を図 2 で与える．
▷

この定義のうち，多段階計算由来の定義は λ [9] に，
代数的エフェクト由来の定義は [2] に基づいている．

る．まず，我々が知りたいスコープに関する情報は次の 3 つである．

1. プログラムがどのスコープにあるか以降では本体系特有の部分について補足していく．

これは型判断 Θ; Γ `(S,γ) M : τ の形で表現する．

まず，型システムで変数スコープを追跡したいの

この γ の役割は，プログラムの場所を記録するこで，それを γ で表現する．集合 ScVar はスコープ変とであり，新しくステージレベル 1，つまりコードレベルでの変数が増えるたびにより深くなってことを想定すると，N の型 τ ! Σ に対して，いく．このことが端的に表れているのが図 3 のinsert : ▷(s,γ1 ) τ1 → ▷(s,γ2 ) τ1 @ε ∈ Σ

規則 (T-LetS) である．コードレベルで let 式

である．ここに出現するスコープ γ1 , γ2 のみに焦点の型付けをスコープ γ で行うとき，N の型付けを当てた時，これら（と γ ）の間に成り立っているべ′は γ より深いスコープ γ で行う．さらに x には′スコープ γ 以降で使えるという情報が型環境に追加される．

き条件はどのようなものか．

• まず N が insert (insert N ′ ) である時は安全であったから，insert の返り値は再度 insert に渡し

2. プログラムがどのスコープで型がつくか
本体系では例えば int 型のコードを表す型が ▷s intてよい，つまり γ2 で型がつくなら γ1 で型がつくべきなので γ2 ≤ γ1 である．

であるように，コード型には ▷ という構築子を用• 次に，insert の返り値はハンドラで新しく定義

いるが，ここでスコープ γ で使える int 型のコー

された変数を含んでいるので，γ あるいはそれよ

ド型を ▷(s,γ) int という型で表現できるようにし，り浅いスコープでは使えない．つまり γ < γ2 でコード型の構築子の中で使うことにする．

ある．

• 最後に，N の中で最も浅いスコープを γn とし3. スコープ同士の大小関係
スコープ上の 2 項関係 < を導入する．γ < γ ′ は′「γ で使える変数の集合 ⊂ γ で使える変数の集合」を意味する．†4 従って，γ < γ ′ で項 M が γ′

で型がつくなら，γ でも型がつく．

たとき，insert ハンドラは引数を限定継続の外に残すので，γ1 ≤ γn が必要になる．
以上の条件をすべて満たすような仕組みを考えたと
き，γ1 = γ2 として，ハンドル式のスコープを γ < γ1に対してγ4. 3 scope generator としてのハンドル式

with h handle γ1 N

本節では，型システムのうち，特に代数的エフェクのようにして，部分式 N のスコープを深くすれば十ト部分であるハンドラやハンドル式の型付け規則が分であることがわかる．これが本節のタイトルである

定まる経緯について述べる．本体系では多段階計算

scope generator としてのハンドル式の意味するところがあることでエフェクトとハンドラがコードをやりである．直観的には，ハンドル式（with h handle N ）とりすることができるので，代数的エフェクト単体のにセットされた h はコードレベルの変数を増やしう

体系における型付け規則をそのまま使うことはできるので，N のスコープを深くする必要があるというない．考察の題材には 3 節に引き続き，コードのやことである．

り取りを伴う insert エフェクトを用いる．
今，ステージ ε，スコープ γ で以下のようなハンドル式 †5 の型について考える．

そしてこの事実が反映された規則が図 3 の規則(T-WHdl) である．ハンドル式をスコープ γ で型をつけるとき，部分式の N の型付けはスコープ γ1 で行う．この γ1 は固有変数であり，N の型付け時にwith h handle N

型環境に加えられた γ ≤ γ1 は，これを満たす任意の

特に N にステージ ε の insert エフェクトが含まれる

γ1 でという意味合いを持つ．なお，ここで γ < γ1 でγはなく γ ≤ γ1 としているのは，主部簡約定理の証明時に必要になるからである．また，一方でこの γ1 は†4 使える変数の集合に関する包含関係と，スコープそのものの包含関係は逆であることに注意されたい．すな
わち，γ < γ ′ は，γ に対応するスコープが γ ′ に対応
するスコープを含むことを意味する．
†5 プログラム中に表れるスコープ変数 γ はプログラムのスコープを表現した便宜上のものであり，構文の一部ではない．

with h handle N の h からは見えないので，そこでは抽象化して持っておく必要がある．それがハンドラの型 H γ.τ ⇒ σ における γ であり，規則 (T-HdlE2)における γh である．

′Θ; Γ, x : ξ@(s, γ ′ ), γ < γ ′ `(s,γ ) N : τ ! ΣΘ; Γ `(s,γ) M : ξ ! Σ

γ′ ∈
/Γ

Θ; Γ `(s,γ) let x = M in N : τ ! Σ(T-LetS)Θ; Γ, γ ≤ γh , x : τ @(ε, γh ) `(ε,γh ) M0 : (▷(s,γh ) σ) ! Σ′[Θ; Γ, γ ≤ γh , γh ≤ γd , x : τi @(ε, γh ), k : ▷(s,γd ) σi ; (▷(s,γh ) σ) ! Σ′ @(ε, γh ) `(ε,γh ) Mi : (▷(s,γh ) σ) ! Σ′ ]1≤i≤n[Θ; Γ, γ ≤ γh , x : τj @(ε, γh ), k : σj ; (▷(s,γh ) σ) ! Σ′ @(ε, γh ) `(ε,γh ) Mj : (▷(s,γh ) σ) ! Σ′ ]1≤j≤m[copi : τi → ▷(s,γh ) σi @ε ∈ Σ, opj : τj → σj @ε ∈ Σ]1≤i≤n,1≤j≤m
Σ \ {copi : τi → ▷(s,γh ) σi @ε, opj : τj → σj @ε}1≤i≤n, 1≤j≤m ⊂ Σ′ ,Θ; Γ `(ε,γ) {return x 7→ M0 ,copi (x; k) 7→ Mi ,Θ; Γ `(ε,γ) M : (H γh . τ ! Σ ⇒ σ ! Σ′ ) ! ϕ

γ h , γd ∈/Γopj (x; k) 7→ Mj } : (H γh . τ ! Σ ⇒ (▷(s,γh ) σ) ! Σ′ ) ! ϕΘ; Γ, γ ≤ γ1 `(ε,γ1 ) N : (τ ! Σ){γh := γ1 }Θ; Γ `(ε,γ) with M handle N : (σ ! Σ′ ){γ
図3

γ1 ∈
/Γ

(T-HdlE2)(T-WHdl)h := γ}型システム（一部抜粋）

4. 4 型付けの具体例

が，これは問題ない．▶ 10 は任意のスコープで型が

本節では，スコープ部分のみに注目した型付けの具付けられるので insert1 の引数として適切である．次

体例を確認する．題材は 3 節で取り上げた insert1，にこの返り値が insert2 に渡せるかを考える．同様に

insert2 を使った 2 つのプログラムである．なお，注して insert2 の型は γ2 → γ2 であるから，このエフェ

目したいのは主にスコープであるから，それ以外の情

クトに insert1 ▶ 10，つまり γ1 で型がつく項を渡せ

報は適宜捨象して記述する．

るかを考えればよく，これは可能である．なぜなら今γ1 ≤ γ2 であることがわかっているので，γ1 で型がγ

with {insert1(x; k) 7→ · · · } handle

γ1

つくなら γ2 でも型がつくからである．以上のようにwith {insert2(x; k) 7→ · · · } handle

γ2insert2 (insert1 ▶ 10)∗−→ ▶ let y1 = 10 in let y2 = y1 in y2
まずは，型がつくべきプログラムの方を見る．h1 とh2 には例えば次のような型がつけられる．

してこのプログラムはスコープの検査を通過する．
次にスコープ逸脱を起こす方には型がつけられないことを示す．
γwith {insert1(x; k) 7→ · · · } handleγ1
with {insert2(x; k) 7→ · · · } handleγ2
insert1 (insert2 ▶ 10)

h1 :H γh1 . ▷(s,γh1 ) (int ! ϕ) ! {insert : γh1 → γh1 }⇒ (▷(s,γh1 ) (int ! ϕ)) ! ϕ
h2 : γh2 . ▷(s,γh2 ) (int ! ϕ) ! {insert : γh2 → γh2 }H⇒ (▷(s,γh2 ) (int ! ϕ)) ! ϕ−→∗ ▶ let y1 = y2 in let y2 = 10 in y1
こちらの例も推論に使う材料はほとんど同じである．まず，insert ハンドラに型をつけるためには規則(T-HdlE2) の cop 節での型付けが必要であり，これにより insert2 の返り値のスコープは γ2 が必要であ

この型付けは規則 (T-HdlE2) によって導出される．従って insert2 ▶ 10 のスコープは γ2 となる．一る．この insert ハンドラは新しく定義したコードレ

方で，γ1 の引数のスコープは γ1 以下である必要があ

ベルの変数を継続に渡すので，cop，op と 2 つあるうる．しかし γ1 と γ2 の関係については γ1 ≤ γ2 しかちの前者の規則で型をつけることになる．次にハン言えないので，γ2 で型がつく insert2 ▶ 10 を insert1ドルされる側のプログラムのスコープを調べる．まに渡すことはできない．以上の推論により，いかなるずは insert1 ▶ 10 であるが，insert1 のハンドラと型もつけられないことがわかる．

型を合わせるために insert1 : γ1 → γ1 が必要になる

案した型システムをより簡潔に表現できる方法がな

5 関連研究いか検討したい．

今回提案した体系は，多段階計算に計算エフェクトを加えた体系と考えることができる．エフェクトを持つ多段階計算の型安全性という問題に取り組んだ

参 考 文 献初期の研究として Kameyama，Kiselyov，Shan らに[1] Kameyama, Y., Kiselyov, O., and Shan, C.-c.:
Shifting the stage: Staging with delimited control, Journal of Functional Programming, Vol. 21,
No. 6(2011), pp. 617–662.
[2] Kammar, O. and Pretnar, M.: No value restriction is needed for algebraic eﬀects and handlers,
Journal of functional programming, Vol. 27(2017).
[3] Kiselyov, O., Kameyama, Y., and Sudo, Y.: Reﬁned Environment Classiﬁers, Asian Symposiumon Programming Languages and Systems, Springer,
2016, pp. 271–291.
[4] OCaml: Multicore OCaml: September 2021,
eﬀect handlers will be in OCaml 5.0!, 2021.
https://discuss.ocaml.org/t/multicore-ocaml-september2021-eﬀect-handlers-will-be-in-ocaml-5-0/8554.
[5] Oishi, J. and Kameyama, Y.: Staging with
control: type-safe multi-stage programming with
control operators, Proceedings of the 16th ACM
SIGPLAN International Conference on Generative
Programming: Concepts and Experiences, 2017,
pp. 29–40.
[6] Plotkin, G. and Pretnar, M.: Handlers of algebraic eﬀects, European Symposium on Programming, Springer, 2009, pp. 80–94.
[7] Pretnar, M.: An introduction to algebraic effects and handlers. invited tutorial paper, Electronic notes in theoretical computer science,Vol. 319(2015), pp. 19–35.
[8] Taha, W. and Nielsen, M. F.: Environment classiﬁers, Proceedings of the 30th ACM SIGPLANSIGACT symposium on Principles of programming
languages, 2003, pp. 26–37.
[9] Tsukada, T. and Igarashi, A.: A Logical Foundation for Environment Classiﬁers, Log. Methods
Comput. Sci., Vol. 6, No. 4(2010).

よる研究があり [1]，エフェクトの実現に shift/resetという限定継続演算子が用いられている．他には

shift0/reset0 という限定継続演算子によってエフェ
クト付きの多段階計算を実現した Oishi らの研究 [5]もある．これらの体系はハンドラを名前付きで指定できないため，エフェクト発生時に，それを補足したいハンドラがいくつ先にあるかを意識する必要があった．代数的エフェクトはエフェクトに名前がついているので，自身を補足するハンドラの指定がより直観的である一方で，スコープ逸脱の議論で例に挙げた insert1，insert2 のハンドラが入れ子になった問題に表れるようにスコープの扱いがより複雑になると予想される．
また，本研究が技術的に影響を受けているのは，

Taha らの Environment classiﬁers [8] と，Kiselyov らの Reﬁned Environment Classiﬁers [3] である．これらの研究では，安全性を保証するためにステージ（あるいはスコープ）に関する情報を抽象化して型システ
ムで追跡するというアイデアが使われており，それは本研究でも大いに参考にした．このうち Taha らの研究は多段階計算言語体系の 1 つの標準となる体系を提案したものであり，Kiselyov らの研究は多段階計
算に書き換え可能な変数を追加して計算エフェクトを実現したものである．

A 型システム6 まとめと今後の課題
本研究では，代数的エフェクトを備えた 2 段階計

本文中で言及しなかったものも含めて，型付け規則
全体を記載する．なお，型付け規則中の ΣS は Σ の算言語の型システムを設計した．特に，スコープ逸脱

部分集合であり，Σ の要素のうち op : τ → σ@S でを解決するためにいくつかの際どい例を観察し，ハン

あるもののみから構成される．また，FSV(·) は，定ドル式を scope generator とみなす規則によって解決

義域に含まれる自由なステージ変数の集合と取り出できることを発見した．今後の課題は，主部簡約定理

す関数である．

などの証明を与えることである．その他には，今回提(x : τ @(S, γ)) ∈ ΓΘ; Γ `(S,γ) x : τ(x : ∀α. ξ@(S, γ)) ∈ Γ(T-Var)Θ; Γ `(S,γ) x : ξ[α := σ](x : ∀γ ′ ≥ γ. ξ@(S, γ)) ∈ ΓΓ ` γ ′′ ≥ γ′′

Θ; Γ `(S,γ ) x : ξ[γ ′ := γ ′′ ]Θ; Γ `(S,γ) true : bool
Θ; Γ `(S,γ) M : τΘ; Γ `(S,γ) M : τ ! Σ(T-True)(T-ScIns)

Θ; Γ `(S,γ) false : bool

Θ; Γ `(ε,γ) M : ψ ! Σ(T-Red)(T-TIns)(T-False)

Θ; Γ, x : ψ@(ε, γ) `(ε,γ) N : τ ! ΣΘ; Γ `(ε,γ) let x = M in N : τ ! Σ′Θ; Γ, x : ξ@(s, γ ′ ), γ < γ ′ `(s,γ ) N : τ ! ΣΘ; Γ `(s,γ) M : ξ ! Σ

γ′ ∈
/Γ

Θ; Γ `(s,γ) let x = M in N : τ ! ΣΘ; Γ `(S,γ) M : bool ! ϕΘ; Γ `(S,γ) N1 : τ ! ΣΘ; Γ `(S,γ) if M then NΘ; Γ `(S,γ) N2 : τ ! ΣΘ; Γ `(ε,γ) λx.M : (τ → σ ! Σε ) ! ϕ′Θ; Γ, x : τ @(s, γ ′ ), γ < γ ′ `(s,γ ) M : σ ! Σ

γ′ ∈
/Γ

Θ; Γ `(S,γ) N : τ ! ϕΘ; Γ `(S,γ) M N : σΘ; Γ `(s,γ) M : τ ! ΣΘ; Γ `(ε,γ) ▶
Θ; Γ `(S,γ) M : σ ! ϕr M : (▷(s,γ)τ ! Σs ) ! Σ ε

Θ; Γ `(S,γ) Λs′ .M : ∀s′ .σ ! ϕ(T-App)Θ; Γ `(ε,γ) M : (▷(s,γ) τ ! Σs ) ! Σε(T-SGen)

Θ; Γ `(ε,γ) M : ∀s. ▷(s,γ) τΘ; Γ `(ε,γ) run M : τ [s := ε]
図5(T-AbsS)

型付け規則 1

(T-▶)

s′ ∈
/ FSV(Γ) ∪ FSV(S)(T-If)(T-AbsE)Θ; Γ `(s,γ) λx.M : (τ → σ ! Σs ) ! Σε

図4

(T-LetS)

1 else N2 : τ ! ΣΘ; Γ, x : τ @(ε, γ) `(ε,γ) M : σ ! ΣΘ; Γ `(S,γ) M : (τ → σ) ! ϕ(T-LetE)Θ; Γ `(s,γ) ◀s M : τ ! Σ(T-◀)Θ; Γ `(S,γ) M : ∀s′ .σ ! ΣΘ; Γ `(S,γ) M u : σ[s′ := u] ! Σ(T-Run)型付け規則 2（多段階計算）(T-SIns)Θ; Γ, γ ≤ γh , x : τ @(ε, γh ) `(ε,γh ) M0 : σ ! Σ′Θ; Γ, γ ≤ γh , x : τi @(ε, γh ), k : σi `(ε,γh ) Mi : σ ! Σ′[opi : τi → σi @ε ∈ Σ]1≤i≤n , Σ \ {opi : τi → σi @ε ∈ Σ}1≤i≤n ⊂ Σ′ , γh ∈/Γ(T-HdlE1)

Θ; Γ `(ε,γ) {opi (x; k) 7→ Mi } : H γh . τ ! Σ ⇒ σ ! Σ′ ! ϕΘ; Γ, γ ≤ γh , x : τ @(ε, γh ) `(ε,γh ) M0 : (▷(s,γh ) σ) ! Σ′[Θ; Γ, γ ≤ γh , γh ≤ γd , x : τi @(ε, γh ), k : ▷(s,γd ) σi ; (▷(s,γh ) σ) ! Σ′ @(ε, γh ) `(ε,γh ) Mi : (▷(s,γh ) σ) ! Σ′ ]1≤i≤n[Θ; Γ, γ ≤ γh , x : τj @(ε, γh ), k : σj ; (▷(s,γh ) σ) ! Σ′ @(ε, γh ) `(ε,γh ) Mj : (▷(s,γh ) σ) ! Σ′ ]1≤j≤m[copi : τi → ▷(s,γh ) σi @ε ∈ Σ, opj : τj → σj @ε ∈ Σ]1≤i≤n,1≤j≤m
Σ \ {copi : τi → ▷(s,γh ) σi @ε, opj : τj → σj @ε}1≤i≤n, 1≤j≤m ⊂ Σ′ ,γ h , γd ∈/ΓΘ; Γ `(ε,γ) {return x 7→ M0 , copi (x; k) 7→ Mi , opj (x; k) 7→ Mj } : (H γh . τ ! Σ ⇒ (▷(s,γh ) σ) ! Σ′ ) ! ϕ(T-HdlE2)

Θ; Γ, x : τ @(s, γh ), γ ≤ γh `(s,γh ) M0 : σ ! Σ′[Θ; Γ, γ ≤ γh , x : τi @(s, γh ), k : σi ; σ ! Σ′ `(s,γh ) Mi : σ ! Σ′ ]1≤i≤n[opi : τi → σi @s ∈ Σ]1≤i≤n , Σ \ {opi : τi → σi @s}1≤i≤n ⊂ Σ′ , γh ∈/Γ(T-HdlS)Θ; Γ `(s,γ) {return x 7→ M0 , opi (x; k) 7→ Mi } : (H γ1 . τ ! Σ ⇒ σ ! Σ′s ) ! Σ′εΘ; Γ `(ε,γ) M : (H γh . τ ! Σ ⇒ σ ! Σ′ ) ! ϕΘ; Γ, γ ≤ γ1 `(ε,γ1 ) N : (τ ! Σ){γh := γ1 }Θ; Γ `(ε,γ) with M handle N : (σ ! Σ′ ){γ
op : τop → σop @S ∈ ΣΘ; Γ `(S,γ) x : τop

Θ; Γ `(S,γ) op x : σ
図6Θ; Γ `(S,γ) x : τ ! ϕΘ; Γ `(S,γ) throw(k, x) : σΘ; Γ `(ε,γ) k : ▷(s,γa ) τ ; (▷(s,γb ) σ) ! ΣΘ; Γ `(ε,γ) k : ▷Σ ⊂ Σ′

Θ; Γ `(S,γ) M : τ ! Σ′′Θ; Γ `(s,γ ) M : τΘ, α; Γ `(S,γ) M : τ ! ΣΘ; Γ `(S,γ) M : (∀α.τ ) ! Σ(T-KApp)γc ∈ Γ

(s,γa ∪γc ) τ ; (▷(s,γb ∪γc ) σ) ! ΣΘ; Γ `(S,γ) M : τ ! ΣΓ ` γ < γ′

(T-Op)

op ! Σ

型付け規則 3（代数的エフェクト）

Θ; Γ `(S,γ) k : τ ; σ

Θ; Γ `(S,γ) M : τ(T-KSub)(T-SigAdd)′(T-Sub1)

Θ; Γ `(ε,γ ) M : (▷(s,γ) τ ) ! ΣΓ ` γ < γ′′Θ; Γ `ε,γ M : (▷(s,γ ′ ) τ ) ! Σ(T-TGen)

図7(T-WHdl)h := γ}Θ; Γ `(S,γ) M : ξ ! ΣΘ; Γ `(S,γ) M : (∀γ ′ > γ. ξ[γ := γ ′ ]) ! Σ

τ ! Σ の型付け規則 4（その他）(T-Sub2)(T-ScGen)