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

緩い値制限に基づく多相と副作用を含むコード生成言
語の型システム
菊地 綾音

亀山 幸義

本研究では，多相と副作用を含むコード生成言語を対象とする型システムを提案する．通常の ML 系言語では，参照が多相型を持ち実行時型エラーを引き起こすという危険性を値制限により型システムで防ぐことができたが，コード生成言語の一つであるマルチステージ言語では不十分であることが知られている．先行研究では，型変数を命令的型変数と作用的変数に分けて一般化できる型変数を制限するという Tofte の手法を拡張してマルチステージ言語に適用し，型安全な体系を構築した．一方，我々はマルチステージ言語 MetaOCaml で用いられている値制限および緩い値制限という制限手法に基づき，ステージを移動する項に含まれる型変数に制限を加えることによって，MetaOCaml に組み込みやすくシンプルな型システムの構築を目指す．

ルチステージ言語は，型安全でないことが知られてい

1 はじめにる [5]．

マルチステージプログラミング [6] は，プログラム

これは，OCaml および MetaOCaml において多相の抽象化と実行効率を両立することができるコード

化する項を制限するために用いられている値制限が生成手法である．プログラムの抽象化は，開発効率や原因である．値制限 (value restriction) は，let 束縛

保守性を向上させるという利点があるが，一方で実行された変数が多相型を持つための条件の 1 つであり，効率の低下を伴う．マルチステージプログラミングを

let 変数に束縛される項を構文的値 (syntactic value)用いると，汎用的で再利用性に優れた高レベルなプロに限るという制約である [9]．ラムダ式は構文的値でグラムから，あるパラメータに特化した効率の良いプ

あり値制限の制約を満たす．コード生成機能を含まなログラムを生成することで，プログラムの抽象化によい言語では構文的値は内部に計算を含まないため，多るオーバーヘッドを削減することが可能となる．

相型を持たせても型安全性は満たされた．一方，マル

コード生成において，生成されるコードが正しくチステージ言語ではラムダ式の内部に計算を含む可動作するという性質を満たすことは非常に重要であ能性があり，多相型を持たせると型安全でなくなる例

る．MetaOCaml を筆頭とする MetaML 系のマルチがある．

ステージプログラミングを支援する機構を持つ言語

OCaml および MetaOCaml には緩い値制限 (re-(以下，マルチステージ言語と呼ぶ) では，副作用をlaxed value restriction) という 値制限とは別の条件含まないコードの型安全性は保証されている [1, 7]．

による let 多相の規則がある．[3] 値制限が項の構文

しかし，プログラムの再利用性を高める多相 (poly-に着目した制限であるのに対して，緩い値制限は項

morphism) と，プログラムの実行効率を向上させるの型に着目した制限であるという著しい違いがあり，参照 (reference) という 2 つの有用な機能を加えたマ

緩い値制限による let 多相は，値制限による let 多相Type System based on Relaxed Value Restriction for
Code Generation with Polymorphism and Reference
Ayane Kikuchi, Yukiyoshi Kameyama, 筑波大学大学院
システム情報工学研究科コンピュータサイエンス専攻,
Dept. of Computer Science, University of Tsukuba.

ではカバーされない項の多相化において有益である．
小林ら [10] は，Tofte の手法 [8] に基づいて，多相および参照を備えたマルチステージ言語に対する型安全な型システムの構築に成功した．Tofte の手

法は多相的な参照を防ぐ制限手法の一つであるが，マルチステージ言語でもそのまま let 多相を許容しMetaOCaml および OCaml で用いられている値制限

ようという提案である．Kiselyov の非ステージ化変とは方向性が異なるため，小林らの手法をそのまま

換変換の存在は，緩い値制限による let 多相をもつ

MetaOCaml に取り込むことはできない．

MetaOCaml が型安全性をもつことを示唆しており，

Kiselyov [5] は，MetaOCaml から OCaml への非本研究ではそのことを示す．Garrigue は，OCaml のステージ化変換を提案し，非ステージ化変換を用いコアに緩い値制限による let 多相を加えた体系の型安て様々な制限のもとでの多相 let を含むコード生成言

全性を，部分型をもつシステムへの帰着によって証明

語の型安全な実装について考察を行った．彼は緩いした [3] が，そこでの型安全性は，いわゆる主部簡約

値制限のもとでの多相 let をに対しては変換に成功し定理 (Subject Reduction Theorem) を経由しないとたが，値制限に対しては型安全な変換とはならなかっいう意味で非標準のものであった．同じ論文で，Gar-た．また，変換が型や意味を保存するという性質の証

rigue は別の方法として，型システムに Subsumption

明は与えられていない．

規則を追加した場合には主部簡約定理が成立するこ本研究では，現在の MetaOCaml に取り込みやすとを示唆している．本研究は後者の方法にならって，い形で多相と参照を含むコードを安全に生成するため構文的手法で主部簡約定理および型安全性を示す．

の型システムを構築することを目指す．具体的には，

上記の 2 つの提案をあわせもつ本研究の体系と，命令的型変数など MetaOCaml にない機能を用いず，先行研究の小林らの体系とは型付けできる項の範囲

値制限および緩い値制限と高い親和性を持つ形でコーが比較不能である．しかし，現在の MetaOCaml がド生成機能を持つ言語に対して型安全な多相 let 式を

OCaml の拡張として実装されていることを考えると，導入することを目的とする．本研究のベースとなる体OCaml の型システムとの相性がよい本研究の手法が系は，値制限より制限した let 多相のみを持つ体系で相対的に有利であると考える．

ある．すなわち，let 多相で束縛される式を構文的値でかつコード埋め込みの構文を含まないものに限定

2 準備するものである．これは強い制限であるが，コード生

2. 1 マルチステージプログラミング

成機能のない MetaOCaml の値制限に対応しており，

マルチステージプログラミング (MSP) [6] は，プ型安全性を持つことが厳密に証明できる．
我々は，この体系を以下の 2 種類の方法で拡張する．第 1 の方法は，値制限を念頭に置いた拡張であログラムを生成するステージ，実行するステージなどの複数のステージに分けてコードを生成するメタプ
ログラミングの一種である．

り，let 多相で束縛される式として構文的値 (コード

通常のプログラムではすべての計算を実行時に行埋め込み構文を含んでよい) を許すが，マルチステー

うが，マルチステージプログラミングでは次節で述べ

ジ構成子である Cross-Stage Persistence (CSP，ス

るコード生成のための構成子をプログラムに加える

テージを越えた値の埋め込み) の対象となる項を基本

ことで，プログラム中の計算を実行時よりも後に遅延型のものに制限する．この制限は，MetaOCaml におさせることができ，遅延された計算をコードとして出ける型安全性の反例となる式から着想を得たもので力することができる．

あり，CSP の対象となる項の多相性を制限することプログラムは計算を行うタイミングによってステー

によって 値制限の制限による let 多相が型安全にな

ジ (段階) が分かれており, ステージをレベルともいるのではないかという予想をした．この体系の型安全う．現在の段階はコードを生成する段階でありこれを性は本稿執筆時点では証明中である．

レベル 0 とする．生成されるコードは将来計算が行第 2 の方法は，緩い値制限をそのままマルチステー

われるステージでありレベル 1 となる．MetaOCaml

ジ言語で用いるものである．すなわち，let 多相で束など一般のマルチステージ言語ではコードの入れ子

縛される式の型が緩い値制限を満たしているとき，が許されているため，コードのコードはレベル 2 となるが，本稿では、簡単化のため、レベル 0 とレベル

1 のみを許すことにする．

3 背景
3. 1 値制限を MetaML へ適用したときの問題

2. 2 MetaOCaml によるコード生成記法

MetaOCaml では型がつくが，実行時型エラーとな

マルチステージ言語 MetaOCaml では，コードをるプログラムとして，参照，多相型，およびコード

生成するための構成子 Bracket, Escape, Run を提供

生成構成子を組み合わせたプログラムが考えられる．

している．

プログラム 2 は，コード生成機能によって，現在メモ

Bracket (.<e>.)：項 e の評価を遅延させてコーリ上に確保された参照をコードに埋め込み (.∼(csp

ドを生成する．コードは現段階では実行されず，(ref [])))，異なる 2 つの型で共有しているためコー値として扱われる．項 e が τ 型を持つとするとド生成時に型エラーとなるべき例である．しかし，値コードの型は τ code 型となる．

制限によって変数 f は値とみなされ多相型が付くた

Escape (.~e)：Bracket で囲まれたコードの中にめ危険なコードが生成されてしまい，コードを実行す

コード e を埋め込むときに使う．

るときに型エラーが発生する．

Run (!.e)：コード e をコンパイルして実行する構成子である．
この 3 つの構成子を用いた例をプログラム 1 に示す．
プログラム 1 コード生成構成子の使用例# let c = . <2+3 >.;;
val c : int code = . <2+3 >.
# let cc = . <.~ c * .~ c >.;;
val cc : int code = . <(2+3) *(2+3) >.
# open Runcode ;;# !. cc ;;- : int = 25

プログラム 2 多相，参照，コード生成の組合わせ# let csp x = . <x >. ;;val csp : ’a -> ’a code = <fun ># let c =. < let f () =.~( csp ( ref []) ) inf () := [1]; " abc " :: !( f () )>.;;# run c ;;~ > segmentation fault

3. 2 先行研究
プログラム 1 において，c は 2+3 という式のコードであり，計算が遅延されていることが確認できる．cc では Escape を用いて c が 2 回埋め込まれている．コードを実行する構成子は Runcode モジュールの中で定義されているため，実行するには Runcode.run(e)もしくは Runcode モジュールを開いた後!.(e) と記
述する．
コード生成のための上記 3 つの構成子の他に，CSP(Cross-Stage Persistence) と呼ばれる機構が存在す
る．CSP はマルチステージプログラミングにおいて値を複数のステージで共有することを意味する．特に2 ステージの場合は，プログラムを生成する段階 (現小林らは，この問題の解決策として Tofte が考案した制限手法 [8] に基づく型システムを提案した [10]．

Tofte の手法は，型変数を作用的型変数と命令的型変数に分け，安全な作用的型変数のみを一般化できる
ように制限する方法である．小林らは，この手法を

λ▷% を拡張したマルチステージ言語に適用し，将来確保される参照のみ多相化して良いという制限を新たに加えて拡張し，型安全性を証明した．しかし，Tofteの手法は OCaml および MetaOCaml が採用している値制限や緩い値制限と方向性が異なるため、小林らの制限手法を既存の MetaOCaml 処理系への追加として実装することが困難であるという問題がある．

在のステージ) で生成した値を，生成するプログラム(将来のステージ) の中で使うことを指す．

4 提案手法
本研究では，多相と参照を含む型安全なマルチス
テージ言語を構築するための let 多相に対する適切な

制限を 3 つ提案する．

た関数 (コンパイル済み関数) を CSP の対象としても問題ないと予想される．ただし，これらについての

4. 1 強い値制限

詳細な検討および証明は今後の課題である．

ベースとなる最も制限が強い制限として，強い値制限について述べる．強い値制限は，多相化できる項を

4. 3 緩い値制限

構文的値であって Escape や CSP を含まないものにOCaml および MetaOCaml で使われている制限と制限する手法である．前述した通り，マルチステージ

して，値制限の他に緩い値制限 [3] がある．緩い値制

言語では，コード挿入 (Escape) を含む関数は，その限は，値制限で多相型がつかない項の多相を復活さ

内部に計算を持つため値ではない．

せるために，項の型に着目して，正の位置 (covariant
position)†1 のみに出現する型変数を多相化するとい

# let
val c
# let
val f

c
:
f
:

プログラム 3 内部に計算を含む関数= . <2 + 3 >. ;;int code = . <2 + 3 >.
= fun x -> . <.~ c * x >.;;
int -> int code = <fun >う手法である．
本研究では，緩い値制限による多相型の導入を提案
体系 PolyMetaML でもそのまま適用する．これは，非ステージ化変換 [5] によって MetaML から ML に

このような関数に多相型を与えると型安全性が壊れる

変換する手法が与えられており，この変換は正の位置

例が作れてしまう．一方，構文的値であって Escapeを変えないため，変換後も多相性が保存される，といや CSP を含まないものは，内部に計算を含まず，多う予想によるものである．後の節では，緩い値制限に相型を持たせても型安全性は壊れない．このように，よる let 多相をもつ型システムが型安全性を持つこと

構文的値より強い制限を強い値制限と呼び，強い値制を示す．

限のもとでの let 多相は型安全である．

5 提案言語 PolyMetaML
4. 2 値制限
ベースとなる体系の拡張として，値制限による let
多相を考える．
この場合，他に何の制限もなければ型安全性が成立しない反例があるため，何らかの制限が必要である．

本研究で提案する PolyMetaML は，時相論理に基づくマルチステージ計算体系 λ◦ [2] を基にした体系に，多相と参照を追加したマルチステージ言語である．本章では，PolyMetaML の構文および操作的意
味論を定義する．

小林らはこの目的のため，Tofte の方法にならい，参本研究では型安全に let 式を追加するための手法を照 (reference) による副作用に関係する場所で現れる

2 つ提案した．2 つの手法を導入した体系を組み立て

型変数を「命令的型変数」と呼び，「命令的型変数」がる定義はほぼ共通であるが，構文と型システムの定義

多相型できなよう制限を加えた．このような制限のもは少し異なることに注意されたい．以降では，強い値とで，型システムの安全性を証明した．

制限を導入した体系は PolyMetaML1 ，CSP を単相

本研究では，MetaOCaml の型システムそのものを変更することなく，型安全なシステムを構築することを目的としているので，Tofte の方法を取ることはできない．検討の結果，CSP を適用する項を基本型の値に限定することにより，let 多相の対象は構文的値のままであっても，型安全性が保証されるのではない
かという着想を得た．具体的には，たとえば，CSP
対応の型を基本型 (整数型や文字列型など) の定数に限定すればよい．また，外部のモジュールで定義されに制限する体系は PolyMetaML2 と呼び，個別の定義が必要な場合は分けて定義する．
定義 1 (構文)図 1 に，PolyMetaML の構文を示す．PolyMetaML
は 2 つのステージから構成される言語で，ステージのレベルは数字によって表す．
「レベル 0」はコード生成†1 OCaml の実際の型システムでは，Principal Typeの観点から，型変数が strictly positive な位置に出現する場合の限定している．

ステージ，「レベル 1」はコード実行ステージを表す．
以下ではレベルを表すメタ変数として i を使う．本稿の範囲では，i ∈ {0, 1} である．

ei , v i , τ i はそれぞれレベル i の項，値，型である．
Γ は型環境を表し，変数と型およびそのレベルの 3 つ組からなる有限列である．x は対象言語における変数，c は定数を表すメタ変数である．ℓ は参照によって確保されるメモリ上のロケーションを表す．b は基底型であり，多相型は (x : ∀α1 · · · αn .τ i ) で表す．

PolyMetaML1 が既存のマルチステージ言語と異なる点は，v 0 に含まれる λ 抽象の本体が一般の式

e0 ではなく，マルチステージ構成子を含まない式
e0λ のみに制限されている点である．これは，第 4 章
で述べた強い値制限を反映するためである．一方，PolyMetaML2 は値制限に基づいており，マルチス
テージ構成子を含む λ 抽象も値となるため何も制限されておらず，既存のものと差異はない．

共通の構文

eicommon ::= x | c | λx.ei | ei ei | unit | ref ei | !ei| ei := ei | ℓ | let x = ei in ei
e0 ::= eicommon (i = 0) | ⟨e1 ⟩
e1 ::= eicommon (i = 1) |∼ e0 | %e0v 1 ::= x | c | λx.v 1 | v 1 v 1 | unit | ref v 1 | !v 1
| v 1 := v 1 | ℓ | let x = v 1 in v 1
τ ::= b | τ 0 → τ 0 | unit | τ 0 ref | τ 1 code0

τ 1 ::= b | τ 1 → τ 1 | unit | τ 1 refΓ ::= ϵ | Γ, (x : τ )i
PolyMetaML1
e0λ ::= eicommon (i = 0) | ⟨eicommon ⟩ (i = 1)v 0 ::= x | c | unit | λx.e0λ | ℓ | ⟨v 1 ⟩⟨⟩, ∼ はそれぞれマルチステージプログラミングの構成子 Bracket と Escape に対応する．現時点では，

Run に対応する構成子は PolyMetaML にはない．%
は CSP のための構成子である．

PolyMetaML2
v 0 ::= x | c | unit | λx.e0 | ℓ | ⟨v 1 ⟩次に，PolyMetaML1 および PolyMetaML2 に対する操作的意味論を定義する．これらの体系は値呼び
図1で left-to-right の操作的意味論を持つ．

PolyMetaML の構文

定義 2 (評価文脈)

定義 4 (簡約規則)

図 2 は，PolyMetaML の評価文脈である．Eji におけ

PolyMetaML の簡約関係は，以下のように項とストる i は評価文脈があるステージのレベル，j は □ のアの組によって定義される．

レベルを表す．

Ei0 [e] | µ ⇝ Ei0 [e′ ] | µ′定義 3 (ストア)参照によって確保されたロケーションと，ロケーショ

簡約規則を図 3 に示す。トップレベルでは，自由変数ンに格納されている値との対応関係を保持するストおよび ℓ を含まないものとする．提案言語では，コー

ア µ を定義する．

ドに含まれる変数がスコープの外に飛び出して自由変• µ に新しい値 v を追加したストアは，(µ, ℓ 7→ v)

数となってしまうという Scope Extrusion の問題 [4]と表す．ここで，ℓ は µ に含まれないロケーショについては取り扱わないため，代入される値に自由変ンとする．

数が含まれていた場合 (v に含まれる自由変数の集合• µ に含まれる既存のロケーション ℓ の値を v に更新したストアは µ{ℓ := v} と表す．

F V (v) が空集合でない場合) は E-AssignW 規則に
よって Wrong という値 (実行時エラーを意味する)になる．

E00 [(λx.e0 ) v 0 ] | µ ⇝ E00 [e0 [x := v 0 ]] | µ
E00 [ref v] | µ ⇝ E00 [ℓ] | (µ,ℓ 7→ v)(E-Ref)

E00 [ℓ := v] | µ ⇝ E00 [unit] | µ{ℓ := v}

if F V (v) = ∅(E-Assign)

E00 [ℓ := v] | µ ⇝ Wrong | µ

if F V (v) ̸= ∅(E-AssignW)

E00 [ref v] | µ ⇝ E00 [ℓ] | (µ,E00 [(let x(E-β)ℓ 7→ v)(E-Ref)

E00 [ !ℓ] | µ ⇝ E00 [µ(ℓ)] | µ(E-Deref)v in e ] | µ ⇝ E00 [e0 [x := v 0 ]] | µ(E-Let)0=

E10 [∼ ⟨v 1 ⟩] | µ ⇝ E10 [v 1 ] | µ(E-CodeCxl)

E10 [%v 0 ] | µ ⇝ E10 [v 0 ] | µ

図3(E-Csp)PolyMetaML の簡約規則

E00 ::= □ | E00 e0 | v 0 E00 | ref E00 | !E00 | E00 := e0

付け Σ，項 e，型 τ ) で定義される．⊢i 中の i は，この型付けが導出できるステージのレベルを表す．

| v 0 := E00 | let x = E00 in e0 | ⟨E01 ⟩E10 ::= E10 e0 | v 0 E10 | ref E10 | !E10 | E10 := e0|v:= E10 | let x0=

Γ; Σ ⊢i ei : τ i

E10 in e0 | ⟨E11 ⟩E01 ::= E01 e1 | v 1 E01 | ref E01 | !E01 | E01 := e1| v 1 := E01 | let x = E01 in e1 |∼ E00 | %E00
E11 ::= □ | E11 e1 | v 1 E11 | ref E11 | !E11 | E11 := e1| v 1 := E11 | let x = E11 in e1 |∼ E10 | %E10

型付け規則を定義するための準備として，4 つの型
変数の集合を定義する．
定義 7 (条件付き型変数の集合)型 τ に自由出現する型変数の集合 FTV(τ ) を以下のように定義する．

図2

PolyMetaML の評価文脈

FTV(α) = {α}FTV(b) = ∅FTV(τ1i → τ2i ) = FTV(τ1i ) ∪ FTV(τ2i )6 提案言語 PolyMetaML に対する型シス
テム
まず，PolyMetaML の型付け関係を定義する前に，ストア中の値の型付けを行うためのストア型付けを定義する．
定義 5 (ストア型付け)
ストア µ についてのストア型付けは，メタ変数 Σ で定義される．

• ストア型付け Σ に，ロケーション ℓ が τ 型を持つという対応を追加したストアを，(Σ, ℓ 7→ τ )と表す．ここで，ℓ は Σ に含まれないロケーショ
ンとする．
定義 6 (型付け関係)
型付け関係は，以下の四項関係 (型環境 Γ，ストア型

FTV(τ i ref) = FTV(τ i )FTV(τ i code) = FTV(τ i )また，緩い値制限を型システムに反映させるために，次の 3 つの型変数の集合を定義する．
型 τ の covariant な 位 置 に 現 れ る 型 変 数 の 集 合

T V + (τ ) を以下のように定義する．
T V + (α) = {α}T V + (b) = {b}T V + (unit) = ∅T V + (τ1i → τ2i ) = T V − (τ1i ) ∪ T V + (τ2i )T V + (τ i ref) = ∅T V + (τ i code) = T V + (τ i )型 τ の contravariant な位置に現れる型変数の集合

T V − (τ ) を以下のように定義する．

げる (CSP) ための規則である．PolyMetaML は 2 ス−

T V (α) = ∅テージのため，項の型をコード型を含まない τ 1 に制

T V − (b) = ∅限し，コードに CSP を適用できないようにしてい−T V (unit) = ∅TV−る．PolyMetaML2 の T-CspMono 規則は，CSP が(τ1i → τ2i ) = T V + (τ1i ) ∪ T V − (τ2i )−適用された項を単相型にするという制限を T-Csp 規

T V (τ ref) = ∅−i

則に加えた規則となっている．
−

ii

T-Wrong 規則は，Scope Extrusion の問題が発T V (τ code) = T V (τ )生し，Wrong(実行時エラーを意味する) となったと型 τ の no-variant な型変数の集合 T V no (τ ) を以

緩い値制限に基づく型システムの健全性を保証す

下のように定義する．

TV(α) = ∅

TV

no

TV

no

no

きに適用する規則である．

るために，以下の subsumption 規則を導入する．

(b) = ∅

Γ; Σ ⊢i e : τ [zero/α1 , · · · , zero/αn ](unit) = ∅(T-Subsumption)
Γ; Σ ⊢i e : τ(*): {α1 , · · · , αn } ∩ (T V − (τ ) ∪ T V no (τ )) = ∅T V no (τ1i → τ2i ) = T V no (τ1i ) ∪ T V no (τ2i )T V no (τ i ref) = FTV(τ i )ここで型 zero は、その要素となる値を持たない型

T V no (τ i code) = T V no (τ i )(空の型) を表す型定数であり、これも基本型に含めるものとする。型 zero に対する規則は上記のものだ型文脈 Γ 中で自由に出現する型変数の集 合 FTV(Γ) は 、FTV((x : ∀α1 · · · αn .τ ) )i i=

FTV(τ ) \ {α1 , . . . , αn } により定める。
i

定義 8 (型付け規則)
型付け規則を図 4 に示す．これらの型付け規則は，けである．これは，Garrigue が緩い値制限を導入した体系で型保存定理が成り立つことを証明するために加えた規則をもとにしている．subsumption 規則を導入した PolyMetaML の体系でも次章で述べる型システムの健全性定理が成り立つ．

ベースとなる共通の型システム，PolyMetaML1 の型システム，PolyMetaML2 の型システムで用いられる

7 型システムの健全性

ものの 3 種類に分かれる．

第 6 章で定義した型システムの健全性を保証する

ここでは，いくつかの重要な規則に関して説明する．

T-LetV 規則は，let 式において変数 x に束縛する項が値であったときに適用できる規則で，PolyMetaML2
では値制限，PolyMetaML1 では強い値制限によって，

Γ および Σ に含まれる自由な型変数を除いた τ 中の自由な型変数を多相化できる．一方，PolyMetaML1
のみに含まれる T-Let 規則は，let 式において変数x に束縛する項が値ではないときに適用する規則であための，主部簡約 (Subject Reduction) 定理と進行(Progress) 定理について述べる．
定義 9 (ストアの正しい型付け)
ストア µ が，Σ に関して正しく型付けされているとは，dom(µ) = dom(Σ) かつ，任意の ℓ ∈ dom(µ) に対して ∅; Σ ⊢i µ(ℓ) : Σ(ℓ) が導出できることをいい，

Σ ⊢i µ で表す．

る．こちらは緩い値制限に基づいて多相化する規則で

PolyMetaML1 および PolyMetaML2 の型システ

あり，T-LetV 規則に比べて多相化できる条件が厳ムに対して，以下の共通の 2 つの定理が成り立つこ

しくなっている．contravariant な位置にある，もしとが期待される．

くは no-variant である型変数以外の型変数が多相化できる．

T-Csp 規則は，レベル 0 の項をレベル 1 に持ち上定理 1 (主部簡約)

Γ; Σ1 ⊢i ei1 : τ i が成り立ち，Γ 中にレベル 0 の変数

は出現せず，ei1 | µ1 ⇝ ei2 | µ2 かつ Σ1 ⊢ µ1 ならば，Γ; Σ2 ⊢iei2 : τ i かつ Σ2 ⊢ µ2 かつ Σ1 ⊆ Σ2 となるような Σ2 が存在する．
定理 2 (進行)Γ; Σ ⊢i ei : τ i ならば，ei = v i となるような v i が存在するか，あるいは ei | µ1 ⇝ ei2 | µ2 となるような

ei2 と µ2 が存在する．
PolyMetaML2 の型システムでは，定理 1 が成り立つことを証明した．定理 2 については証明中である．

PolyMetaML1 に対する型システムは，緩い値制限
による多相 let の型付け規則 (T-Let 規則) が含まれているため，素朴に主部簡約定理を証明することは難しい．したがって，Garrigue が提案した Subsump-tion 規則を追加する手法によって構文的な主部簡約定理の証明を行う．

8 まとめと今後の課題
本研究では，参照による副作用を含むコード生成言
語に let 多相による多相型を型安全に加えるために，
値制限を修正した制限手法と 緩い値制限による制限
手法の 2 つを提案した．また，これらに基づき，多相と参照を含むコード生成言語 PolyMetaML およびそれに対する型システムを設計した．本研究の提案は、既存の OCaml や MetaOCaml と親和性の高いシン
プルな制約のもとでの多相型を実現するものである。
今後は，PolyMetaML 全体の健全性を保証することと言語の実装を行う予定である。

参 考 文 献[ 1 ] Calcagno, C., Moggi, E., and Taha, W.: MLLike Inference for Classifiers, Programming Lan-guages and Systems, 13th European Symposium on
Programming, ESOP 2004, Held as Part of the
Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain,
March 29 - April 2, 2004, Proceedings, 2004,
pp. 79–93.
[ 2 ] Davies, R.: A Temporal-Logic Approach to
Binding-Time Analysis, Proceedings, 11th AnnualIEEE Symposium on Logic in Computer Science,
New Brunswick, New Jersey, USA, July 27-30,
1996, 1996, pp. 184–195.
[ 3 ] Garrigue, J.: Relaxing the Value Restriction,
Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Nara, Japan,
April 7-9, 2004, Proceedings, 2004, pp. 196–213.
[ 4 ] Kameyama, Y., Kiselyov, O., and Shan, C.:
Shifting the stage: staging with delimited control,
Proceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based
Program Manipulation, PEPM 2009, Savannah,
GA, USA, January 19-20, 2009, 2009, pp. 111–
120.
[ 5 ] Kiselyov, O.: Generating Code with Polymorphic let: A Ballad of Value Restriction, Copying and Sharing, Proceedings ML Family / OCaml
Users and Developers workshops, ML Family/OCaml 2015, Vancouver, Canada, 3rd & 4th September 2015., 2015, pp. 1–22.
[ 6 ] Taha, W.: A Gentle Introduction to Multi-stage
Programming, Domain-Specific Program Generation, International Seminar, Dagstuhl Castle, Germany, March 23-28, 2003, Revised Papers, 2003,
pp. 30–50.
[ 7 ] Taha, W. and Nielsen, M. F.: Environment classifiers, ACM SIGPLAN Notices, Vol. 38, No. 1,
ACM, 2003, pp. 26–37.
[ 8 ] Tofte, M.: Type Inference for Polymorphic References, Inf. Comput., Vol. 89, No. 1(1990), pp. 1–
34.
[ 9 ] Wright, A. K. and Felleisen, M.: A Syntactic Approach to Type Soundness, Inf. Comput., Vol. 115,
No. 1(1994), pp. 38–94.
[10] 小林恵, 五十嵐淳: 参照を備えた多段階計算のための多相的型システム, 日本ソフトウェア科学会大会論文集, Vol. 32(2015), pp. 1–11.

共通の型付け規則(x : τ1 )i ∈ Γ

τ1 ≥ τ2i≤jΓ; Σ ⊢ x : τ2jΓ, (x : τ1 )i ; Σ ⊢i e : τ2
Γ; Σ ⊢i λx.e : τ1 → τ2
Γ; Σ ⊢i e1 : τ1 → τ2

(T-Var)(T-Lam)Γ; Σ ⊢i e2 : τ1

Γ; Σ ⊢i e1 e2 : τ2
Γ; Σ ⊢i i : int
Γ; Σ ⊢i b : bool
Γ; Σ ⊢i v1 : τ1

(T-App)(T-Int)(T-Bool)Γ, (x : ∀α1 · · · αn .τ1 )i ; Σ ⊢i e2 : τ2

(T-LetV)Γ; Σ ⊢i let x = v1 in e2 : τ2
ただし，α1 , · · · , αn ∈ FTV(τ1 ) − FTV(Γ) − FTV(Σ)Γ; Σ ⊢i e : τ(T-Ref)Γ; Σ ⊢i ref e : τ refΓ; Σ ⊢i e1 : τ refΓ; Σ ⊢i e2 : τ

Γ; Σ ⊢i e1 := e2 : unit
Γ; Σ ⊢i e : τ refΓ; Σ ⊢i !e : τ(T-Assign)(T-Deref)ℓ 7→ τ ∈ Σ(T-Loc)Γ, Σ ⊢i ℓ : τ refΓ; Σ ⊢1 e1 : τ 1
Γ; Σ ⊢0 ⟨e1 ⟩ : τ 1 codeΓ; Σ ⊢0 e0 : τ 1 codeΓ; Σ ⊢1 ∼ e0 : τ 1
Γ; Σ ⊢i Wrong : τ i(T-Bracket)(T-Escape)(T-Wrong)

PolyMetaML1
Γ; Σ ⊢i e1 : τ1

Γ, (x : ∀α1 · · · αn .τ1 )i ; Σ ⊢i e2 : τ2

(T-Let)Γ; Σ ⊢ let x = e1 in e2 : τ2
ただし，α1 , · · · , αn ∈ FTV(τ1 ) − T V − (τ1 ) − T V no (τ1 ) − FTV(Γ) − FTV(Σ)Γ; Σ ⊢0 e0 : τ 1(T-Csp)Γ; Σ ⊢1 %e0 : τ 1iΓ; Σ ⊢i e : τ [zero/α1 , · · · , zero/αn ]Γ; Σ ⊢i e : τ(α ∈ T V + (τ ))PolyMetaML2
Γ; Σ ⊢0 e0 : τ 1 FTV(τ 1 ) = ∅Γ; Σ ⊢1 %e0 : τ 1
図4(T-CspMono)

PolyMetaML の型付け規則