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

参照を備えた多段階計算のための多相的型システム
小林 恵

五十嵐 淳

本稿では，参照・let 多相を備えた多段階計算体系に対する複数の型システムを提案し比較を行う．参照と let 多相を型安全に組み合わせる手法としては値多相が広く使われているが，これを素朴に多段階計算に適用すると体系の型
安全性が失われるという問題が指摘されている．これは，通常は値と考えられる式が多段階計算では計算が発生する式となる場合があることに起因している．我々は，Tofte による命令的型変数のアイデアを元にして，ふたつの型安全な型システムを構築する．ひとつめの型システムでは，命令的型変数が具体化されるステージを考慮することでより多くのプログラムに型がつくようにしている．ふたつめの型システムは，ひとつめの型システムより制限が厳しい
が，素朴な値多相による型システムに近く，その型安全性からは，CSP と呼ばれる多段階計算の機能を使わない限り，素朴な値多相で型安全性を保証できることがいえる．

ラリ関数 not を bracket 内で参照することができる．

1 はじめにこの，早く計算されるステージの変数を後で計算さ多段階プログラミングとは，実行時にコードの生成れるステージで使うことができる機能は cross-stage

や操作，実行ができるプログラミングパラダイムのこ

persistence(CSP) と呼ばれている．MetaOCaml のとである．こういった多段階プログラミング言語の型

型システムの理論は，計算効果を持たない純粋なプロシステムでは，単に生成するプログラムが安全に実行

グラムについてはよく研究されており，MetaOCaml

できることだけでなく，生成されたコードの安全性もをモデル化した体系に対してその型安全性が示され保証できることが望ましい．

ている [9] [1]．

このような型安全な多段階プログラミングをサ

しかし，この MetaOCaml の型システムは，参照

ポートしている言語のひとつに，OCaml の拡張でなど計算効果のある言語機能と素朴に組み合わせるある MetaOCaml [8] [5] がある．MetaOCaml ではと問題があることが知られている．ひとつは Scope

bracket, escape, run の 3 つの操作による実行時コー

Extrusion という問題で，コード中に含まれる変数がド生成を行える．bracket (.<e>.) はコードを作る操スコープから出てしまうという問題である．例えば，作であり，bracket によって作られたコード内は run(!. e) で実行したときに計算され，その値を得ることができる．escape (.˜e) は，bracket 内で使われ，コー
ド中に e を計算した結果のコードを埋め込むことが# let r = ref .<1>. in
let= .< fun x → .˜( r := .<x + 2>.; .<3>.)>. in!. (!r);;できる．また，let x = 1 + 2 in .<not (x > 2)>.のように，bracket の外側で宣言された変数 x やライブ
Polymorphic Type Systems for Multi-Stage Programming with References
Megumi Kobayashi, Atsushi Igarashi, 京 都 大 学 情 報
学 研 究 科, Graduate School of Informatics, Kyoto
University.

のようなプログラムでは，int 型のコードを格納する参照 r に x+2 という関数パラメータを含むコードを代入
し，それを実行しようとしてしまうが，MetaOCamlの型システムはこれを受理してしまう．(MetaOCamlの処理系 BER MetaOCaml では実行時例外が発生

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

2する．) もうひとつは Kiselyov と Shan が指摘した性質について述べる．最後に 5 節で関連研究につい

値多相の問題である [6]．以下の MetaOCaml のプロて述べ，6 節でまとめる．

グラムには型がつくが，これは実行時型エラーを起こしてしまう．

# let c = .<let f () = .˜(let x = ref [] in .<x>.)in f():=[1]; ”123” :: !(f()) >. ;;val c : string list code = .<let f 1 () = (∗ CSP x ∗) in (f 1 ()) := [1]; ”123”:: (! (f 1 ()))>.

2 MiniML▷% と型システムの概要
本節では，MiniML▷% の概要を説明し，我々の型システムのアイデアを議論する．

2. 1 MiniML▷% の概要
MiniML▷% は，λ 計算を let 式，参照で拡張し，さらに，λ▷% [3] に基く (MetaOCaml 風) 多段階プログ# !. c;;ラミングのための機構を加えたような言語である．

Segmentation fault

項 M に対して，MetaOCaml でいう bracket やこのプログラムでは，f が束縛される式は関数抽象で

escape のような働きをする構築子が ▶α , ◀α である．

あるため，OCaml の型システムは f は値に束縛されこれらに 添字付けられている α は遷移変数と呼ばれると判断し，(Relaxed) Value Restriction [12] [2] にている．遷移変数には，遷移変数の列である遷移を基づいて，f には多相型 unit → ’a list ref を与える．

代入することができ，その遷移変数の列によって ▶ ，

一方で，実行時には，空リストへの参照の生成，CSP◀ の個数が変化する．この遷移変数に空の列を代入

による参照のコードへの埋め込みが，c が束縛される

した場合に， ▶ などが消え，コード本体の項の評価

コードの実行より前に起こる．結局，!. c が実行されを進めることができるようになる．また，▶ や ◀ のると，fは先に生成された参照を返す定数関数に束縛

入れ子の深さをこの遷移で表すことができる．▶α でされ，その参照への整数リストの代入と文字列リスト

α ぶん入れ子が増え，◀α で α ぶん入れ子が減るととしての読み出しが発生し，最終的に返ってくる値は考えると，これが項が評価される段階 (ステージ) を不正な値 [”123”; 1] になってしまう．

表している．この遷移の列は部分列の関係で比較する

本稿では，先ほど挙げた問題のうち後者の値多相ことができ，大きい列が何らかの代入によって空の列に関する問題を扱う．具体的には，多段階計算の機能になるとき，その部分列もその代入によって必ず空のと参照を含む言語 MiniML▷% と，それに対する型シ列になる．

ステムをふたつ定義し，その性質について議論する．

コードを表す型にもこの遷移変数のラベル付けがさひとつめの型システムは，Tofte の命令的型変数のアれており，▷α T は遷移変数 α でラベル付されたコー

イデア [11] を改良したもので，命令的型変数が具体

ドの型を表している．

化されるステージを考慮することでより多くのプロ

上に述べたとおり，空列を遷移変数に代入すること

グラムに型がつくようにしている．ふたつめの型シスでコード中の項が評価可能になる．それではコードの

テムは，ひとつめの型システムより制限が厳しいが，実行をどう行うかというと，遷移変数の束縛と，遷移

素朴な値多相による型システムに近く，その型安全性への適用を使って行う．また，遷移変数の束縛を行っからは，CSP と呼ばれる多段階計算の機能を使わなた Λα.M を遷移に適用すると，項 M 中の束縛されい限り，素朴な値多相で型安全性を保証できることをている遷移変数 α に遷移変数に遷移が代入される．

目指している．

とくに空列に適用した場合は ▶ がすべて消え，その本 稿 の 構 成 は 以 下 の と お り で あ る ．2 節 でMiniML▷% とふたつの型システムのアイデアについて説明する．3 節で MiniML▷%

中の項の評価を進めることができるようになる．
項 M に型 T がつくとき，λ▷% では，遷移変数をの文法・意味論の束縛した項 Λα.M には ∀α.T という型が付く．こう定義を 4 節でそれに対する型システムの定義とそのいった型の出現を let 多相による型変数の一般化とま日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集
とめたいため，MiniML▷% では遷移変数を束縛できるのは let で局所定義される項のみに制限する．

3の属するステージよりも先に計算が起こるステージに参照を確保する項があり，後者では let 式の属する% は，CSP のための，α ぶん後のステージに項をステージと同じステージに参照を確保する項がある

持ち上げる操作である．これは espcape のように何ことがわかる．束縛されている項が関数の場合は，参かと打ち消しあうわけではなく，型付けのためのも照を確保する項が let 式のあるステージ以後にある場のだと思ってもよい．(この体系や λ▷%では) コードの実行の際に空列が代入されて消えることになって合はその参照は確保されないため，参照の型に現れる
型変数を一般化することができる．
このステージの比較を行うため，let 式の型付けでいる．

一般化できる型変数をその let 式のあるステージでラ

2. 2 型システムのアイデア▷%

ベル付けされたものと参照の型に現れないもののみにのための型システムをふ制限する．型変数のラベルの直観的な意味は，「その型たつ提案するが，ひとつめの型システムは，Tofte の変数はラベルとなっているステージまでには具体化さ手法 [11] を改良したものであり，ふたつめの型システれている」というものである．参照の型付けでは，参ムはそれをさらに修正したものとなっている．

照が確保されるときには参照の中身の型が決まってい

本稿ではこの MiniML

Tofte の手法は，型変数を参照型に現れることのなる必要がある．なので，参照の型付けに現れてもよい

い作用的型変数と参照型に現れる可能性のある命令

型変数は，その参照を確保する項が属するステージよ的型変数に分け，let によって変数が束縛される項がりも先に計算されるステージのもののみに制限する．

値でない場合は，一般化できる型変数を作用的型変数のみに制限することで健全な型システムを得ている．

Tofte の手法だけでも型安全性を保証できるが，これまた，let 式で束縛されるものが関数でない場合の例を見ると，

let c = let f = Λα.▶α (λx.%α (ref (λy.y))) in

だけでは多くの安全に実行できるプログラムがはじ((f ε) unit) := (λx.(x + 1));

かれてしまうため，ひとつめの型システムでは，命令!((f ε) unit) true

的型変数をステージごとに細分化することで，単純にのように let 式と参照を確保する項が同じステージにTofte の方法を適用するよりも多くのプログラムに型ある場合は参照が確保されてしまう．よって，let 式をつけられるようにする．

自体のあるステージでラベル付されたものは一般化どういった場合に命令的型変数が一般化できるかを考える．前節のような問題が起きるプログラムを

MiniML▷%で書くと，以下のようになる．

let c = Λα.▶α (let f = λx.%α (ref (λy.y)) in

することができない．
ふたつめの型システムは，項の先頭の構築子だけを見て値かどうかを判断する素朴な値制限だけでも，CSP を使わない限り健全になのではないか，という(f unit) := (λx.(x + 1));

観察に基づき，ひとつめの型システムを変更したもの!(f unit) true)

である．具体的には，CSP の対象となる項の型にあこういった一見値に見えるが実際には先に参照が確らわれる型変数のうち参照型に現れるものにのみス

保されてしまう場合には，その参照に現れる型変数

テージの制限が加わることになる．ふたつめの型シスを一般化してはいけない．逆に，以下のようなものでテムは受理できる項の観点からはひとつめの型シス

は f の型を一般化してもよい．なぜなら，この例でテムより制限が強いが，CSP を使わない限り命令的は参照が確保されることはないからである．

型変数を使わないため，素朴な値制限を採用した型シ

let c = Λα.▶α (let f = λx.ref (λx.x))

ステムと実質同じであり単純なものとなっている．

in f unit := (λx.(x + 1)); !(f unit) true)
この 2 つの例の間の違いを考えると，前者では let 式

3 MiniML▷% の構文と操作的意味論
この節では，MiniML▷% の文法と操作的意味論を

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

4◀ の出現には条件があるため，このような定義になっ

定義する．
▷%

定義 1 (MiniMLの文法). MiniML

▷%

の変数，遷

移変数，遷移，ロケーション，項を以下のように定義ている．
次に，操作的意味論で用いる代入を定義する．
定義 3 (代入). 遷移 A 中の遷移変数 β への遷移 B

する．
変数 x, y, z ∈ Υ
遷移変数 α, β ∈ Θの代入 A[β := B] を以下のように定義する．

ε[α := B] = ε∗

遷移 A, B ∈ Θ
ロケーション l ∈ L

項 M, N ::= x A1 · · · An | λx.M | M N | unit

(Aα)[α := B] = (A[α := B])B
(Aα)[β := B] = (A[β := B])β(if α ̸= β)−→−→( A An+1 )[β := B] = ( A [β := B])(An+1 [β := B])| ref M | !M | M := N | l

次に，項 M 中の遷移変数 α への遷移 A の代入を以| ▶α M | ◀α M | %α M

下のように書く．
−→−→(x A )[α := A] = x ( A [α := A])| let x = Λα1 · · · αn .M in N
遷移は，遷移変数の長さ 0 以上の有限列である．遷(▶α M )[α := A] = ▶A (M [α := A])

移 A と B に対して． AA′ = B となるような遷移

ただし， A = α1 · · · αn (n ≥ 0) とすると，A′ が存在するとき，A ≤ B とかくことにする．ロ▶A M = ▶α1 · · · ▶αn M

ケーションは，確保された参照のメモリ上での位置◀A M = ◀αn · · · ◀α1 Mを表すもので，ロケーションの可算無限集合 L の元

%A M = % αn · · · %α1 M

である．λ

▷%

では遷移変数に関する抽象を行うための項 Λα.M があったが，型システムの簡略化のため，
ここでは let で局所定義される項のみに制限する．ただし，複数の遷移変数での抽象を許している．対応して，遷移 (の列) に適用できるのは変数のみとなっている．以下，(n が重要でないところでは)Λα1 · · · αn .
−
→
→
を Λ−
α . と，x A · · · A を x A と書く．

であり，特に n = 0 のとき ▶ε M = ◀ε M = %ε M =→M となる．最後に，項 M 中の変数 x への Λ−
α .N→の代入 M [x := Λ−α .N ] を定義する．
−
→
−
→
−
→
→
(x A )[x := Λ α .N ] = N [−α := A ]→→→(M N )[x := Λ−α .N ] = (M [x := Λ−α .N ]) (N [x := Λ−α .N ])..
.

集合 V A を以下のように定義する．このうち，V ε の

−
→
→
([−
α := A ] は同時代入に拡張した表記である．)−→→
代 入 で 特 に 重 要 な の は ，(x A )[x := Λ−α .N ] =−→−→▷%N [ α := A ] の場合である．MiniMLの元となって元を値と呼び，メタ変数は (添字のない) v を使う．

いる λ▷% [3] では，遷移変数による抽象 Λα.M や遷移

値 v ∈ V ::= λx.M | unit | ▶α v | l−→
v A ∈ V A ::= x B | λx.v A | v A v A | unit

への適用 M A が項であり，(Λα.M ) A → M [α := A]1n

定義 2 (値, 簡約基). 遷移で添字付けされた項の部分

ε

ε

α

| ref v A | !v A | v A := v A′| ◀α v A (A′ α = A and A′ ̸= ε)′| ▶α v Aα | %α v A (A′ α = A)→
| let x = Λ−
α .v A in v A
また，簡約基を以下のように定義する．
簡約基 Rε ::= (λx.M ) v ε | ref v ε | !l | l := v ε→| let x = Λ−
α .v ε in M

Rα ::= ◀α ▶α M
おおまかにいうと，V α1 ...αn の元は，コード値▶α1 · · · ▶αn の中に現れてよい項を表している．ここには基本的には全ての種類の項が現れてよいのだが，という簡約が与えられていた．一方，MiniML▷% では遷移変数に関する抽象が出現する位置を制限しており，(Λα.N )A という項は構文的に許されていない．
そのため，αi を Ai で具体化するプロセスを簡約ではなく代入で一気に行ってしまうようにしたものが上で定義した代入である．
定義 4 (自由な変数，遷移変数). 項 M に自由に出現する変数，遷移変数の集合をそれぞれ F V (M )，F T rV (M ) と書き，それぞれ以下のように定義する．

日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集(ただし，ここでは重要な場合のみ示している．)−→
F V (x A ) = {x}F V (λx.M ) = F V (M ) \ {x}−→F V (let x = Λ α .M in N ) =F V (M ) ∪ (F V (N ) \ {x})−→−→F T rV (x A ) = F T rV ( A )F T rV (▶α M ) = {α} ∪ F T rV (M )→F T rV (let x = Λ−α .M in N ) =→(F T rV (M ) \ {−α }) ∪ F T rV (N )項のステージや値呼びであることを考慮した簡約の定義のため，評価文脈を定義する．
定義 5 (評価文脈). 簡約規則を定めるための評価文

5

定義 7 (簡約規則). MiniML▷% の簡約関係は，

M | µ → M ′ | µ′という形の項とストアの組の二項関係であり，図 2で与える簡約規則からなる最小の関係である．

Scope extrusion はこの型システムでは関知しない
ため，E-RefE ，E-AssignE の 2 つの規則で，参照の中に変数が自由に出現するような項が代入された時点で実行時エラーを発生させる．

4 型システム
本節では，前節で定義した言語に対し，型システム
を与える．

脈を，図 1 で定義する．評価文脈はふたつの遷移 A,

B で添字付けされており．直観的には，遷移 A がそ4. 1 定義の評価文脈自体のあるステージ，遷移 B が □ のス

まず，型変数と，作用的・命令的型変数を区別する

AA
テージを表している．また，EB[M ] で EB中の □ためのカインドを定義する．

を M で置き換えた項を表す，

定義 8 (型変数，カインド).
型変数 X, Y, Z ∈ ΦεEB∈ ECtxεB ::=εε□ (if B = ε) | EB
M | v ε EBεεε
| ref EB
| !EB
| EB
:= M
ε
α
| v ε := EB| ▶α EB→| let x = Λ−α .E ε in M
B

A
A
A
EB
∈ ECtxA
B ::= □ (if A = B) | λx.EB | EB MAAA
| v A EB
| ref EB
| !EB
A
A
| EB
:= M | v A := EB′Aα
A| ▶α EB| ◀α EB(A′ α = A)′A
| %α EB(A′ α = A)→
| let x = Λ−α .E A in M
BA→
| let x = Λ−
α .v A in EB

カインド K ∈ {app} ∪ Θ∗
型変数が作用的である場合は app，命令的である場
合は そのステージを表す遷移がそのカインドとなる．
定義 9 (型，型スキーム). 遷移変数の列 α1 · · · αn→に 対 し て ∀α . · · · .∀α を ∀−α と ，型 変 数 と カ イ
1n

ンドからなる列 X1 :: K1 · · · Xm :: Km に対して−−−−→
∀X1 :: K1 . · · · .∀Xm :: Km を ∀X :: K とかく．
以下のように型 T と型スキーム S を定義する．

T ::= b | X | T → T| Unit | Ref T | ▷α T−−−−→→
S ::= ∀−α .∀X :: K.T
ただし，b は基底型である．

図1

評価文脈

型環境は，変数とその型，もしくは，型変数とそのカインドの対応関係の宣言の並びである．

定義 6 (ストア). 各参照と，それに保持されている

定義 10 (型環境). 型環境 Γ を以下のように定義する．

値の対応であるストアを，ロケーションの集合 L か型環境 Γ ::= ∅ | Γ, x : S@A | Γ, X :: K

ら値の集合 V ε への有限部分写像とする．

変数は他の多段階計算体系と同様に型だけでなな

また，簡約規則などでは以下のような略記を用いる．

くステージ (遷移) とも関連付けられている．

• (µ, l 7→ v) で µ に l 7→ v を追加したストアをあ定義 11 (型・型スキーム・型環境の自由な遷移変数・型

らわす (ただし l ∈/ dom(µ) とする)．
′• [l 7→ v]µ で µ 中の l 7→ v を l 7→ v に置き換えたストアを表す (ただし l ∈ dom(µ) とする)．

変数). 型，型スキーム，型環境に自由に出現する型変数の集合をそれぞれ F T V (T )，F T V (S)， F T V (Γ)

6

日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集l∈/ dom(µ) and F T rV (v) = ∅EεA [(λx.M ) v] | µ → EεA [M [x := v]] | µ (E-App)F V (v) ̸= ∅EεA [ref v] | µ → SEError(E-Ref)F V (v) ̸= ∅EεA [l := v] | µ → SEError

EεA [ref v] | µ → EεA [l] | (µ, l 7→ v)
F V (v) = ∅EεA [l := v] | µ→ EεA [unit] | [l 7→ v]µl ∈ dom(µ)(E-Assign)→ EεA [µ(l)] | µEεA [!l] | µ(E-Ref)(E-Assign)(E-Deref)→→EεA [let x = Λ−
α .v in N ] | µ → N [x := EεA [Λ−α .v]] | µ (E-Let)EαA [▶α ◀α M ] | µ → EαA [M ] | µ (E-▶◀)
図2

簡約規則

の代入 T [X := T ′ ] を以下のように定義する．

と書き，以下のように定義する．

b[X := T ′ ] = b

F T V (X) = {X}
−
→
−
→
−
→
F T V (∀ α .∀ X .T ) = F T V (T ) \ X∪
F T V (Γ) =F T V (S)X[X := T ′ ] = T
Y [X := T ′ ] = Y(X ̸= Y )′(T1 → T2 )[X := T ] = (T1 [X := T ′ ]) → (T2 [X := T ′ ])x:S@A∈Γ

また， 型，型スキーム，型環境に自由に出現する
遷移変数の集合をそれぞれ F T rV (T )，F T rV (S)，F T rV (Γ) と書き，以下のように定義する．

Unit[X := T ′ ] = Unit
(Ref T )[X := T ′ ] = Ref (T [X := T ′ ])(▷α T )[X := T ′ ] = ▷α (T [X := T ′ ])型に対する遷移の代入 T [α := A] を以下のように定F T rV (▷α T ) = {α}
義する．
−
→
−
→
→
→
F T rV (∀−α .∀ X .T ) = (F T rV (T ) ∪ F T rV ( X )) \ {−α}∪b[α := A] = b
F T rV (Γ) =(F T rV (S) ∪ F T rV (A))
X[α := A] = X
x:S@A∈Γ
また，型 T 中で参照の型の中に現れる型変数の集合(T → T )[α := A] = (T [α := A]) → (T [α := A])
1

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

2

1

Unit[α := A] = Unit

F IT V (b) = ∅(Ref T )[α := A] = Ref (T [α := A])

F IT V (X) = ∅(▷α T )[α := A] = ▷A (T [α := A])

F IT V (T1 → T2 ) = F IT V (T1 ) ∪ F IT V (T2 )(▷β T )[α := A] = ▷β (T [α := A])

F IT V (Unit) = ∅F IT V (ref T ) = F T V (T )(β ̸= α)ただし，▷A は ▶A と同様に定義する．

F IT V (▷α T ) = F IT V (T )型に現れる型変数とステージの制約を表現するた例 12. F T V (X → ref Y ) = {X, Y } が成立する．また F IT V (X → ref Y ) = {Y } が成立する．
定義 13 (型への代入). 型 T 中の型変数 X への T

2め，以下のような関係 Γ ⊢ T ≤ K を定義する．
def′

定義 14. Γ ⊢ T ≤ K ⇐⇒ K = app または，あるA について K = A かつ ∀X ∈ F T V (T ).X :: B ∈Γ かつ B ≤ A．
定義 15 (ストア型付け). ロケーションの型付けを行うため，ストアと同様にロケーションの集合 L から型の集合 Types への有限部分写像であるストア型付

日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集
けを導入する．また，ストアと同様に以下のような略記を用いる．

7

まず，いくつかの準備的定義を行う．ストアとストア型付けが正しく対応していることを示す以下の関• l∈/ dom(Σ) のとき (Σ, l 7→ T ) で Σ に l 7→ T

定義 17 (ストアの正しい型付け). dom(µ) = dom(Σ)

を追加したストアをあらわす．

• l ∈ dom(Σ) のとき [l 7→ T ]Σ で Σ 中の l 7→ T係を導入する．

′を l 7→ T に置き換えたストアを表す．

かつ ∀l ∈ dom(µ).∅; Σ ⊢1 µ(l) : Σ(l) @ε のときスト
ア型付け Σ のもとでストア µ に型が付くといい，Σ ⊢1 µ定義 16 (型付け関係). 図 3 の共通の型付け規則と型付け規則 1 のみから Γ; Σ ⊢ M : T @A が導出できる
とき，

と書く．
また，健全性の条件となる型環境の条件 ε-free を

Γ; Σ ⊢1 M : T @A

以下のように定義する．

と書く．同様に，共通の型付け規則と型付け規則 2 か

定義 18 (ε-free). ∀(x : S@A) ∈ Γ.A ̸= ε であるとら Γ; Σ ⊢ M : T @A が導出できるとき，き，Γ は ε-free であるという，

Γ; Σ ⊢2 M : T @Aと書く．
型システム 1 で特に重要な規則は， T-Ref, T-

まず，型システム 1 で型がつく項は，評価文脈とRedex に一意に分解できる，すなわち型が付く項では評価結果が一意に定まる．

LetLam, T-Let である．let 式の型付け規則が 2 種定理 19 (型システム 1 の Unique Decomposition).

類あり，定義されるのがラムダ抽象である場合の型付

Γ; Σ ⊢1 M : T @A かつ Γ が ε-free ならば，M ∈ V A

け (T-LetLam) では，参照の型では使われない作用Aであるか，または M = EB
[RB ] となるようなペア的型変数と，let 式のあるステージを表す遷移をカイA, RB ) が一意に存在する．ただし， B は ε か，(EBンドとする命令的型変数のみ一般化できる．それ以単一の遷移変数からなる列 β である．

外の項の場合には，作用的型変数と，let 式のあるス

証明. Γ; Σ ⊢1 M : T @A に関する帰納法で示すことテージを表す遷移にさらに束縛されている遷移変数をができる．

含む列を加えた遷移をカインドとする型変数のみが一般化できる．参照の型付けでは，参照のあるステー
ジよりも前のステージがその型に現れる型変数とし次に，型システム 1 の健全性として，Progress とSubject reduction を証明する．

て使われていなければならない．これらの制限によっ

Progress は，型が付く項は正しく評価を進めるこて，let 式全体が簡約されるより先に確保される参照とができるか，あるいは Scope extrusion が起きるかの型変数は一般化されないようになる．

であることを示している．

型システム 2 は，ほとんど通常の値制限の型シス定理 20 (型システム 1 の Progress). Γ; Σ ⊢1 M : T @A，テムになっており，ラムダ式やコード以外の項は letΣ ⊢1 µ かつ Γ が ε-free ならば，M | µ → M ′ | µ′に現れても単相的にしか使えない (T-Let)．一方，参と な る よ う な 項 M ′ と ス ト ア µ′ が 存 在 す る か ，照の型付けにあった条件が，CSP 操作の型付け規則

M | µ → SEError となる．

に移っている．これにより，CSP によってステージをまたいで使われるロケーションの型に現れる型変数が後のステージで束縛されることを防いでいる．

Progress に関しては， Unique Decomposition を使って簡単に示すことができる．
A
証明. Unique Decomposition より，M = EB
[RB ]となる評価文脈と Redex が一意に存在する．よって，

4. 2 型システム 1 の性質

いずれかの簡約規則を用いて評価を進めることがで上で定義した型システム 1 が健全であることをきる．特に E-Deref の場合， RB =!l となるが，subject reduction, progress の性質を証明することで示す．

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

8
共通の型付け規則−−−−→→
x : ∀−α .∀X :: K.T @A ∈ ΓΓ ⊢ Ti ≤ Ki
(T-Var)
−
→
−
→ −
→
−
→
→
Γ; Σ ⊢ x A : T [−α := A ][ X := T ] @A

Γ, x : T1 @A; Σ ⊢ M : T2 @A(T-Abs)Γ; Σ ⊢ λx.M : T1 → T2 @A

Γ; Σ ⊢ M : T1 → T2 @A
Γ; Σ ⊢ N : T1 @A(T-App)Γ; Σ ⊢ M N : T2 @A
Γ; Σ ⊢ M : Ref T @A
Γ; Σ ⊢ N : T @A
(T-Assign)Γ; Σ ⊢ M := N : Unit @Al ∈ dom(Σ)(T-Loc)Γ; Σ ⊢ l : T @εΓ; Σ ⊢ M : Ref T @A
(T-Deref)Γ; Σ ⊢!M : T @A

Γ; Σ ⊢ M : T @Aα(T-▶)Γ; Σ ⊢ ▶α M : ▷α T @A

Γ; Σ ⊢ M : ▷α T @A
(T-◀)Γ; Σ ⊢ ◀α M : T @Aα

−−−−→
−−−−→
→
Γ, X :: K; Σ ⊢ λx.M : T ′ @A
Ki ∈ {app, A}
Γ, x : ∀−α .∀X :: K.T ′ @A; Σ ⊢ N : T @A
(T-LetLam)→
Γ; Σ ⊢ let x = Λ−α .λx.M in N : T @A

型付け規則 1
Γ; Σ ⊢ M : T @AΓ⊢T ≤A(T-Ref)Γ; Σ ⊢ ref M : Ref T @A

Γ; Σ ⊢ M : T @A
(T-%)Γ; Σ ⊢ %α M : T @Aα−−−−→→
Γ, X :: K; Σ ⊢ λx.M : T ′ @A
Ki ∈ {app} ∪ {AA′ α | A′ ∈ Θ∗ , α ∈ −α}−−−−→ ′→−
Γ, x : ∀ α .∀X :: K.T @A; Σ ⊢ N : T @A
(T-Let)→Γ; Σ ⊢ let x = Λ−α .M in N : T @A

型付け規則 2
Γ; Σ ⊢ M : T @A
(T-Ref)Γ; Σ ⊢ ref M : Ref T @A

Γ; Σ ⊢ M : T @A
∀X ∈ F IT V (T ).Γ ⊢ X ≤ A(T-%)Γ; Σ ⊢ %α M : T @Aα−−−−→→
Γ, X :: K; Σ ⊢ ▶α M : T ′ @A
Ki ∈ {app, Aα}
α∈−
α
−−−−→
−
→
Γ, x : ∀ α .∀X :: K.T @A; Σ ⊢ N : T @A
(T-Let▶)→Γ; Σ ⊢ let x = Λ−α .▶α M in N : T @A→
Γ; Σ ⊢ M : T ′ @AΓ, x : ∀−α .T ′ @A; Σ ⊢ N : T @A
(T-Let)−→Γ; Σ ⊢ let x = Λ α .M in N : T @A
図3

型付け規則

Σ ⊢1 µ より l ∈ dom(µ) である．
Subject reduction では，正しく型付けされた項とストアから正しく評価が進んだとき，評価した結果の項とストアもまた正しく型がつくことを示している．
定 理 21 (型 シ ス テ ム 1 の Subject Reduction).

Γ; Σ ⊢1 M : T @A，Σ ⊢1 µ，M | µ → M ′ | µ′ がな
りたち，T ，Γ には ステージ ε の命令的な型変数が自由に出現しないならば，Γ; Σ′ ⊢1 M ′ : T @A かつΣ′ ⊢1 µ′ が成り立つようなストアの型付け Σ′ ⊇ Σが存在する．

Subject reduction の証明のために，いくつかの補題を証明する．
まず，代入に関して型付けが保存されることを示
す代入補題を示す．そのために，型スキーム，カイン

ド，型環境への型・遷移の代入を定義する．
定 義 22. 型 ス キ ー ム に 対 す る 型 の 代 入
−−−−→
→
(∀−
α .∀Y :: K.T )[X := T ′ ] を以下のように定義する．

−−−−→
−−−−→
→
→
(∀−
α .∀Y :: K.T )[X := T ′ ] = ∀−α .∀Y :: K.(T [X := T ′ ])−→−→ただし X ∈
/ Y か つ F T V (T ′ ) ∩ Y = ∅ か つ→
F T rV (T ′ ) ∩ −α = ∅．次に，型環境に対する型の
代入 Γ[X := T ′ ] を以下のように定義する．

(Γ, x : S@A)[X := T ′ ]= (Γ[X := T ′ ]), x : (S[X := T ′ ])@A(Γ, Y :: K)[X := T ′ ]= (Γ[X := T ′ ]), Y :: K
(X ̸= Y )−−−−→−→型スキームに対する遷移の代入 (∀ α .∀Y :: K.T )[β := B]−−−−→→を以下のように定義する．(∀−α .∀Y :: K.T )[β := B] =
−−−−→
→
→
∀−
α .∀Y :: K.(T [β := B]) (た だ し β ∈
/ −
α かつ
→
F T V (B) ∩ −α = ∅)．最 後 に ，型 環 境 に 対 す る 遷

日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集
補 題

移の代入 Γ[β := B] を以下のように定義する．

25

9(Redex の 型 付 け 中 の 型 変 数).

(Γ, x : S@A)[β := B]AΓ; Σ ⊢1 M : T @A かつ M = EB[ref v] となるよ= (Γ[β := B]), x : (S[β := B])@(A[β := B])

Aと Redex R = ref v が存在し，うな評価文脈 EB(Γ, X :: K)[β := B]

RB = ref v かつ ∀X ∈ F T V (T ) ∪ F T V (Γ).X ::= (Γ[β := B]), X :: (K[β := B])ε ∈/ Γ な ら ば ，導 出 中 の Redex RB の 型 付 け

ただし，カインドに対する遷移の代入 K[β := B] はΓ; Σ ⊢1 R : T ′ @B で F T V (T ′ ) = ∅ が成り立つよ

A[β := B] の定義を app[β := B] = app で拡張すれうな Γ; Σ ⊢1 M : T @A の導出が存在する．

ばよい．
補題 23 (型システム 1 の代入補題).
−−−−→→
1. Γ, x : ∀−α .∀X :: K.T @A; Σ ⊢1 M : T @A かつ→
Γ; Σ ⊢ N : T ′ @B か つ ∀α ∈ −α .α ∈/
1

A
証明. 評価文脈 EB
に関する帰納法で示すことができる．
以上の補題より， Subject Reduction を示すことができる．

F T V (A) ∪ F T V (Γ) ならば→
Γ; Σ ⊢ M [x := Λ−α .N ] : T @A．

型システム 1 の Subject Reduction の証明. 補 題

1

2. Γ; Σ ⊢1 M : T @A ならば

25 よ り，Redex の 型 に 型 変 数 が 現 れ な い よ う なΓ[X := T ′ ]; Σ[X := T ′ ] ⊢1 M : T [X := T ′ ] @A
3. Γ; Σ ⊢1 M : T @A ならばΓ; Σ ⊢1 M : T @A の導出が存在する．補題 24 より，型に型変数が自由に現れないような Redex の簡Γ[α := A]; Σ[α := A] ⊢M [α := A]

約については型が保存される．よって，項全体の簡約: T [α := A] @A[α := A]として見ても Γ; Σ′ ⊢1 M : T @A, Σ′ ⊢1 µ′ が成り立
つようなストア型付け Σ′ ⊇ Σ が存在する．

証明.

−−−−→
→
1. Γ, x : ∀−α .∀X :: K; Σ ⊢1 M : T @A に 関 す る
4. 3 型システム 2 の性質

帰納法で示せる．

2. Γ; Σ ⊢1 M : T @A に関する帰納法で示せる．

型 シ ス テ ム 2 も ，型 シ ス テ ム 1 と 同 じ よ う に

3. Γ; Σ ⊢1 M : T @A に関する帰納法で示せる．

Σ ⊢2 µ を定義することで，Unique Decompositionと Progress が成り立つ．
定理 26 (型システム 2 の Unique Decomposition).

この代入補題を用いて，さらに 2 つの補題を証明する．

Γ; Σ ⊢2 M : T @A かつ Γ が ε-free ならば，M ∈ V A
Aであるか，または M = EB
[RB ] となるようなペア

補題 24 (Redex の型の保存).
′

1. Redex ref v に つ い て ，ref v | µ → N | µ ，Γ; Σ ⊢1 ref v : T @B ，Σ ⊢1 µ であり，∀X ∈A(EB, RB ) が一意に存在する．ただし， B は ε か，単一の遷移変数からなる列 β である．

F T V (T ).X :: ε ∈/ Γ ならば，Γ; Σ′ ⊢1 N : T @B

証明. 型システム 1 の Unique Decomposition と同，Σ′ ⊢1 µ′ が成り立つようなストア型付け Σ′ ⊇ Σ様に，Γ; Σ ⊢2 M : T @A に関する帰納法で証明するが存在する．

ことができる．

2. Redex RB (̸=ref v) ( B は ε ま た は

単一の遷移変数からなる列 β ) につい′て ，R | µ → N | µ ，Γ; Σ ⊢1 R
B

B

: T @B ，′Σ ⊢1 µ ならば，Γ; Σ ⊢1 N : T @B ，Σ ⊢1 µ が定理 27 (型システム 2 の Progress). Γ; Σ ⊢2 M : T @A，

Σ ⊢2 µ かつ Γ が ε-free ならば，M | µ → M ′ | µ′と な る よ う な 項 M ′ と ス ト ア µ′ が 存 在 す る か ，

M | µ → SEError となる．

成り立つ．
証明. 型システム 1 の Progress と同様に，Unique
証明. 代入補題より証明できる．

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

10

Decomposition によって簡単に証明できる．
また，Subject Reduction も成り立つと予想される．
予想28tion).

(型 シ ス テ ム 2 の Subject ReducΓ; Σ ⊢2 M : T @A か つ Σ ⊢2 µ か つ

M | µ → M ′ | µ′ がなりたち，T ，Γ には ステー
ジ ε の命令的な型変数が自由に出現しないならば，

Γ; Σ′ ⊢2 M ′ : T @A かつ Σ′ ⊢2 µ′ が成り立つようなストアの型付け Σ′ ⊇ Σ が存在する．

4. 4 比較型システム 1 と型システム 2 を比較したとき，型システム 2 で型がつくプログラムは型システム 1 でもまた型が付くと予想される．
予想 29. Γ; Σ ⊢2 M : T @A ⇒ Γ; Σ ⊢1 M : T @A
型システムとしては型システム 1 は 型システム 2
よりも強い．関数適用などであっても，参照の操作を含まないようなものならば多相型をつけることができる．
しかし，現在広く使われている値制限により近いのは型システム 2 である．とくに CSP を使わない場合には単純にコードや関数を値とみなして型をつけることができ，型変数のステージを気にせずにプログラ
ムを書くことができる．

には命令的型変数が現れるため一般化することができない．一方，我々の型システム 1 では引用中の refの出現と引用の外のそれとをカインドで区別することができるので，上の f を多相的に使うことができる．
このように命令的型変数をさらに詳細化するアイ
デアは，Standard ML of New Jersey (SML/NJ) で採用されていた weak type variable [4] とも共通するものといえる．SML/NJ では，関数抽象の中に現れるために関数適用が発生するまでは参照を生成しない ref の出現と，そうでない出現を区別し，適用が何度起こると参照が確保されるかの情報を表すために命令的型変数を自然数で添字付けしたような型シ
ステムを採用していた．一方，我々の型システムはどの遷移変数に ε が代入されると参照が確保されるかの情報を表すために命令的型変数に遷移を加えていると考えることができる．
今回の多段階プログラミングのモデルとなる計算体
系は λ▷% [3] をベースとしたが，より MetaOCamlに近い型システムである λα [9] や λi [1] をベースとしても，今回と同様なアイデアが適用できると考えているが，これらの体系では，明示的に遷移の受渡しが行われなかったり，コードの評価の意味が λ▷% と微妙に異なるため，その点は考慮する必要があるだろう．

5 関連研究本稿で提案する型システムは既に述べたように

Tofte による命令的型変数を使った参照のための多相型システム [11] に基づいている．Tofte の手法だけでも，MiniML▷% に対する健全な型システムは構築できるが，コードの内と外を区別しないので，ref を含
むコードを純粋な計算で操作する時に多相性を失うという欠点がある．例えば，

その他にも，closure typing [7]，エフェクトシステ
ム [10] などを使い参照と多相性を型安全に両立させるための研究が数多くされてきた．これらを多段階プロ
グラミングのための型システムと組み合わせてみることは今後の研究として興味深い．特にエフェクトシス
テムは scope extrusion 問題への解決策としても研究されているため ，値多相の問題も解決できるのであれ
ば，ふたつの問題を同時に解決できる可能性がある．

let c = Λα.▶α let f = λz.◀α ((λx.x) (▶α (ref (λy.y)))) in . . .
のようなプログラムを考える．これは，単にエスケー
プ部分で恒等関数をコード片に適用しているだけで，結果としてlet c = Λα.▶α let f = λz.ref (λy.y) in . . .
となるので，f は多相的に使えてもよいのだが，Tofteの型システムをそのまま適用すると，ref (λy.y) の型

6 おわりに本稿では，参照と let 式を備えた多段階プログラミ

ング言語 MiniML▷% を定義し，それに対する型シス
テムをふたつ提案した．また，ふたつめの型システムに関しては一部予想ではあるが，これらの型システムの健全性や関係についての定理および予想を示した．
今後の課題としては，実用に近づくためにはこの日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集型システムに対応する型推論アルゴリズムを考えることがあげられる．もうひとつの問題である Scope

extrusion については本稿の型システムでは静的に検出することができないため，この問題を解決することも課題の一つである．

参 考 文 献[ 1 ] Calcagno, C., Moggi, E., and Taha, W.: MLLike Inference for Classifiers, Proceedings of European Symposium on Programming (ESOP’04),
Springer LNCS, Vol. 2986, 2004, pp. 79–93.
[ 2 ] Garrigue, J.: Relaxing the Value Restriction,
Proc. of International Symposium on Functionaland Logic Programming (FLOPS 2004), Spritger
LNCS, Vol. 2998, 2004.
[ 3 ] Hanada, Y. and Igarashi, A.: On Cross-Stage
Persistence in Multi-Stage Programming, Functional and Logic Programming - 12th International
Symposium, FLOPS 2014, Kanazawa, Japan, June
4-6, 2014. Proceedings, 2014, pp. 103–118.
[ 4 ] Hoang, M., Mitchell, J., and Viswanathan, R.:
Standard ML-NJ weak polymorphism and imperative constructs, Proc. of IEEE Symposium on Logicin Computer Science (LICS’93), 1993, pp. 15–25.
[ 5 ] Kiselyov, O.: The Design and Implementation of BER MetaOCaml: System Description,

11

Proc. of International Symposium on Functionaland Logic Programming (FLOPS 2014), Springer
LNCS, Vol. 8475, 2014, pp. 86–102.
[ 6 ] Kiselyov, O. and Shan, C.-c.: Staged letgeneralization may be unsound, http://okmij.org/
ftp/meta-programming/calculi.html#staged-poly,2010.
[ 7 ] Leroy, X. and Weis, P.: Polymorphic Type Inference and Assignment, Proc. of ACM Symposium on
Principles of Programming Languages (POPL’91),
1991, pp. 291–302.
[ 8 ] Taha, W.: A Gentle Introduction to Multi-stage
Programming, Domain-Specific Program Generation, International Seminar, Dagstuhl Castle,
Germany, March 23-28, 2003, Revised Papers,
Lengauer, C., Batory, D. S., Consel, C., and Odersky, M.(eds.), Lecture Notes in Computer Science,Vol. 3016, Springer, 2003, pp. 30–50.
[ 9 ] Taha, W. and Nielsen, M. F.: Environment Classifiers, Proceedings of ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (POPL’03), 2003, pp. 26–37.
[10] Talpin, J.-P. and Jouvelot, P.: The Type andEﬀect Discipline, Information and Comptation,
Vol. 111, No. 2(1994), pp. 245–296.
[11] Tofte, M.: Type Inference for Polymorphic References, Information and computation, Vol. 89,
No. 1(1990), pp. 1–34.
[12] Wright, A. K.: Simple Imperative Polymorphism, Lisp and Symbolic Computation, Vol. 8(1995).