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

多段階 let 挿入を行うコード生成言語の型システムの
設計
大石 純平

亀山 幸義

コード生成法は，プログラムの実行性能の高さと保守性・再利用性を両立できるプログラミング手法として有力なものである．本研究は，コード生成法で必要とされる「多段階 let 挿入」等を簡潔に表現できるコントロールオペレー
タである shift0/reset0 を持つコード生成言語とその型システムを構築し，生成されたコードの型安全性を保証するための型システムを構築した．多段階 let 挿入は，入れ子になった for ループを飛び越えたコード移動を許す仕組みであり，ループ不変式の移動などのために必要である．コード生成言語の型安全性に関して，破壊的代入を持
つ体系に対する Sudo らの研究等があるが，本研究は，彼らの環境識別子にジョインを追加するという拡張により，
shift0/reset0 を持つコード生成言語に対する型システムが構築できることを示した．

て，コードを移動する機能である．

1 はじめに本研究は，多段階 let 挿入を可能とするコード生成

コード生成法は，プログラムの生産性・保守性と実体系の構築のため，比較的最近になって理論的性質が行性能の高さを両立させられるプログラミング手法解明された shift0/reset0 [3] というコントロールオペとして有力なものである．本研究は，コード生成法でレータに着目する．このコントロールオペレータに対必要とされる「多段階 let 挿入」等を簡潔に表現できする型規則を適切に設計することにより，型安全性をるコントロールオペレータである shift0/reset0 を持解決することを目的とする．コントロールオペレー

つコード生成言語とその型システムを構築し，生成さタを含む項の計算について分析した結果，スコープれたコードの型安全性を静的に保証する言語体系おの包含関係が逆転することや 2 つのスコープの合流

よび型システムを設計する．これにより，コード生成があることから，変数スコープを表す識別子にジョイ器のコンパイル段階，すなわち，実際にコードが生成

ン (和集合) を追加すればよいという着想を得て，型されてコンパイルされるより遥かに前の段階でのエシステムを設計することに成功した．

ラーの検出が可能となるという利点がある．

本研究に関連した従来研究としては，束縛子を越えコード生成における let 挿入は，生成されたコードない範囲でのコントロールオペレータを許した研究を移動して効率良いコードに変形するための機能でや，局所的な代入可能変数を持つ体系に対する須藤あり，ループ不変式を for ループの外側に移動したらの研究 [5]，後者を，グローバルな代入可能変数をり，コードの計算結果を共有するなどのコード変換

持つ体系に拡張した研究 [2] などがある．しかし，い(コード最適化) において必要な機能である．多段階ずれの研究でも 多段階の for ループを飛び越えた let

let 挿入は，入れ子になった for ループ等を飛び越え

挿入は許していない．本研究は，須藤らの研究をベースに，shift0/reset0 を持つコード生成体系を設計しType-Safe Code Generation with Multi-level Letinsertion
Junpei Ohishi, Yukiyoshi Kameyama, 筑波大学システ
ム情報工学研究科コンピュータ・サイエンス専攻, Department of Computer Science, University of Tsukuba.

た点に新規性がある．

するプログラムである．

2 コード生成と let 挿入(int 3) ⇝∗ <3>

コード生成，すなわち，プログラムによるプログ(int 3) + (int 5) ⇝∗ <3 + 5>

ラム (コード) の生成の手法は，対象領域に関する知

int は整数を整数のコードに変換し，+ は，整数の識，実行環境，利用可能な計算機リソースなどのパラ

コード 2 つをもらって，それらの加算をおこなうコー

メータに特化した (実行性能の高い) プログラムを生ドを生成するコードコンビネータである．なお，⇝∗成する目的で広く利用されている．生成されるコーは 0 ステップ以上の簡約を表す．

ドを文字列として表現する素朴なコード生成法では，構文エラーなどのエラーを含むコードを生成してしまう危険があり，さらに，生成されたコードのディバッ
グが非常に困難であるという問題がある．

λx.e と @ はそれぞれラムダ抽象と関数適用のコードを生成する．

λx.x+(int 3) ⇝∗ <λu.u + 3>
(λx.x+(int 3)) @ (int 5) ⇝∗ <(λu.u + 3) 5>

これらの問題を解決するため，コード生成器 (コーラムダ抽象のコードコンビネータにおいて，x はド生成をするプログラム) を記述するためのプログラ「(コードレベルの) 変数」そのものを表すのではなく，

ム言語の研究が行わており，特に静的な型システムの「変数のコード」をあらわす．上記の例の計算過程で，サポートを持つ言語として，MetaOCaml, Templatex は <u>(ここで u は新たに作成されたコードレベル

Haskell, Scala LMS などがある．

の変数) に簡約され，計算が進む．

本 研 究 は ，MetaOCaml な ど の 値 呼 び 関 数 型 言

let は let 式のコードを生成する．

語に基づいたコード生成言語を対象としているが，let x = (int 3) in x + (int 7)

言語のプレゼンテーションでは，先行研究になら⇝∗ <let u = 3 in u + 7>

いコードコンビネータ (Code Combinator) 方式を

実は，let は，コードコンビネータとしてのラムダ抽使う．MetaML/MetaOCaml などにおける擬似引用

象と適用によりマクロ定義され，上記の式は，以下の(Quasi-quotation) 方式は，コード生成に関する言語

式と同じである．

要素として「ブラケット (コード生成,quotation)」と(λx. x + (int 7) ) @ (int 3)「エスケープ (コード合成,anti-quotation)」を用いる⇝∗ <let u = 3 in u + 7>のに対して，コードコンビネータ方式では，各演算本研究の対象言語は，MetaML や MetaOCaml と子に対して，「コード生成版の演算子 (コードコンビ

同様，静的束縛の言語であり，以下の例では，束縛変ネータ)」を用意してコード生成器を記述する．たと数の名前が正しく付け換えられる．

えば，加算 e1 + e2 に対して，コードコンビネータ版

λy.let x = y in λy. x + y ⇝∗ <λu.λu′ .u + u′ >は e1 +e2 というように，演算子名に下線をつけてあこの例では，2 つのラムダ抽象が y という変数をもっらわす．

ているが，これらは異なる束縛変数であるので，計算

本章では，例に基づいてコード生成器と let 挿入にの過程で衝突が起きるときは名前換えが発生する．

ついて説明する．対象言語の構文・意味論などの形式的体系の説明は後に行う．

2. 2 コード生成における let 挿入
for は for 式を生成するコードコンビネータである．

2. 1 コードコンビネータ方式のプログラム例

ここで，(コードレベルの) 配列 a の第 n 要素に対すまず，(完成した) コードは，<3> や <3 + 5> のようる代入を a[n] ← e と表し，aryset a e1 e2 は対応すにブラケットで囲んで表す．次の例は，これらを生成るコードコンビネータであると仮定する．また，a は

適宜 n 次元のものを考えることにする．

ことで実現できることが知られている．本研究では，

for x = (int 3) to (int 7) do

shift0/reset0 というコントロールオペレータを用い

aryset <a> x (int 0)∗⇝ <for i = 3 to 7 do a[i] ← 0>
for を入れ子にすると，入れ子の for 式が生成できる．

て let 挿入を実現する．
上記のコード生成器にコントロールオペレータを組みこんだものが次のプログラムである．

for x = (int 3) to (int 7) do

reset0 (for x = (int 3) to (int 7) dofor y = (int 1) to (int 9) do(for y = (int 1) to (int 9) do

aryset <a> (x, y) (int 0)∗⇝ <for i = 3 to 7 dofor j = 1 to 9 doa[i, j] ← 0>
この二重ループの中で，複雑な計算をするループ

shift0 k1 → let z = e inthrow k1 (aryset <a> (x, y) z)))
赤字の reset0,shift0,throw がコントロールオペレー
タであり，それらに対するインフォーマルな †2 計算
規則は以下の通りである．

不変式があったとする．たとえば，配列の初期値として 0 でなく，(何らかの複雑な) 計算結果を代入する

reset0 v → v

が，その計算にはループ変数 i, j を使わない場合を考

reset0 (E[shift0 k → · · · (throw k v) · · · ])える．それを e とすると，→ · · · (reset0(E[v])) · · ·<for i = 3 to 7 do

ここで v は値，E は評価文脈である．2 行目では，

for j = 1 to 9 doreset0 と shift0 に挟まれた文脈が切り取られ，変数a[i, j] ← e>

k に束縛され，throw k e の形の式の場所で利用さというコードの代わりに<let z = e inれる．ここで切り取られる文脈には，トップにあった reset0 も含まれているため，簡約後のトップから

for i = 3 to 7 doreset0 が消えている．よく知られている shift/resetfor j = 1 to 9 do

では，この reset0 が残る点が異なっている．

a[i, j] ← z>

上記のコード生成器をこの計算規則によというコードの方が実行性能が高くなることが期待

り 計 算 す る と ，2 重 の for 式 に 相 当 す る 文 脈できる．

for x = · · · to · · · do for y = · · · to · · · do [ ] が

このように，生成するコードの上部 (トップレベル

切り取られ throw の部分の k1 で使われる．結果とに近い方) に let 式を挿入することができれば，早いして，let z = e in の部分が，この文脈の外側に移動

段階で値を計算できたり，また，同一の部分式がある

する効果が得られ，let 挿入が実現できる．
上記の例では，一番外側まで let 挿入を行ったが，場合は計算結果を再利用できたり，という利点がある †1 ．

式 e が x に相当するループ変数を含むときは，一番外

そこで，コード生成器に let 挿入の機能を組み込も側まで持っていくことはできず，2 つの for 式の中間

う．let 挿入は部分計算の分野等で研究されており，地点まで移動することになる．このためには，reset0

CPS 変換あるいはコントロールオペレータを用いるの設置場所を変更すればよい．
問題は，このように let 挿入をしたい式が複数あ†1 この変形・最適化は，コードを生成してから行なう
のでよければ技術的に難しいものではない．しかし，コード生成においては，生成されるコード量の爆発が問題になることが多く，無駄なコードはできるだけ早い段階で除去したい，すなわち，コードを生成してから最適化するのではなく生成段階でコードを変形・最適化したいという強い要求がある．

る場合である．
「let 挿入をする先」に reset0 を 1 つ置くため，いくつかの let 挿入においては直近の re-

set0 まで移動するのではなく，2 つ以上先の (遠く†2 精密な意味論は後述する．

の)reset0 まで let を移動したいことがある．これは，vironment Classifier) を導入した．環境識別子 α は，

shift0/reset0 を入れ子にすることにより，以下のよ

コード生成のステージに対応し，「そのステージで使

うに実現できる．

える (コードレベル) の変数とその型の集合 (あるいreset0 (for x = (int 3) to (int 7) doは型文脈)」を抽象的に表現した変数であり，⟨int⟩αreset0 (for y = (int 1) to (int 9) doのように，コード型の一部として使用される．

shift0 k2 → shift0 k1 → let z = e in

須藤ら [5] は，破壊的変数を持つコード生成言語に

throw k1 (throw k2 (aryset <a> (x, y) z))))

対する型安全性を保証するため，環境識別子を精密

青字のコントロールオペレータをいれた場合，let 挿化した．本節では，須藤らのアイディアを解説する．

入の「目的地」であるトップの位置 (赤字の reset0 で以下の図は，彼らの言語における危険なプログラム例

指定された位置) は，2 つ先の reset0 になってしまっである．

たが，これは，shift0 と throw をそれぞれ 2 回入れ子にすることにより実現できる．これが多段階 let 挿
入である．
なお，このように直近の reset0 を越えた地点までの移動 (あるいは文脈の切り取り) は，shift/reset で

危険な例
ここで，r は，整数のコードを格納する参照 (破壊的は実現できず，その拡張である階層的 shift/reset やセル) であり，r := y と !r はそれぞれ，r への代入

shift0/reset0 が必要となる．本研究では，簡潔さのと r の中身の読み出しを表す．上記のプログラムは，ため，shift0/reset0 を用いることとした．

コードレベルのラムダ抽象 (y に対するラムダ抽象)

さて，以上のように shift0/reset0 を使うことによで生成されるコードレベル変数を u とするとき，<u>

り多段階 let 挿入が実現できることがわかったが，自を r に格納し，u のスコープ (黄色で示したもの) が由な使用を許せば，危ないコード生成器を書けてし終わったあとに取り出しているため，計算結果は，自まう．上記の例では，項 e がどのループ変数に依存

由変数をもつコード <u> となり，危険である．

するかによって，let をどこまで移動してよいかが変上記のようなプログラムを型エラーとするため，須わってきた．例えば，トップレベルまで移動するコー

藤らは，コードレベル変数のスコープごとに環境識

ド生成器の場合，e が <7> のときは型がつき，x や別子を割り当てた．上記では外側のスコープ (青) がy のとき型が付かないようにしたい．このような精密

γ0 ，内側のスコープ (黄) が γ1 という環境識別子で表な区別を実現する型システムを構築するのが本研究現される．γ0 で有効なコードレベル変数はなく，γ1の目的である．

で有効なコードレベル変数は y(に対応して生成され3 環境識別子による型システムの構築

る変数) である．γ0 のスコープは γ1 のスコープを含む．言い換えれば，γ1 で使える変数の方が γ0 で使え

3. 1 先行研究のアイディア

る変数の方が (同じか) 多い．このことを γ1 ≥ γ0 と

表現力と安全性を兼ね備えたコード生成の体系とし表すことにする．r は ⟨int⟩γ0 ref 型を持つ．y は γ1ては，2009 年の亀山らの研究 [1] が最初である．彼らで使える変数であるが，γ0 では使えないため，r には，MetaOCaml において shift/reset とよばれるコ

y を代入することはできず，r := y のところで型エントロールオペレータを使うスタイルでのプログララーとなる．

ミング を提案するとともに，コントロールオペレー

コードレベルの変数スコープと，型によるスコー

タの影響が変数スコープを越えることを制限する型

プの表現をあらわしたのが，以下の図である．for やシステムを構築し，安全性を厳密に保証した.

let などコードレベルの束縛子があるたびに，新しい

Taha ら [4] は，純粋な (副作用のない) コード生成の言語の型安全性を保証するため，環境識別子 (En-スコープが開かれ，使える変数が増えていくことが分かるだろう．

コードレベルの変数の型に，(精密化した) 環境識
別子を付与することで，その変数が使えるスコープがわかり，破壊的代入などの副作用があるプログラムにおいてもスコープや型の安全性を保つことができる．
なお，須藤らの対象としていた言語が持っていた計算エフェクトは，「局所的なスコープをもつ参照」であり，現実の OCaml/MetaOCaml 等とは異なるも上の方の図で，使えるコードレベル変数が異なる場所のであった．同一の著者グループは，最近，精密化しごとに，γ0 , γ1 , γ2 , γ3 と名付けた．須藤らの体系通り

た環境識別子のアイディアを用いて，グローバルな参であれば，これらの環境識別子の間の順序は，スコー

照を持つ言語に対するある種の型安全性が成立する

プの包含関係通りであるので，ことを示している [2]．という順序がつくはずである．しかし，計算を進めて

3. 2 本研究: 環境識別子の拡張得られたコードを見ると (上記の下の図はコードの中本研究で扱う shift0/reset0 によるコントロールエ

身を示している)，γ1 (緑色) と γ2 (黄色) の位置関係がフェクトは，須藤らによる精密化された環境識別子で入れ代わっている．結果のコードの型が整合する (束も扱うことができない．本節では，その問題点を明ら縛変数が自由になることはない等) ためには，γ2 におかにし，その問題の解決の鍵となる join (∪) の導入

いて γ1 で使える変数を使ってはいけないことがわかについて述べる．

る．一方で，赤字で示された γ3 においては，γ1 の変

このため，前述の 2 重の for ループ生成において，その中間に let 挿入をするプログラムについて考察す

数も γ2 の変数も使って構わない．これらを考慮すると，環境識別子の間の順序は以下の図となる．

る．その概形は下記の 1 つ目の図である．

ここでのポイントは，γ0 から，2 つの異なる (包含関係のない)γ1 と γ2 に別れたあと，再び γ3 で合流することである．須藤らの体系では，環境識別子のなす半順序集合全体は木の形であったが，本研究の体系
では，このように１度別れたものが合流することがある．なお，γ3 で使える変数の集合は γ1 と γ2 で使える変数の和集合と一致するので γ3 = γ1 ∪ γ2 とおくことができる．このように，環境識別子の世界に最終的に得られた throw の型付け規則は以下のもJoin (∪) を導入することにより，コントロールオペのであり，継続変数 k には，特別な関数型 ⇒ を与レータによる文脈の移動に対応できることになった．

えていること (通常の関数型は → で表現している)，
また，γ1 から γ0 への変換子として得られた k を，

3. 3 本研究: 型システムの構築

γ1 ∪ γ2 から γ2 = γ0 ∪ γ2 への変換子として利用して本研究の基本アイディアは前項で述べたようなシいることがわかる．
Γ ⊢ v : ⟨t1 ⟩γ1 ∪γ2 ; σ

ンプルなものであるが，言語体系と型システムの構築にあたってはいくつかの困難があった．ここでは，そのうち，コントロールオペレータが切りとった継続に関する多相性について述べる．
前節の例では，shift0 が切り取る文脈 (継続) は，穴が γ1 のスコープにあり (その型は ⟨t1 ⟩γ1 の型)，文脈全体が γ0 のスコープのにある (その型は ⟨t0 ⟩γ0 の形)となっている．これを throw において使うときは，γ3スコープのものを γ2 スコープに変換している．すな
わち，k は ⟨t1 ⟩γ3 型から ⟨t0 ⟩γ2 型への関数であるよ
うに振る舞う．
この 2 つのギャップを埋めるのは，継続 (評価文脈)のある種の多相性である．このケースでは，⟨t1 ⟩γ1 → ⟨t0 ⟩γ0という型で定義された継続変数 k が，任意の γ2 ≥ γ0に対して，

⟨t1 ⟩γ1 ∪γ2 → ⟨t0 ⟩γ0 ∪γ2という型を持つことが言えれば良いことがわかる．

(γ3 = γ1 ∪ γ2 ある こ と ，ま た ，γ2 ≥ γ0 な ら ば
γ0 ∪ γ2 = γ2 であることに注意されたい．)
このような多相性 (サブタイプのもとでの多相性)
は，継続の研究ではいくつか知られており，今回のケースでも成立すると考えられる †3 ．
本研究では，将来的に型推論アルゴリズムを構築す
ることを考慮して，環境識別子に関する一般的な多相性を導入することを避け，継続変数について特別な型を与え，その変数を throw で使うときに，多相性を利用できるようにするという方策をとった．これにより型システムを複雑化させることなく，コントロール
オペレータの導入ができ，簡潔な型保存性の証明につながった．
†3 この型付けが問題ないことは直感的には明らかであるが，意味論の上で，このような型付け規則が「正しい」ことの証明は，将来課題である．

γ1 σΓ, k : ⟨t1 ⟩⇒ ⟨t0 ⟩

γ0

Γ |= γ2 ≥ γ0

⊢ throw k v : ⟨t0 ⟩γ2 ; σ

なお，継続が作用する型 (上記の ⟨t1 ⟩γ1 など) は，
本研究ではコード型に限定した．その理由は，須藤らの体系の方式で，参照 (ref) が関数型を持つことを許すとコードレベル変数が束縛域を脱出してしまい，本研究のコントロールオペレータを持つ体系でも同様の事態が生じると予想されたからである．なお，コード型のみを扱うことのできるコントロールオペレー
タであっても，多段階 let 挿入の表現のためには十分である．

4 対象言語: 構文と意味論
本研究における対象言語は，ラムダ計算にコード生
成機能とコントロールオペレータ shift0/reset0 を追加したものに型システムを導入したものである．
本稿では，最小限の言語のみについて考えるため，
コード生成機能の「ステージ (段階)」は，コード生成
段階 (レベル 0，現在ステージ) と生成されたコードの実行段階 (レベル 1，将来ステージ) の 2 ステージのみを考える．
前述したように，本研究の言語では，コードコンビ
ネータ (Code Combinator) 方式を使い，コードコン
ビネータは，+ や if のように下線を引いて表す．

4. 1 構文の定義
対象言語の構文を定義する．
変数は，レベル 0 変数 (x), レベル 1 変数 (u), (レベル 0 の) 継続変数 (k) の 3 種類がある．レベル 0 項(e0 )，レベル 1 項 (e1 ) およびレベル 0 の値 (v) を下の通り定義する．

計算規則は以下の通り定義する．

c ::= i | b | int | @ | + | + | if

(λx.e) v → e{x := v}

v ::= x | c | λx.e0 | <e1 >if true then e1 else e2 → e1

e0 ::= v | e0 e0 | if e0 then e0 else e0

if else then e1 else e2 → e2

| λx.e | λu.e
00

λx.e → λu.(e{x := <u>})| reset0 e | shift0 k → e | throw k v
00

λu.<e> → <λu.e>e ::= u | c | λu.e | e e | if e then e else e
1

1

1

1

1

1

1

reset0 v → v
reset0(E[shift0 k → e]) → e{k ⇐ E}

ここで i は整数の定数，b は真理値定数である．

ただし，4 行目の u はフレッシュなコードレベル変数

定数のうち，下線がついているものはコードコンとし，最後の行の E は穴の周りに reset0 を含まないビネータである．変数は，ラムダ抽象 (下線なし，

評価文脈とする．また，この行の右辺のトップレベル

下線つき，二重下線つき) および shift0 により束縛に reset0 がない点が，shift/reset の振舞いとの違い

され，α 同値な項は同一視する．let x = e1 in e2

である．すなわち，shift0 を 1 回計算すると，reset0

および let x = e1 in e2 は，それぞれ，(λx.e2 )e1

が 1 つはずれるため，shift0 を N 個入れ子にするこ(λx.e2 ) @ e1 の省略形である．前述の例でのべた forとにより，N 個分外側の reset0 までアクセスするこは，コード構築定数とコードレベル適用 ∩ を用いてとができ，多段階 let 挿入を実現できるようになる．

導入することとし，(この導入にあたっての型システ

上記における継続変数に対する代入 e{k ⇐ E} は

ムの拡張は容易なので) ここでは省略する．

次の通り定義する．

(throw k v){k ⇐ E} ≡ reset0(E[v])(throw k′ v){k ⇐ E} ≡ throw k′ (v{k ⇐ E})

4. 2 操作的意味論

ただし k ̸= k ′対象言語は，値呼びで left-to-right の操作的意味論を持つ．ここでは評価文脈に基づく定義を与える．
評価文脈を以下のように定義する．

E ::= [ ] | E e0 | v E

上記以外の e に対する代入の定義は透過的であるとする．上記の定義の 1 行目で reset0 を挿入しているのは shift0 の意味論に対応しており，これを挿入し| if E then e else e | reset0 E | λu.Eない場合は別のコントロールオペレータ (Felleisen のコード生成言語で特徴的なことは，コードレベルのcontrol/prompt に類似した control0/prompt0) の振ラムダ抽象の内部で評価が進行する点である．実際，舞いとなる．

00

上記の定義には，λu.E が含まれている．たとえば，

λu.u+[ ] は評価文脈である．

コードコンビネータ定数の振舞い (ラムダ計算における δ 規則に相当) は以下のように定義する．

この評価文脈 E と次に述べる計算規則 r → l により，評価関係 e ⇝ e′ を次のように定義する．
r→lE[r] ⇝ E[l]int n → <n><e1 > @ <e2 > → <e1 e2 ><e1 > + <e2 > → <e1 + e2 >if <e1 > <e2 > <e3 > → <if e1 then e2 else e3 >5 型システム
本研究での型システムについて述べる．
基本型 b，環境識別子 (Environment Classifier)γを以下の通り定義する．

型判断は，以下の 2 つの形である．

b ::= int | boolΓ ⊢L e : t; σγ ::= γx | γ ∪ γ

Γ |= γ ≥ γ

γ の定義における γx は環境識別子の変数を表す．すここで，型文脈 Γ は次のように定義される．

なわち，環境識別子は，変数であるかそれらを ∪ でΓ ::= ∅ | Γ, (γ ≥ γ) | Γ, (x : t) | Γ, (u : t)γ

結合した形である．以下では，メタ変数と変数を区別

型判断の導出規則を与える．まず，Γ |= γ ≥ γ のせず γx を γ と表記する．ここで環境識別子として ∪形に対する規則である．

を導入した理由は後述する．

L ::=| γ は現在ステージと将来ステージをまとめて

Γ |= γ1 ≥ γ1表す記号である．たとえば，Γ ⊢ e : t ; σ は，L =Γ, γ1 ≥ γ2 |= γ1 ≥ γ2L

Γ |= γ1 ≥ γ2 Γ |= γ2 ≥ γ3
Γ |= γ1 ≥ γ3のとき現在ステージの判断で，L = γ のとき将来ステージの判断となる．
レベル 0 の型 t0 ，レベル 1 の型 t1 ，(レベル 0 の)型の有限列 σ, (レベル 0 の) 継続の型 κ を次の通り定Γ |= γ1 ∪ γ2 ≥ γ1

Γ |= γ3 ≥ γ1 Γ |= γ3 ≥ γ2
Γ |= γ3 ≥ γ1 ∪ γ2

義する．
σt0 ::= b | t0 → t0 | ⟨t1 ⟩γ
t1 ::= b | t1 → t1
σ ::= ϵ | σ, t0

Γ |= γ1 ∪ γ2 ≥ γ2

次に，Γ ⊢L e : t; σ の形に対する導出規則を与える．まずは，レベル 0 における単純な規則である．

σκ0 ::= ⟨t1 ⟩γ ⇒ ⟨t1 ⟩γ
σ

レベル 0 の関数型 t0 → t0 は，エフェクトをあらわ

Γ, x : t ⊢ x : t ; σ

す列 σ を伴っている．これは，その関数型をもつ項をΓ ⊢L c : tc ; σ

引数に適用したときに生じる計算エフェクトであり，
具体的には，shift0 の answer type の列である．前Γ ⊢ L e 1 : t2 → t1 ; σ

述したように shift0 は多段階の reset0 にアクセスできるため，n 個先の reset0 の answer type まで記憶するため，このように型の列 σ で表現している．ただし，本研究の範囲では，answer type modification に対応する必要はないので，エフェクトはシンプルに型

Γ, (u : t)γ ⊢γ u : t ; σΓ ⊢L e2 : t2 ; σΓ ⊢L e1 e2 : t1 ; σΓ, x : t1 ⊢ e : t2 ; σΓ, (u : t1 )γ ⊢γ e : t2 ; σΓ ⊢ λx.e : t1 → t2 ; σ ′Γ ⊢γ λx.e : t1 → t2 ; σ ′σΓ ⊢L e1 : bool; σΓ ⊢L e2 : t; σΓ ⊢L e3 : t; σの列 (n 個先の reset0 の answer type を n = 1, · · · , kΓ ⊢ if e1 then e2 else e3 : t ; σに対して並べた列) で表現している．この型システム

次にコードレベル変数に関するラムダ抽象の規則の詳細は，Materzok ら [3] の研究を参照されたい．
本稿の範囲では，コントロールオペレータは現在ステージのみにあらわれ，生成されるコードの中にはあらわないため，レベル 1 の関数型は，エフェクトを表す列を持たない．また，本項では，shift0/reset0 は
コードを操作する目的にのみ使うため，継続の型は，コードからコードへの関数の形をしている．ここでは，後の定義を簡略化するため，継続を，通常の関数とは区別しており，そのため，継続の型も通常の関数の型とは区別して二重の横線で表現している．

L

である．

Γ, γ1 ≥ γ, x : ⟨t1 ⟩γ1 ⊢ e : ⟨t2 ⟩γ1 ; σ(γ1 is eigen var)Γ ⊢ λx.e : ⟨t1 → t2 ⟩γ ; σΓ, γ1 ≥ γ, x : (u : t1 )γ1 ⊢ e : ⟨t2 ⟩γ1 ; σΓ ⊢ λu1 .e : ⟨t1 → t2 ⟩γ ; σ
コントロールオペレータに対する型導出規則である．

Γ ⊢ e : ⟨t⟩γ ; ⟨t⟩γ , σΓ ⊢ reset0 e : ⟨t⟩γ ; σσΓ, k : ⟨t1 ⟩γ1 ⇒ ⟨t0 ⟩γ0 ⊢ e : ⟨t0 ⟩γ0 ; σ Γ |= γ1 ≥ γ0
Γ ⊢ shift0 k → e : ⟨t1 ⟩γ1 ; ⟨t0 ⟩γ0 , σΓ ⊢ v : ⟨t1 ⟩γ1 ∪γ2 ; σΓ,Γ |= γ2 ≥ γ0σ
k : ⟨t1 ⟩γ1 ⇒ ⟨t0 ⟩γ0 ⊢ throw k v : ⟨t0 ⟩γ2 ; σ

コード生成に関する補助的な規則として，Sub-

sumption に相当する規則等がある．
Γ ⊢ e : ⟨t⟩γ1 ; σ Γ |= γ2 ≥ γ1Γ ⊢ e : ⟨t⟩γ2 ; σΓ ⊢γ1 e : t ; σ Γ |= γ2 ≥ γ1
Γ ⊢γ2 e : t ; σできれば) 進行 (Progress) 定理とあわせて型システ
ムの健全性を導く定理である．

(型保存性) ⊢ e : t ; σ かつ e ⇝ e′ であれば，⊢ e′ : t ; σ である．
この定理は reset0-shift0 の計算規則が多相性を持たない場合には容易に証明できるが，多相性については精密な扱いが必要であり，現段階では，型保存定理の証明は進行中である．

6 まとめと今後の課題
本研究では，効率的コード生成に有用な技法であΓ ⊢ e : t ;σる let 挿入を，型安全に実現するための言語と型シΓ ⊢ <e> : ⟨t ⟩ ; σ

ステムについて述べた．局所的な代入可能変数を持

γ

1

1 γ

つ体系に対する須藤らの研究 [5] などに基づき，多段

5. 1 型付け例

階の for ループを飛び越えた let 挿入を実現するため

上記の型システムのもとで，いくつかの項の型付けに，shift0/reset0 を持つコード生成体系を設計した．

について述べる．

須藤らの研究で精密化された環境識別子 (Environ-ment Classifier) に join (∪) を導入することで，計
e1 = reset0 let x1 = %3 in

算の順序を変更するようなコントロールオペレータ

reset0 let x2 = %5 in（shift0/reset0）を扱えるようにし，安全に多段階のshift0 k → let y = t in

let 挿入を行えるように型システムを構築した．このthrow k (x1 + x2 + y)

ような let 挿入が束縛子を越えるケースは，ループに

この式 e1 に対して，もし，t = %7 あるいは t = x1

おける不変式の括り出しなどの有用な最適化を含むであれば，e1 は型付け可能である．一方，t = x2 でが，これまでの研究では一般的な let 挿入を安全に実あれば，e1 は型付けできない．

現した体系の提案はなく，我々の知る限り本研究がはじめてである．

e2 = reset0 let x1 = %3 in

今後の課題として，まずあげられるのは，進行

reset0 let x2 = %5 in(Progress) の性質および型推論アルゴリズムの開発

shift0 k2 → shift0 k1 → let y = t inである．また，理論的には Kiselyov らのグローバル

throw k1 (throw k2 (x1 + x2 + y))

な参照を持つ体系との融合が可能になれば，広い範囲

この式 e2 に対して，もし t = %7 であれば e1 は型のコード生成技法・最適化技法をカバーできるため極付け可能である．一方，t = x2 あるいは t = x1 であめて有用である．また，既存の MetaOCaml との比

れば，e1 は型付けできない．

較においては，2 レベルのみのコード生成に限定してこのように，(少なくとも) 上記の例については安いる点や run (生成したコードの実行) や cross-stage

全な式と危険な式を正しく峻別できていることがわ

persistence (現在ステージの値をコードに埋め込む機

かった．

能) などに対応していない点が欠点であり，これらの拡張が可能であるかどうかの検討は非常に興味深い

5. 2 型安全性について
本研究の型システムに対する型保存 (Subject Re-

duction) 定理について述べる．型保存定理は，(証明

将来課題である．
謝辞 本研究は，JSPS 科研費 15K12007 の支援を受けている．

参 考 文 献[1] Kameyama, Y., Kiselyov, O., and Shan, C.-c.:
Shifting the Stage: Staging with Delimited Control,
Proceedings of the 2009 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM ’09, New York, NY, USA, ACM, 2009,
pp. 111–120.
[2] Kiselyov, O., Kameyama, Y., and Sudo, Y.: Refined Environment Classifiers: Type- and Scope-safe
Code Generation with Mutable Cells, Proceedings ofthe 14th Asian Symposium on Programming Lan-guages and Systems, APLAS 2016, to appear.
[3] Materzok, M. and Biernacki, D.: Subtyping Delimited Continuations, SIGPLAN Not., Vol. 46,
No. 9(2011), pp. 81–93.
[4] Taha, W. and Nielsen, M. F.: Environment Classifiers, Proceedings of the 30th ACM SIGPLANSIGACT Symposium on Principles of Programming
Languages, POPL ’03, New York, NY, USA, ACM,
2003, pp. 26–37.
[5] 須藤悠斗, Kiselyov, O., 亀山幸義: コード生成のための自然演繹. 日本ソフトウェア科学会第 31 回大会,
2014 年 9 月, 名古屋大学. PPL4-4, 9 ページ.