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

依存型を含むマルチステージプログラミングの型理論
河田 旺

五十嵐 淳

実行中にプログラム自体を生成・実行するマルチステージプログラミングにおいて，生成されたプログラムの安全性を保証することは重要な課題である. 本研究では，Hanada,，Igarashi による既存のマルチステージプログラミング
言語を拡張し, 依存型を扱えるようにすることで，生成されたプログラムの安全性をより強固に保証する型システムを提案する. 依存型を導入するには型同士の等価関係を定義することが必要だが，コード化されたプログラムの型の間の等価関係は，値をコードの中に埋め込むための CSP と呼ばれる操作と関連するときに自明ではない．本研究では，型とカインドについて暗黙に CSP を認め，それに対応する等価関係のための規則を追加することで型の間の等価関係を定義した．更に提案する型システムに望ましい性質として型システムの健全性と合流性，強正規化性を挙げ，その証明の見通しについて議論する．

さ n の Int 型の配列から要素を読みだす関数 read1 はじめには read : (Πn : Int.(Vect n → Index n → Int)) と

1. 1 依存型

表現できる．Π は依存関数型のための記号であり，依存型とは値に依存する型である．依存型を使え

Πx : T1 .T2 は T1 型の引数を受け取り T2 を返す関数ば，単純型付きラムダ計算では表現できない，長さ nの型を表す．ただし，T2 は x を含んでもよく，返りの整数を要素とする配列の型 Vect n や，範囲を 0 か

値型が引数 x に依存することを表す．この型を持つ

ら n − 1 までに制限した整数の型 Index n を表現す関数 read による配列へのアクセスは決して配列外参ることができる．

照を起こさないことが保証できる．

依存型の応用例として配列外参照の防止 [14] が挙げられる．配列外参照とは配列の範囲外のメモリ領域へのアクセスを指し，コンピュータセキュリティ上の深刻なセキュリティホールになりうる．

1. 2 マルチステージプログラミング
マルチステージプログラミングとはランタイムにプログラムのコード片を組み合わせ，生成，実行でき依存型をもつ型付ラムダ計算 λLF [1] では，Vect

るプログラミングのパラダイムの一つである．これらは Vect :: (Int → ∗) と宣言され，Index は Index ::の操作によりプログラムを部分的に最適化し，高速化(Int → ∗) のように宣言される．∗ は型を表すカイン

することが可能になる．

ドで，この宣言はそれぞれ，整数 n を受け取り長さ

本研究ではマルチステージプログラミングを実現

n の配列の型 Vect n を返す，整数 n を受け取り範囲する方法として，bracket，escape，run，cross-stage

を 0 から n − 1 までに制限した整数の型 Index n を

persistence(CSP) といった機構 [11] を備える型付き返すという意味である．この 2 つの型を使うと，長プログラミング言語を考える．bracket，escape，run

Type Theory for Multi-stage Programming with Dependent Types
Akira KAWATA, Atushi IGARASHI, 京都大学大学院
情報学研究科, Graduate School of Infomatics, Kyoto
University.

はそれぞれプログラムの断片をコードと呼ばれる値として得る操作，プログラムを実行しその結果得られるコード値を bracket 中に埋め込む操作，コード値をプログラムとして実行する操作である．cross-stage

persistence は bracket 中にその bracket の外で定義

2 λMD の形式化

された変数または項を埋め込む操作である．
これらの操作の型安全性を保証する，特に，run が実行するコードが型安全であることを静的に保証する

この節では λMD について詳細に述べる. 2.1 節から λMD の構文, 簡約規則, 型システムを定義する.

ための型システムとして様々なもの [11] [6] [10] が提案

λMD は λLF と λ▷% 双方の拡張になっている．λLF

されている．Hanada と Igarashi [6] は，ステージ変と λ▷% は CSP を除いて機能的に互いに干渉する部数と呼ばれる，各コードがどこでコード化されたのか分がなく，組み合わせるのは比較的容易であった．たを表す情報と，ステージ変数に関する抽象化を使ってだし，λ▷% の CSP に関する部分は λLF と組み合わbracket，escape，run，cross-stage persistence の全せるにあたって非自明な考察が必要であった．

▷%てを含む言語 λのための型システムを提案し，そ2. 1 構文の型安全性を示している．

λMD の構文を定義する.
1. 3 依存型を含むマルチステージプログラミング
本研究では λ▷%に λLF を組み込み，依存型を含む

マルチステージプログラミングを扱える型システム

t ::= x | λx : T.t | t t |▶α t |◀α t | Λα.t | t ϵ | %α t
T ::= X | Πx : T.T | T t | ▷α T | ∀α.T
K ::= ∗ | Πx : T.K

ではマルチステージプログラ

Γ ::= ∅ | Γ, x : T @A (x ̸∈ FV(Γ))

ミングで生成，実行するコードに依存型を用いて型付| Γ, X :: K@A (X ̸∈ FV(Γ))

MD

λを実現する．λMDけすることができる．
例えば，ベクトルの長さを受け取って，2 つのベク

ここで, t は項, x は変数，T は型, X は型変数，K

トルを受け取って 2 つのベクトルの和を返す関数のはカインド, Γ は環境を表す. また α, β はステージ

コードを返す関数 add-vec を考える．add-vec の型は変数, A, B はステージであり 0 個以上のステージ変

次のようになる．ここで ∀α. ▷α T はコードが実行可数の列である. ϵ は 0 個のステージ変数からなるス

能であることを表している．

テージを表す. λx : T.t は t 中の自由な x を束縛し，

add-vec :(Πx : Int.

Πx : T1 .T2 は T2 中の自由な x を束縛する．同様に∀α. ▷α ((Vect x) → (Vect x) → (Vect x)))add-vec ではコードを生成する際にベクトルの長さ xΛα.t は t 中の自由な α を束縛し，∀α.t は t 中の自由な α を束縛する．

を使うことができるので，add-vec が生成したコード

まず，λMD の項について直感的な説明を与える．既の実行時には配列の境界検査が省略できる．さらに，に述べたように，λMD は (簡略化のためのいくつかの

x の情報を使ってベクトルの各要素を足し合わせる

制限はあるが)λ▷% の拡張であり，λ▷% で依存型を扱

ループを展開すれば，ループによる分岐命令や jmp

えるようにしたものである．λMD の項はほぼ λ▷% と命令が削除できるので大幅な高速化が見込まれる．

同じものであり，単純型付きラムダ計算の構文要素にの形式的加えて，5 つの追加要素がある．▶α t は t をコードMDの判化したものを表す．◀α t は escape で ▶α の中で使わ

断，2.3 節では簡約規則，2.4 節では型システムにつれる．t を評価して得られたステージ α のコードを周MD

本論文の構成を説明する．2 節では λな定義を行う．2.1 節では構文，2.2 節では λMDの例とその型りのコード値に埋め込む．Λα.t はステージ変数に関

MD

の満たす

する抽象，t ϵ は ϵ によるステージ変数の空列によるべき性質について述べる．5 節では関連研究について

インスタンス化を表す．%α t は CSP を表すための述べた後に，6 節で結論と今後の課題を論じる．

記号である．

いてそれぞれ説明する．3 節では λ付け導出について説明する．4 節では λλ▷% では任意のステージでインスタンス化できる
ステージ抽象と ϵ のみでインスタンス化できるステー

ジ抽象の 2 種類のステージ抽象が存在したが，λMDはカインド K が環境 Γ の下でステージ A においてには ϵ のみでインスタンス化できるステージ抽象しか適格 (well-formed) なカインドであることを表す.

Γ ⊢ T :: K@A

存在しない．これは型システムを簡略化するための制は型 T が環境 Γ の下でステージ A において K のカ限である．
例えば，▶α ((λx.x)(λy.y)) はコード化された計

インドがつくことを表す.

算の例であり，(Λα. ▶α ((λx.x)(λy.y))) ϵ として後Γ ⊢ t : T @A

で説明するように実行すると λy.y になる．また，は項 t が環境 Γ の下でステージ A において T の型が▶α ((λx.λy.x) (◀α ▶α ((λx.x)(λy.y))) (λz.z)) はつくことを表す.

t1 −→β t2

コード化された計算を escape する例であり，簡約すると ▶α ((λx.λy.x) (λy.y) (λz.z)) になる．
MD

次に，λ
MD

λ

は項 t1 が一回の β 簡約で t2 になることを表す.

t1 −→◀▶ t2の型について直感的な説明を与える．
▷%の型は λLF 由来のものと λ由来のものの 2 種は項 t1 が一回の ◀▶ 簡約で t2 になることを表す.

t1 −→Λ t2

類にわけられる．X は型変数であり，λLF 由来である．

Πx : T.T ，T t は λLF 由来の型である．Πx : T1 .T2

は項 t1 が一回の Λ 簡約で t2 になることを表す.

は値 x に依存する型を表し，T2 に x が自由に出現しΓ ⊢ K1 ≡ K2 @A

ないときは T1 → T2 と書かれることがある．T t ははカインド K1 と K2 が環境 Γ の下でステージ A に値に依存する型 T に値 t を適用した結果の型を表し，おいて等価であることを表す.

Vect 10 などが該当する．▷α T ，∀α.T は λ▷%Γ ⊢ T1 ≡ T2 @A

由来の型である．▷α T はステージ α における型 T のコード

は型 T1 と T2 が環境 Γ の下でステージ A において等の型を表し，∀α.T は，ステージ変数に関する抽象化価であることを表す.

Γ ⊢ t1 ≡ t2 @A

に対して与えられる型で，項がステージ変数 α について閉じていることを表す．

λ▷%ではステージ変数に関する抽象化に対して与は項 T1 と T2 が環境 Γ の下でステージ A において等価であることを表す.

えられる型には，任意のステージでインスタンス化できるステージ抽象につくものと ϵ のみでインスタン

2. 3 簡約規則

ス化できるステージ抽象につくものの二種類が存在

λMD には 3 種類の簡約規則がある.

したが，λMD には ϵ のみでインスタンス化できるス−→β は β 簡約である. −→β はテージ抽象につく型しか存在しない．これは項と同じ(λx : T.t1 ) t2 −→β t1 [x 7→ t2 ]を満たす項に関する最小の合同な二項関係である．こ

理由である．
最後に，λMD のカインドについて直感的な説明を与こで t1 [x 7→ t2 ] は t1 中の x の自由な出現に t2 を代える．∗ は値につく型につくカインドである．例えば，

入して得られる項である．ただし T の中に含まれる

Int や Vect 10 にはカインド ∗ がつく．Πx : T.K は項については β 簡約を行わないものとする．

型 T の値を受け取ってカインド K を返す型につくカ
インドである．例えば Vect にはカインド Πx : Int.∗がつく．ただし K に x が自由に出現しないときはT → K と書かれることがある．

−→◀▶ はコード化とエスケープに関する簡約規則である. −→◀▶ は◀α (▶α t) −→◀▶ tを満たす項に関する最小の合同な二項関係である．この規則は項 t をコード化した ▶α t を escape すると

t に戻ることを表している. この簡約も依存型のパラ2. 2 判断λMDには 9 種類の判断がある.

Γ ⊢ K kind@A

メータの項については行わないものとする．

−→Λ はステージ変数の書き換え規則である. −→Λ

K-Abs，K-App，K-Conv は λLF 由来の規則であは(Λα.t)ϵ −→Λ t[α 7→ ϵ]

る．K-▷, K-Gen は λMD で新たに加わった規則であを満たす項に関する最小の二項関係である．ここでる．K-▷ は構文規則の中の ▷α T に対応し，K-Gen はt[α 7→ ϵ] は t 中の α をすべて ϵ で置き換えたもので∀α.T に対応している．

ある．▶α ，◀α ，%α の α に ϵ を代入するとこれら

K-Csp は型の CSP に関するカインド付け規則での 3 つの記号は消える．Tsukada, Igarashi [13] やあり，λMD に特有の規則である．
Γ ⊢ T :: K@A
K-Csp
Γ ⊢ T :: K@Aα
K-Csp はステージ A で型 T に K というカインドがHanada, Igarashi [6] で議論されているように，ステージ変数に対する ϵ の代入はコードの実行に対応している．この簡約も −→β や −→◀▶ と同様に依存型のパラメータの項については行わないものとする．

つくのなら，ステージ Aα でも型 T に K を導出できるということを意味している．例えば，ステージ ϵ で

2. 4 型システム
λMD の型システムについて述べる. λMD の型シス
テムは型付け規則，カインド付け規則，カインドの適定義した型変数 Vect はステージ α でも，ステージ βでも利用可能である．
最後にカインドの適格性判断規則について説明する．

格性判断規則を定義する部分と項，型，カインドの等

W-Star, W-Abs は構文規則の中の ∗ と Πx : T.K

価性を定義する部分からなる．

に対応するカインドの適格性判断規則である．W-▷,2. 4. 1 型付け規則，カインド付け規則，
カインドの適格性判断規則
図 1 に λMD の型付け規則，カインド付け規則，カ
インドの適格性判断規則を示す．
まず型付け規則について説明する．T-Var, T-Abs,

T-App は単純型付きラムダ計算と同じである．T-▶,
T-◀, T-Gen, T-Ins, T-Csp は λ▷% 由来の規則である．T-▶, T-◀, T-Gen, T-Ins はそれぞれ, プログラ
ムのコード化，escape，ステージ変数の抽象，ステー
ジの適用のための型付け規則である．T-Csp は CSPのための型付け規則であり，前のステージにおける項を次のステージの項として扱い，その項の型を変えずに次のステージでの型としている．

T-Conv は依存型に関する規則であり，ある項 t に型 T がつきさらに T が T ′ と等価ならば，t に T ′ を付けてもよいという規則である．T-Conv は例えば
図 2 のように使われる．この例は λMD に含まれない
自然数に関する演算を含むため，厳密なものではない．しかし T-Conv の直感的な意味をよく捉えている．この導出木はある項 t に長さ (3 + 4) の配列型がつき，さらに長さ (3 + 4) の配列型と 7 の配列型が等価なので，t に長さ 7 の配列型をつけられるということを表している．
次にカインド付け規則について説明する．K-Var,

W-Csp はそれぞれ K-▷, K-Csp に対応するカインドの適格性判断規則である．

2. 4. 2 等価性規則
型付け規則に加えて λMD には項等価性，型等価性，カインド等価性を定義する規則がある．図 3，図 4，
図 5 に λMD のカインド等価性，型等価性，項等価性
規則を示す．
型等価性の規則は T-Conv が等価な型の付け替えを許すために必要である．図 4 の QT-で始まるもの
が型等価性の規則である．また依存型においては型の中に項が含まれる場合があるため，項等価性の規則も必要である．図 5 の Q-で始まるものは項の等価性規則である．さらに QT-App の中にカインド同士の等価性判定が含まれるので，カインドの等価性規則も必要である．図 3 の QK-で始まるものがカインドの等価性規則である．
型等価性の規則とは型上の関係 ≡ を定義する規則
であり，3 種類に分けられる．1 種類目は ≡ を型に関する合同関係にするための規則であり，QT-Abs，

QT-App，QT-▷，QT-Gen，QT-Csp が該当する．
2 種類目は ≡ を同値関係にするための規則であり，
QT-Refl，QT-Sym，QT-Trans が該当する．
項等価性の規則は項上の関係 ≡ を定義する規則
であり，型等価性の規則と同様に 3 種類に分けられΓ ⊢ K kindWell-formed kindsΓ ⊢ ∗ kind@AΓ ⊢ T :: ∗@A

W-StarΓ ⊢ (Πx : T.K) kind@AΓ ⊢ K kind@AΓ ⊢ K kind@AαΓ ⊢ T :: KΓ ⊢ K kind@Aα

W-CspΓ ⊢ K kind@A

W-Abs

W-▷

KindingΓ ⊢ K kind@A

Γ, X :: K@A, ∆ ⊢ X :: K@AΓ ⊢ T2 :: (Πx : T1 .K)@AΓ ⊢ T :: K@AαΓ ⊢ ▷α T :: K@AK-▷Γ ⊢ T1 :: ∗@AK-VarΓ ⊢ t1 : T1 @AΓ ⊢ T2 t1 :: K[x 7→ t1 ]@AΓ⊢t:T

Γ, x : T @A ⊢ K kind@A

Γ, x : T1 @A ⊢ T2 :: K2 @AΓ ⊢ (Πx : T1 .T2 ) :: (Πx : T1 .K2 )@AΓ ⊢ T :: K@AΓ ⊢ K ≡ K ′ kind@AΓ ⊢ T :: K@A

K-App

K-Abs

Γ ⊢ T :: K ′ @Aα∈
/ FTV(Γ) ∪ FTV(A)Γ ⊢ ∀α.T :: K@A

K-Gen

K-ConvΓ ⊢ T :: K@AΓ ⊢ T :: K@Aα

K-Csp

TypingΓ ⊢ T :: ∗@AΓ, x : T @A, ∆ ⊢ x : T @A

Γ ⊢ t1 : (Πx : T2 .T1 )@AΓ ⊢ T2 :: ∗@AT-VarΓ ⊢ (λx : T2 .t1 ) : (Πx : T2 .T1 )@AΓ ⊢ t2 : T2 @AΓ ⊢ t1 t2 : T1 [x 7→ t2 ]@AΓ ⊢ t : T @Aα
Γ ⊢▶α t : ▷α T @A

T-▶

Γ, x : T2 @A ⊢ t1 : T1 @A

T-AppΓ ⊢ t : ▷α T @A
Γ ⊢◀α t : T @AαΓ ⊢ t : ∀α.T @AΓ ⊢ t ϵ : T [α 7→ ϵ]@A

T-◀

T-Ins

Γ ⊢ T ≡ T ′ :: ∗@AΓ ⊢ t : T @A

Γ ⊢ t : T ′ @AΓ ⊢ t : T @A

T-Abs

T-Convα∈/ FTV(Γ) ∪ FTV(A)Γ ⊢ Λα.t : ∀α.T @AΓ ⊢ t : T @A
Γ ⊢ %α t : T @Aα

T-Gen

T-Csp

ただし

FTV(Γ) は環境 Γ 中の，FTV(A) はステージ A 中の自由なステージ変数の集合を表す．
Γ ⊢ T1 ≡ T2 :: K@A は Γ ⊢ T1 ≡ T2 @A かつ Γ ⊢ T1 :: K@A かつ Γ ⊢ T2 :: K@A の略記であり，
Γ ⊢ K1 ≡ K2 kind@A は Γ ⊢ K1 ≡ K2 @A かつ Γ ⊢ K1 kind@A かつ Γ ⊢ K2 kind@A の略記である．
図1

λMD の型付け規則，カインド付け規則，カインドの適格性判断規則

Γ ⊢ t : Vect (3 + 4)@ϵΓ ⊢ Vect(3 + 4) ≡ Vect 7@ϵ
T-ConvΓ ⊢ t : Vect 7@ϵ
図2

T-Conv の使用例

る．Q-Abs，Q-App，Q-▶，Q-◀，Q-Gen，Q-Ins，を等価性に入れる規則である．Q-Csp は CSP を表

Q-Csp は ≡ を項に関する合同関係にするための規則

す記号% を扱うために導入された規則である．このである．同値関係に関する規則は Q-Refl，Q-Sym，

規則の意味は，ある項 t1 がステージ A と Aα の両方

Q-Trans である．簡約規則に関する規則は Q-β ，で導出されたならば，%α t1 と t1 を等価性に加える

Q-◀▶，Q-Λ，Q-%である．このうち Q-β ，Q-◀▶，というものである．λMD ではステージ変数に ϵ 以外

Q-Λ はそれぞれ −→β ，−→◀▶ ，−→Λ に対応するもを代入することはないことから，この規則の正当性がのであり，簡約される前の項と簡約された後の項の組確認できる．つまりすべてのコード化されたプログラΓ ⊢ K1 ≡ K2 @A

Kind Equivalence≡ の合同性のための規則Γ ⊢ T1 ≡ T2 :: ∗@AΓ, x : T1 @A ⊢ K1 ≡ K2 @AΓ ⊢ Πx : T1 .K1 ≡ Πx : T2 .K2 @A

QK-AbsΓ ⊢ K1 ≡ K2 @AΓ ⊢ K1 ≡ K2 @Aα

QK-Csp≡ を同値関係にするための規則
Γ ⊢ K kind@AΓ⊢ K≡KAΓ ⊢ K1 ≡ K2 @A

QK-ReflΓ ⊢ K1 ≡ K2 @AΓ ⊢ K2 ≡ K1 @AΓ ⊢ K2 ≡ K3 @AΓ ⊢ K1 ≡ K3 @A

QK-Trans

λMD のカインド等価性規則

図3

Γ ⊢ T1 ≡ T2 @A

QK-SymType Equivalence≡ の合同性のための規則Γ ⊢ T1 ≡ T2 :: ∗@AΓ, x : T1 @A ⊢ T3 ≡ T4 @AΓ ⊢ Πx : T1 .T3 ≡ Πx : T2 .T4 @AΓ ⊢ T1 ≡ T2 :: Πx : T3 .K@A

Γ ⊢ t1 ≡ t2 : T3 @AΓ ⊢ T1 t1 ≡ T2 t2 @AΓ ⊢ T1 ≡ T2 @AαΓ ⊢ ▷α T1 ≡ ▷α T2 @AΓ ⊢ T1 ≡ T2 @A

QT-▷

QT-AbsQT-Appα∈/ FTV(Γ) ∪ FTV(A)Γ ⊢ ∀α.T1 ≡ ∀α.T2 @AΓ ⊢ T1 ≡ T2 @AΓ ⊢ T1 ≡ T2 @Aα

QT-GenQT-Csp≡ を同値関係にするための規則Γ ⊢ T :: K@AΓ ⊢ T ≡ T @A

Γ ⊢ T1 ≡ T2 @A

QT-ReflΓ ⊢ T1 ≡ T2 @AΓ ⊢ T2 ≡ T1 @AΓ ⊢ T2 ≡ T3 @AΓ ⊢ T1 ≡ T3 @A

QT-Sym

QT-Trans

ただしΓ ⊢ t1 ≡ t2 : T @A は Γ ⊢ t1 ≡ t2 @A かつ Γ ⊢ t1 : T かつ Γ ⊢ t2 : T の略記であり，
Γ ⊢ T1 ≡ T2 :: K@A は Γ ⊢ T1 ≡ T2 @A かつ Γ ⊢ T1 :: K かつ Γ ⊢ T2 :: K の略記である．
図4

λMD の型等価性規則

ムが実行されたあとでは，すべてのステージ変数に ϵ

カインドに関する合同関係にするための規則であり，が代入され%はすべて消滅するので，%α t1 と t1 は全QK-Abs，QK-Cps が該当する．2 種類目は ≡ を同値

く同じ項になる．

関係にするための規則であり，QK-Refl，QK-Sym，

カインド等価性はカインド上の関係 ≡ を定義する規則であり，2 種類に分けられる．1 種類目は ≡ を

QK-Trans が該当する．
これらの等価性の規則は，単純型付きラムダ計算のΓ ⊢ t1 ≡ t2 @A

Term Equivalence≡ の合同性のための規則
Γ ⊢ S1 ≡ S2 @A

Γ, x : S1 @A ⊢ t1 ≡ t2 @AΓ ⊢ λx : S1 .t1 ≡ λx : S2 .t2 @AΓ ⊢ t1 ≡ s1 : (Πx : T2 .T1 )@AΓ ⊢ t2 ≡ s2 : T2 @AΓ ⊢ t1 t2 ≡ s1 s2 @AΓ ⊢ t1 ≡ t2 @Aα
Γ ⊢▶α t1 ≡▶α t2 @AΓ ⊢ t1 ≡ t2 @A

Q-AppΓ ⊢ t1 ≡ t2 : ▷α T @AQ-▶

Γ ⊢◀α t1 ≡◀α t2 @Aαα∈/ FTV(Γ) ∪ FTV(A)Γ ⊢ Λα.t1 ≡ Λα.t2 @A

Q-Abs

Γ ⊢ t1 ≡ t2 : ∀α.T @A

Q-GenΓ ⊢ t1 ≡ t2 @AΓ ⊢ %α t1 ≡ %α t2 @AαQ-◀

Γ ⊢ t1 ϵ ≡ t2 ϵ@A

Q-Ins

Q-Csp

≡ を同値関係にするための規則Γ ⊢ t ≡ t@A

Q-ReflΓ ⊢ t ≡ s@AΓ ⊢ s ≡ t@AΓ ⊢ t1 ≡ t2 @A

Q-Sym

Γ ⊢ t2 ≡ t3 @AΓ ⊢ t1 ≡ t3 @A

Q-Trans

簡約規則に関する規則

Γ, x : S@A ⊢ t : T @A

Γ ⊢ s : S@AΓ ⊢ (λx : S.t) s ≡ t[x 7→ s]@AΓ ⊢ Λα.t1 : ∀α.T1 @AΓ ⊢ (Λα.t1 ) ϵ ≡ t1 [α → ϵ]@AQ-Λ

Γ ⊢ t1 ≡ t2 @A

Q-β

Γ ⊢◀α (▶α t1 ) ≡ t2 @AΓ ⊢ t1 : T1 @AαQ-◀▶

Γ ⊢ t1 : T1′ @AΓ ⊢ %α t1 ≡ t1 @Aα

Q-%

ただし

Γ ⊢ t1 ≡ t2 : T @A は Γ ⊢ t1 ≡ t2 @A かつ Γ ⊢ t1 : T かつ Γ ⊢ t2 : T の略記である．
図5

λMD の項等価性規則

簡約だけでなく，ステージに関する抽象やその簡約，

Index は範囲付きの整数を表す．

CSP の記号%を扱えるように定義されている．既存

Index は整数 i を受け取って，範囲を 0 から i − 1

研究にはこのような等価性の規則は存在しないため，に制限した整数の型を返す．例えば (Index 13) 型のこれらの規則は本研究の貢献である．

x は 0 から 12 までの値しか取らない．これは 1.1 節で導入した Index 型と同じものである．

3 例

さらに，(Index 13) 型の値 m をステージ α で定義

λMD によって型付けされる例を一つ挙げる. まずしている．プログラム中では型 Index (%α 13) を持

わかりやすさのために let 式を使って例を表示したあつ変数 y に m を代入し，その後その y をそのまま返MDと, let 式を λに変換して表示し，その型付け導出を表示する．ただしこの節では整数 Int を定義せずに使う．
ラムダ項と適用を let 式に変換したものを図 6 に示す．この例では環境で型変数 Index を定義している．

すという処理をコード化している．

let 式を用いずに同じ例を表示したものを図 7 に示
し，更にその型付け導出木を図 8 に示す．導出木のサイズが非常に大きいので，導出木を 3 つに分割している．

導出木のうち λMD に特徴的な部分を説明する．
まず label-p1 で変数 y が型 Index (%α 13)@α を持
つことを導出している．導出木の左上の部分において，K-Csp で型変数 Index をステージ ϵ からステー
ジ α に持ち上げて使えるのは λMDの大きな特徴である．K-Csp がなければ型変数 Index をステージ ϵ でも定義しておく必要がある．
さらに label-p2 で型 Index (%α 13) と型 Index 13
がステージ α で等価であることを導出している．特に左上の部分において，QT-Csp を用いて型 IndexΓ ⊢ T2 :: K1 @A．
• Γ ⊢ t1 ≡ t2 @A かつ Γ ⊢ t1 : T1 @A ならばΓ ⊢ t2 : T1 @A．
定理 3 (簡約による型の保存).

• Γ ⊢ t1 : T1 @A かつ t1 −→β t2 ならばΓ ⊢ t2 : T1 @A．
• Γ ⊢ t1 : T1 @A かつ t1 −→◀▶ t2 ならばΓ ⊢ t2 : T1 @A．
• Γ ⊢ t1 : T1 @A かつ t1 −→Λ t2 ならばΓ ⊢ t2 : T1 @A．

が型 Index とステージ α で等価であることを導出し進行性を示すためには λMD における値を定義するており，これは λMD で新たに導入した QT-Csp が必要がある．しかし，λMD は λ▷% の拡張であり，さ機能している例である．

らに項の構文は λ▷% と同じであるため，λMD の進行
性は λ▷% の進行性に簡単に帰着できる．本研究では

4 性質と証明

λ▷% の値の定義を流用して，λMD の進行性を示す予λMD の満たすべき性質について述べる. 本研究で

定である．

はλ

MD

の強正規化性，合流性と型健全性を証明することを目標としている．

5 関連研究λMD の強正規化性は λLF と同様に λMD の強正規

プログラミング言語における依存型の理論は 1980

化性を単純型付けラムダ計算のそれに帰着させるこ

年代半ばに確立された．この時期の依存型に関するとで示すことができる．

論文として，Meyer と Reinhold による λΠ [9]，Co-

λMD の合流性は簡約に関する帰納法で弱合流性を

quand と Huet による Calculus of Constructions [4]，示したあと，Newman’s Lemma と強正規化性から示Harper，Honsell，Plotkin による λLF [7] が挙げられせる．

る．本研究では依存型の基礎として Aspinall, Hoﬀ-

型健全性を示すためには簡約による型の保存と，型

man [1] を使った．

のつく項に対する簡約の進行性を示す必要がある．簡

依存型を扱えるプログラミング言語としては Idris

約による型の保存は以下の定理を導出に関する帰納[3] が存在する．また，Coq [12] や Agda [2] などの定法で証明することで示せると考えている．

理証明支援システムでも依存型を使うことができる．

定理 1 (代入補題).

依存型を実際にプログラムの安全性向上のために用

Γ, x : T2 @B, ∆ ⊢ J@A かつ Γ ⊢ t2 : T2 @B

いた研究としては Xi と Pfenning によるもの [14] がならば Γ, ∆[x 7→ t2 ] ⊢ J[x 7→ t2 ]@A．

ある．この研究では Standard ML を限定された形のた だ し t1 : T1 @A, T1 :: K1 @A, K1 kind@A,

t1 ≡ t2 @A, T1 ≡ T2 @A, K1 ≡ K2 @A をまとめ依存型を使えるように拡張し，配列の境界検査の回数を減らすことに成功している．

て J@A と書く.

一方，マルチステージプログラミングの型理論も長定理 2 (整合性).

く研究されている．Davies は λ◦ [5] でマルチステー• Γ ⊢ T1 :: K1 @A ならば Γ ⊢ K1 kind@A.

ジプログラミングと様相論理の間にカリーハワード同• Γ ⊢ t1 : T1 @A ならば Γ ⊢ T1 :: ∗@A.

型があることを明らかにした．しかし，λ◦ にはコー• Γ ⊢ K1 ≡ K2 @A かつ Γ ⊢ K1 kind@A

ドの実行や CSP が存在しなかった．

ならば Γ ⊢ K2 kind@A．

• Γ ⊢ T1 ≡ T2 @A かつ Γ ⊢ T1 :: K1 @A ならば

Taha と Sheard は MetaML [11] でコードの実行と CSP を導入した．さらに Taha と Nielsen は λαIndex :: Πx : Int. ∗ @ϵ, m : Index 13@α ⊢ (▶α ( let y = m : Index (%α 13) in y)) : ▷α Index 13@ϵ
図6

見やすさのために let 式を用いて表示した λMD のプログラムの例

Index :: Πx : Int. ∗ @ϵ, m : Index 13@α ⊢▶α ((λ(y : Index (%α 13)).y) m) : ▷α Index 13@α
図7

let 式を用いずに表示した λMD のプログラムの例

Γ を Index :: Π(x : Int). ∗ @ϵ, m : Index 13@α とする．
p1 を Γ, y : Index (%α 13)@α ⊢ y : Index(%α 13)@α とする．
p2 を Γ, y : Index (%α 13)@α ⊢ Index (%α 13) ≡ Index 13@αとする．

(goto label-p1 )(goto label-p2 )
..
p1
p2
.
T-ConvΓ, y : Index (%α 13)@α ⊢ y : Index 13@αΓ ⊢ Index (%α 13) : ∗@αT-AbsΓ ⊢ (λ(y : Index (%α 13)).y) : Π(y : Index 13).Index 13@αΓ ⊢ (λ(y : Index (%α 13)).y) m : Index 13@αT-▶
Γ ⊢▶α ((λ(y : Index (%α 13)).y) m) : ▷α Index 13@ϵ..
.
Γ ⊢ m : Index 13@αT-Applabel-p1 :Γ′ を Index :: Πx : Int. ∗ @ϵ, m : Index 13@α, y : Index (%α 13)@α

とする．

..
.
Γ′ ⊢ 13 : Int@ϵT-Csp
Γ′ ⊢ (%α 13) : Int@αK-AppΓ′ ⊢ Index (%α 13) :: ∗@αT-VarΓ, y : Index (%α 13)@α ⊢ y : Index (%α 13)@α..
.
Γ′ ⊢ Index :: Πx : Int. ∗ @ϵK-Csp
Γ′ ⊢ Index :: Πx : Int. ∗ @αlabel-p2 :Γ′ を Index :: Π(x : Int). ∗ @ϵ, m : Index 13@α, y : Index (%α 13)@α

とする．

...
..
Γ ⊢ Index :: Πx : Int. ∗ @ϵ.
..
..
QT-ReflΓ ⊢ Index ≡ Index@ϵΓ ⊢ Index :: Πx : Int. ∗ @ϵ.
.
QT-CspK-Csp
Γ′ ⊢ Index ≡ Index@αΓ′ ⊢ Index :: Πx : Int. ∗ @αΓ′ ⊢ 13 : Int@αΓ′ ⊢ 13@ϵQ-%
略記Γ′ ⊢ Index ≡ Index :: Πx : Int. ∗ @αΓ′ ⊢ (%α 13) ≡ 13 : Int@α
QT-AppΓ, y : Index (%α 13)@α ⊢ Index (%α 13) ≡ Index 13@α
図8

λMD における型付け導出[10] で Environment Classifer を導入し，bracket，es-

Hanada と Igarashi は λ▷% で λ▷ に CSP を付け加

cape，run，cross-stage persistence の 4 種類の操作えることに成功した．λ▷% は本研究におけるマルチを可能であり，型安全な型システムを構築した．まステージプログラミングの体系の基礎である．

▷

た，Tsukada と Igarashi は λ [13] で Environment

実際に使えるマルチステージプログラミング言語とClassifer を含む計算体系に対応する論理体系を発見しては BER MetaOCaml [8] が挙げられる．MetaO-

し，Environment Classifer を ϵ で置き換えることでCaml BER はコードの実行や CSP をサポートしてコードの実行を表現できることを示した．

いる．

いずれの体系も依存型を扱っておらず，我々の知る限り bracket, escape, run, CSP を持つ依存型システ
ムは本研究が初めてである．

6 おわりに
本研究は依存型を含むマルチステージプログラミ
ングの型理論 λMD を定義した．特にコード化された
値をパラメータに持つ型の等価性規則と，CSP を含むマルチステージプログラミング言語におけるカイ
ンド付け規則，カインドの適格性判断規則を与えた．
今後は定義した型システムと簡約規則のもとで，強正規化性と型健全性が保たれることを示す．現在，この証明に着手しており，既存研究と同一の手法で証明する予定である．
さらに λMD を実際に使うために，λMD を基礎とした型システムを設計し，そのインタプリタや JIT コ
ンパイラの作成を予定している．インタプリタだけ
でなく JIT コンパイラを作成する理由は，マルチス
テージプログラミングの利点が活かされる可能性があると考えているからである．

謝辞
原稿を読み，有益なコメントを寄せてくれた馬谷誠二氏に謝意を表したい．本研究は JSPS 科研費

17H01723 の助成を受けたものである．
参 考 文 献[ 1 ] Aspinall, D. and Hofmann, M.: Advanced topics
in types and programming languages, MIT press,
2005, chapter 2 Dependent Types.
[ 2 ] Bove, A., Dybjer, P., and Norell, U.: A Brief
Overview of Agda — A Functional Language with
Dependent Types, Proceedings of the 22nd International Conference on Theorem Proving in Higher
Order Logics, TPHOLs ’09, Berlin, Heidelberg,
Springer-Verlag, 2009, pp. 73–78.

[ 3 ] Brady, E.: Idris, a general-purpose dependently
typed programming language: Design and implementation, Journal of Functional Programming,Vol. 23, No. 5(2013), pp. 552–593.
[ 4 ] Coquand, T. and Huet, G.: The calculus of constructions, Technical Report RR-0530, INRIA, May1986.
[ 5 ] Davies, R.: A temporal-logic approach tobinding-time analysis, Logic in Computer Science, 1996. LICS’96. Proceedings., Eleventh Annual IEEE Symposium on, IEEE, 1996, pp. 184–
195.
[ 6 ] Hanada, Y. and Igarashi, A.: On cross-stage persistence in multi-stage programming, International
Symposium on Functional and Logic Programming,
Springer, 2014, pp. 103–118.
[ 7 ] Harper, R., Honsell, F., and Plotkin, G.: A
framework for defining logics, Journal of the ACM(JACM), Vol. 40, No. 1(1993), pp. 143–184.
[ 8 ] Kiselyov, O.: The Design and Implementation of
BER MetaOCaml - System Description, Functionaland Logic Programming - 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6,
2014. Proceedings, Codish, M. and Sumii, E.(eds.),
Lecture Notes in Computer Science, Vol. 8475,
Springer, 2014, pp. 86–102.
[ 9 ] Meyer, A. R. and Reinhold, M. B.: ”Type” isNot a Type, Proceedings of the 13th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages, POPL ’86, New York, NY, USA,ACM, 1986, pp. 287–295.
[10] Taha, W. and Nielsen, M. F.: Environment classifiers, ACM SIGPLAN Notices, Vol. 38, No. 1,
ACM, 2003, pp. 26–37.
[11] Taha, W. and Sheard, T.: MetaML andMulti-stage Programming with Explicit Annotations, Theor. Comput. Sci., Vol. 248, No. 1-2(2000),
pp. 211–242.
[12] The Coq Development Team: The Coq Proof
Assistant Reference Manual, 2009.
[13] Tsukada, T. and Igarashi, A.: A Logical Foundation for Environment Classifiers, Logical Methods
in Computer Science, Vol. Volume 6, Issue 4(2010).
[14] Xi, H. and Pfenning, F.: Eliminating Array
Bound Checking Through Dependent Types, Proceedings of the ACM SIGPLAN 1998 Conference
on Programming Language Design and Implementation, PLDI ’98, New York, NY, USA, ACM, 1998,
pp. 249–257.