Agda による定式化された型推論器の拡張と改良
門脇 香子, 浅井 健一
お茶の水女子大学大学院 人間文化創成科学研究科
kado@pllab.is.ocha.ac.jp, asai@is.ocha.ac.jp
概 要Agda はマルティンレフの型理論に基づいた定理証明支援器であり、その一方で関数型プログラミング言語でもある。Agda では依存型 (Dependent Types) を用いることができるのも大きな特徴である。また、定理証明支援器とプログラミング言語両方の特徴をもちあわせていることから、何かを実装しつつ証明するのに適している。既存研究で我々は、McBride の理論をもとにして Agda による unification を実現し、それを用いて正当性が保証された型推論器を Agda により構成した。しかし、そこで完成させた型推論器は型変数の数を人の手によって計算・管理するもので、証明は煩雑であった。
また、型を固定されたコンストラクタとして定義していたことにより、構文や型を拡張する際にさまざまな証明を書きなおさなければならなかった。そこで本研究では変数の数を不等式によって管理し、加えて type descriptor を用いて型を一般的に定義すること
で、構文の拡張と証明の簡略化を可能にした。

1

Introduction

Agda [7] は Haskell に似た構文を持つ依存型を用いた定理証明支援機構及びプログラミング言語であり、プログラミング言語と定理証明支援機構の両面を持っていることから、何かを実装しつつその正当性を証明することに適している。依存型とは値に依存する型のことであり、例えば List n(n は自然数) という型は「長さ n のリスト」という意味を持つ型のことである。これを応用すると「ある言語の項のうち、言語内で Int 型が付けられるもの」などを表現することも可能になる。また、
Agda は論理体系としてマルティンレフ型理論 [9] に基づいている。

1.1

研究背景

McBride は、型変数の数を巧妙に管理することで構造に従った再帰を使って（つまり停止性が明
らかな形で）型の unification を表現できることを示した [5]。我々は昨年、この unification の理論をもとにして unification を実装し、それを用いて型変数の数を管理することによって、正当性の証
明のついた型推論器を完全に pure functional に実装した [3]。
しかし、実装した型推論では、型変数の数を count 関数で数え、型変数の数が矛盾しないことを巧妙に管理する必要があった。この手法は、各構文に合わせて必要な型変数の数をいちいち数えるとともに、その数を型に含む命題を証明しなくてはならないため、人手で型変数の数を合わせなくてはならず、証明が（不可能ではないにしろ）非常に困難であった。さらに、これまでの型推論は、特定の型を対象にして作られていたため、構文を拡張して別の型を導入しようとすると、新しい構
文の型推論に加えて、代入や unification など基本的な操作を全て再実装する必要があった。そのため、新しい型の導入が困難であった。

1.2

研究概要

前節で示した 2 つの問題のうち、前者の問題を回避するため、今回の型推論器では、型変数を数ではなく不等式を持ち歩くことで管理する手法を採用する。正確な数ではなく、満たすべき条件を不等式の形で持ち歩くことで、その条件さえ満たせば型推論を行えるようになる。満たすべき条件

1

は、証明の他の部分から必然的に導かれてくるため、必要な証明を Agda に指示されるままに証明すれば良く、証明は以前と比べてずっと簡明になる。その結果、型変数の数を考慮した型推論を入出力付きの型規則の形で定式化できた。
一方、もうひとつの問題を回避するため、型定義に generic programming [6] の考え方を取り入れる。McBride が示した unification [5] は関数型のみを対象とするものだったが、それを sum of
product の形で表現される任意の型に拡張する。いったん、このような拡張を行うと、任意のデータ型に対する unification を行えるようになり、新たな型を導入する際にも同じ unification をそのまま使用することができるようになる。その結果、新たな構文を加える際には、その構文に対する型
推論部分のみを実装すれば良いことになる。本稿では、その例として組（Fst, Snd, Cons）を示す。
本稿の貢献は、以下の４点にまとめられる。

• 不等式に基づいた型推論を Agda で実装するとともに、それを型規則の形で定式化した。不等式制約を用いることで、以前の実装よりも簡潔な証明が得られた。
• McBride が示した unification の機構 [5] を sum of product の形で表現される任意の型に拡張した。これにより、型の拡張を簡単にした。
• 型推論の結果、得られた型付き項から型を取り除くと元の項が得られることも証明した。
• 型推論の拡張の例として、組を導入した。
以下、2 節では、型推論器で用いる構文と型定義を示す。3 節では、 McBride による unificationに加えて unification の正当性を保証した機構とその実装について述べる。4 節では、正当性の証明がついた型推論器の実装について、不等式を用いた代入について述べたのち、必要な証明に留意しながら述べる。5 節では、構文を拡張するにあたり使用した generic programming の手法について述べる。6 節では、5 節で拡張した構文 Fst, Snd, Cons それぞれに対して型推論の実装を与えていく。7 節で本稿のまとめを行う。なお、ここで示した型推論器の実装は以下の URL で公開している。
http://github.com/kdxu/InferAgda

型と構文の定義2

本節では、まず型推論器を実装するにあたって用いる型と構文、 unification の定義を見ていく。

2.1

型定義と推論規則

型定義は以下のように表現する。

τ= m | τ1 → τ2

自然数 m は型変数を表し、τ1 → τ2 は関数型を表している。
項は以下のように表現する。

M= x | λx. M1 | App M1 M2

型判断は以下の通りに行う。

Γ⊢M :τ
これは「型環境 Γ のもとで項 M は型 τ を持つ」と読む。
また、型規則は以下のようになる。

Γ(x) = τΓ⊢x:τ

Γ, x : τ2 ⊢ M1 : τ1
Γ ⊢ λx. M1 : τ2 → τ1

Γ ⊢ M1 : τ2 → τ1 Γ ⊢ M2 : τ2
Γ ⊢ App M1 M2 : τ12

上に示したのは通常の型規則だが、本論文では型推論を表現するために以下のような特別な型判
断を使う。
′′

′′

′

m
(m)
σ[↓m
) ⊢ M : τ (m )m′ ](↑m Γ′′′′
ここで、入力（赤）は Γ, m, M で、出力（青）は σ, m′ , m′′ , τ である。（↑mm は m と m から自動で挿入される。）Γ と τ の肩の添字は、「最大でいくつの型変数が現われ得るか」を示す。例え(m)ば、Γ
は 0 から m − 1 までの番号がついた型変数が現われ得る。この型判断は以下のように読む。
「型変数を最大 m 個持つ型環境 Γ のもとで項 M の型を推論すると、型変数を最大 m′ 個含む型 τ が推論される。その推論途中で、新しい型変数を m′′ 個まで割り当てる。その m′′ 個の型変数′′′は、σ[↓mm′ ] で表される代入によって単一化が起こり、m 個に減る。推論結果は以下を満たす。型
環境 Γ の型変数の数を m′′ まで持ち上げてから代入 σ をかけて得られた型環境のもとで項 M は型 τ を持つ。」
このような形で型推論を記述すると、型推論の結果、得られる型と代入が満たす性質も同時に記述できる。この書き方は後に述べる Agda による型推論の実装と厳密に対応したものとなっている。
Agda による型推論の実装をこのようなわかりやすい形で提示し、メタ変数の数も含めて厳密な形で型推論を定式化したのは、本論文の貢献のひとつである。
同様にして、型推論時の unification は、以下のように表現する。
′′′′(m′′ ) .
(m′′ )σ[↓m) = σ[↓m)m′ ](τ1m′ ](τ2

ここで、入力（赤）は τ1 , τ2 , m′′ で、出力（青）は σ, m′ である。τ1 と τ2 の肩の添字は、型変数の数を示す。この unification は以下のように読む。
′′「型変数を最大 m′′ 個持つ型 τ1 と τ2 は、型変数を m′′ 個から m′ 個まで減らす代入 σ[↓mm′ ] によって unification 可能である。」

2.2

構文定義

本稿の型推論器で用いる syntax は以下の通りである。変数の出現位置に関して de Bruijn index
を用いている。
入力される構文として、 自由変数の数が n 個の well-scoped な項として以下を定義する。
– 自由変数の数が n 個の well-scope な項
data WellScopedTerm (n : N) : Set where
Var : Fin n → WellScopedTerm n
Lam : (s : WellScopedTerm (suc n)) → WellScopedTerm n
App : (s1 : WellScopedTerm n) → (s2 : WellScopedTerm n) → WellScopedTerm n

ここで、Fin n は 0 から n − 1 までの有限集合の型である。
出力される構文として、 well-typed な項を定義する。
– WellTypedTerm Γ t : 自由変数の数が n 個– 型が t であるような well-typed な項
data WellTypedTerm {m n : N} (Γ : Cxt n) :Type m → Set where
Var : (x : Fin n) → WellTypedTerm Γ (lookup x Γ)
Lam : (t : Type m) → {t’ : Type m} → WellTypedTerm (t :: Γ) t’ → WellTypedTerm Γ (t ⇒ t’)
App : {t t’ : Type m} → WellTypedTerm Γ (t ⇒ t’) → WellTypedTerm Γ t → WellTypedTerm Γ t’

これは自由変数の数が n 個、型環境 Γ において型が t であるような well-typed な項を表している。
これは即ち term が書けた時点で well-typed であることが保証されるもので、 simply-typed の型規則をそのまま埋め込んでいる。

3

本節の型推論では、well-scoped な term を引数に取り型と必要な代入、対応する well-typed な
term を返す関数 infer を作ることを目的とする。また、well-typed term から型情報を削除して wellscoped term に戻す erase 関数を用いて、もとの term と推論後の term が同一であることを確かめている。

3

Unification

本節では、型推論に必要な型の unification について述べる。型の unification は、書き換え可能なセルを使うと簡明に実装することができる [10]。しかし、Agda では書き換えは許されないのに加えて、停止性が保証されている必要がある。
そこで McBride は「型変数が具体化されるたびに、具体化されていない型変数の数がひとつ減る」という点に注目した。m 個の「具体化されていない型変数」を Fin m 型の数字で表現し、そのm を減らすことで停止性が明らかな形の unification を実現した。ひとたび型変数をこのような形で表現できたら、その後の unification は通常通りに進む。具体的には、型の中に型変数が出現するかどうかを調べる関数 check を実装し、それを使って最汎の単一化子 (most general unifier) を求める。
今回はこの McBride の手法を用いて unification の関数 mgu を Agda で (今回使用する型定義の上で) 実装した。型定義は以下のようになる。
mgu : {D : Desc} → {m : N} → (t1 t2 : Fix D m) → Maybe (Σ [ m’ ∈ N ] AList D m m’)

ここで Desc 型は 5 節で説明する generic な型定義、Fix はその不動点である。Fix 型は unification を行う対象の型である。また AList D m m′ は、型変数の数を m から m′ にする代入の型である。
加えて、well-typed な型推論器の実装においては、unification の際に単一化を行う代入 σ を得る
のみでなく、「確かに単一化されている」という証明′′′′(m′′ ) .
(m′′ )σ[↓m) = σ[↓m)m′ ](τ1m′ ](τ2も返すことが必要となる。
そこで、mgu にこの証明を加えて返す mgu2 関数を実装した。型定義は以下のようになる。
– 型 t1 と t2 を unify する代入を、確かに unify できることの証明とともに返す
mgu2 : {D : Desc} → {m : N} → (t1 t2 : Fix D m) →Maybe (Σ [ m’ ∈ N ] Σ [ σ ∈ AList D m m’ ] substFix σ t1 ≡ substFix σ t2)

ここで、substFix σ t は型 t に対して代入 σ を施す関数である。

4型推論

本節では、以上の型定義、型規則、unification の実装を元に実際に型推論器を構成していく。本
稿の型推論では、algorithm W [1] の単相の部分を使用する。具体的には、型環境と well-scoped な
項 s をもらってきたら、s の型と必要な代入を Maybe モナドに包んで返す関数 infer を実装する。本節では、まず Var、Lam、App に関して証明を与える。

4

4.1

不等式を用いた代入

既存研究 [3] による型推論では、型変数の数を count 関数で数え、型変数の数が矛盾しない証明
と共に infer 関数に再帰的に持ち歩かせる必要があった。この手法は、構文に応じて型変数の数を人が厳密に数えて証明を実装する必要があり、型変数の数が複雑になる構文では実装が困難になるという問題があった。そこで今回の型推論器では、型変数を数ではなく不等式を持ち歩くことで管理する手法を採用した。
′′′′′
そもそも、代入 σ[↓mm′ ] は m 個の型変数を持つ型を m 個の型変数を持つ型にする代入であり、型判断は以下のように表現される。
′′

′′

′

m
(m)
σ[↓m
) ⊢ M : τ (m )m′ ](↑m Γ
′′

′′

m
′′
型環境における型変数の数が m である Γ に σ[↓mm′ ] を施すとき、↑m は m と m から自動で挿入される。これは「型変数の数を m′′ から m′ にする代入 σ を型変数の数が m である Γ に施すとき、まず Γ のメタ変数の数を持ち上げて型変数の数を m′′ に増やしてから代入を施す」という意味である。既存研究では、この m′′ がいくつであるか厳密に計算していた。しかし、この代入を施すためには m′′ が m 以上でなければならず、またその条件を満たす m′′ が存在すれば良い、ということがわかる。よって、m ≤ m′′ のとき、かつその時に限り、
′′

′′

m
(m) )
σ[↓m
m′ ](↑m Γ

を行うことができ、このとき、m′′ は「条件を満たしていれば」なんでもよく、型変数の数をつねに厳密に把握している必要はない。よって、持ち歩くべき制約は m ≤ m′′ で十分だということが分かった。型変数に関する制約がゆるくなったことにより、人は不等式の証明だけすればよくなり、型変数を事細かに手計算する必要がなくなった。

4.2

infer 関数の型実装すべき型推論器の関数定義は以下のようになる。
infer : (m : N) → {n : N} → (Γ : Cxt {m} n) → (s : WellScopedTerm n) →Maybe (Σ [ m” ∈ N ]Σ [ m’ ∈ N ]Σ [ m≤m” ∈ m ≤ m” ]
Σ [ σ ∈ AListType m” m’ ]
Σ [ τ ∈ Type m’ ]
Σ [ w ∈ WellTypedTerm (substCxt≤ σ m≤m” Γ) τ ]erase w ≡ s)

この関数は以下のものを入出力する。
入力• s : 最大で m 個の型変数をもつ WellScopedTerm• Γ : 型環境
出力• m′′ , m′ : N at
• m≤m′′ : m ≤ m′′ であることの証明• σ : m′′ 個の型変数を持つ型を m′ 個の型変数を持つ型にする代入• τ : 代入後の型 (Type m’)• w : WellTypedTerm Γ′ τ
• s ≡ erase w : 返された well-typed term s から型情報を削除したものが、もとの well-scoped
term と等しいという証明
以下の節で各構文に対する型推論の実装を説明する。各節の最後に最終的に得られた型推論を型規則の形で表現する。

5

4.3

Var

Var の型規則は以下のようになる。
Γ(x) = τΓ⊢x:τ
Var x の場合は、単に型環境に入っている x の型を返せばよいので、
Γ(x) = τϕ[↓mm ](Γ) ⊢ x : τとなり返す代入は ϕ[↓m
、返す型は τ 、返す term は Var x となる。
m ]（空の代入）
ここで注意する点は、空の代入を施した Γ を well-scoped term の型環境として返しているので、「型環境に対して空の代入を入れたものがもとの型環境と同一である」という証明
m (m) = Γ(m)ϕ[↓mm ]↑m Γを入れることで、 term の型が同一であることを明示的に示すことが必要になる点である。この証
明は、型環境の中のそれぞれの型 τ (m) に対して
(m) ) = τ (m)
ϕ[↓m
m ](τ

となることを示し、型環境の中のそれぞれの型 τ (m) に対してその証明を再帰的に与えてやればよい。
型推論をまとめると、以下のようになる。

Γ(m) (x) = τ (m)m (m) ) ⊢ x : τ (m)ϕ[↓mm ](↑m Γ

4.4

Lam

つぎに term がラムダ式 Lam s の形になっている場合である。型規則は以下のとおりである。

Γ, x : m(m+1) ⊢ s : τ1
Γ ⊢ Lam s : m(m+1) → τ1
ラムダ式の場合は、引数の型がどうなるかすぐにはわからないので、新しい型変数 m(m+1) を x の型に割り振った上で s の型推論を行う。s に型がついた場合には、「m(m+1) → s の型」が全体の型となる。
まず、新しい型変数 m(m+1) を型環境に加えた上で s の型推論を行うと、
′′

′′

′

m
m+1 Γ), x : m(m+1) )(m+1) ) ⊢ s : τ (m )σ[↓mm′ ](↑m+1 ((↑mなる σ 、τ を得る。これを変形すると、
′′

′′

′′

′′

′

m
m+1 Γ(m) ), x : σ[↓m ](↑m(m+1) ) ⊢ s : τ (m )
σ[↓m
m+1 m
m′ ](↑m+1 ↑mm′となる。
すると、Lam の型規則が適用できて、
′′

′′

′′

′′

′

m
m+1 Γ(m) ), x : σ[↓m ](↑m(m+1) ) ⊢ s : τ (m )
σ[↓m
m+1 m
m′ ](↑m+1 ↑m
m′
′′

′′

′′

′′

m(m+1) は新しい型変数′mm+1 Γ(m) ) ⊢ Lam s : σ[↓m ](↑m(m+1) ) → τ (m )
σ[↓m
m+1 m
m′ ](↑m+1 ↑m
m′

となる。
′′
m′′ (m) ) の形で出力するが、そのためには
ここで、この型推論では、返ってくる代入を σ[↓mm′ ](↑m Γ′′m′′
m+1 Γ(m) ) という式を σ[↓m′′ ](↑m′′ Γ(m) ) に変形出来ればよい。
σ[↓mmm′ ](↑m+1 ↑mm′
この変形は「型環境中の型変数の数を一気に持ち上げても、2 回に分けて持ち上げても同じ」という意味であり、直観的には正しいとわかるが、証明が必要になる。これは、Var x の場合と同様に型環境の中のそれぞれの型 τ に対してその性質を示してやればよく、

6

′

′

m+k τ (m) =↑m τ (m)↑mm
m+k ↑mが成り立っているということを示し、型環境の中のそれぞれの型 τ に対してその証明を再帰的に与えてやればよい。
この変形を用いると、先ほどの型推論は
′′

′′

′′

′′

′

m
m+1 Γ(m) ), x : σ[↓m ](↑m(m+1) ) ⊢ s : τ (m )
σ[↓m
m+1 m
m′ ](↑m+1 ↑m
m′

σ[↓

m′′
m′

m′′

m′′
m′

](↑m Γ(m) ) ⊢ Lam s : σ[↓m(m+1) は新しい型変数m′′′](↑m+1 m(m+1) ) → τ (m )

′′

′′

′′

′

m
m
(m+1) ) → τ (m ) となる。となる。必要な代入は σ[↓mm′ ] であり、返ってくる型は σ[↓m′ ](↑m+1 m以上の型推論をまとめると、以下のようになる。
′′

′′

′

m
m+1 Γ), x : m(m+1) )(m+1) ) ⊢ s : τ (m )σ[↓m1m′ ](↑m+1 ((↑m′′′′m(m+1) は新しい型変数

′′

′′

′

(m+1) ) → τ (m )m(m) ) ⊢ Lam s : σ[↓m ](↑m
σ[↓m
1
m+1 m
m′ ](↑m Γ
m′

4.5

App

App の型規則は以下の通り。
Γ ⊢ s1 : τ2 → τ1 Γ ⊢ s2 : τ2
Γ ⊢ App s1 s2 : τ1
App s1 s2 の型推論では、まず s1 を型推論すると、
m′′

m′′

′

σ1 [↓m1′ ](↑m1 Γ(m) ) ⊢ s1 : τ1 (m1 )1

なる σ1 と τ1 が得られる。
次に、得られた代入 σ1 をかけた型環境下で s2 を型推論し、
m′′

m′′

m′′

2

1

1

m′′

σ2 [↓m2′ ](↑m2′ (σ1 [↓m1′ ](↑m1 Γ(m) ))(m′1 )′) ⊢ s2 : τ2 (m2 )なる σ2 と τ2 を得る。
型推論が成功するには、τ1 は τ2 → β の形をしているはずなので、unification を行うと、
m′ +1

σ3 [↓m2′
3

′
′
m′′
m′′
m′ +1
m′ +1
.
(m′ +1)(σ2 [↓m2′ ](↑m2′ τ1 (m1 ) ))) = σ3 [↓m2′ ](↑m2′ τ2 (m2 ) → m′2 2 )m′ +1](↑m′2
2

2

1

3

2

′

(m′2 (m2 +1) は新しい型変数) となる σ3 と、上記の等式 eq が得られる。
次に、導出された式の両辺のメタ変数の数を持ち上げ、代入をかける。ここの四角は、枠内のすべての型変数に枠外のメタ変数の数の持ち上げや代入を行うという意味である。
m′ +1

σ3 [↓m2′
3

m′ +1](↑m2′
2

m′′

m′′

m′′

2

1

1

m′′

′

(σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ(m) ) ⊢ s1 : τ1 (m1 ) )))

すると、
m′ +1

σ3 [↓m2′
3

m′ +1

m′′

m′′

m′′

2

1

1

m′ +1

m′′

σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ(m) )))) ⊢ s1 : σ3 [↓m2′]((↑m2′2m′ +1](↑m2′
2

3

m′′

m′′

2

1

′

σ2 [↓m2′ ](↑m2′ τ1 (m1 ) ))のようになり、これの s1 の型は eq から
m′ +1

σ3 [↓m2′
3

m′ +1]((↑m2′
2

m′′

m′′

m′′

2

1

1

m′′

m′ +1

σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ(m) )))) ⊢ s1 : σ3 [↓m2′

m′ +1](↑m2′23′

τ2 (m2 ) → m′2(m′2 +1)となる。
また、s2 に関しても同様のことを行い
m′ +1

σ3 [↓m2′
3

m′ +1](↑m2′
2

m′′

m′′

m′′

2

1

1

m′′

′

′

σ2 [↓m2′ ](↑m2′ (σ1 [↓m1′ ](↑m1 Γ(m) ))(m1 ) ) ⊢ s2 : τ2 (m2 ) )

を
m′ +1

σ3 [↓m2′
3

m′ +1](↑m2′
2

m′′

m′′

m′′

2

1

1

m′′

′

m′ +1

σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ(m) )(m1 ) )) ⊢ s2 : σ3 [↓m2′
3と変形する。

7m′ +1](↑m2′2′

τ2 (m2 ) ))これらを用いると、App の型規則が適用できて
m′ +1

σ3 [↓m2′
3

2

m′ +1

σ3 [↓m2′
3

m′ +1

]↑m2′

m′ +1

](↑m2′
2m′ +1

σ3 [↓m2′
3

m′′

m′′

m′′

2

1

1

m′′

m′′

m′′

2

1

1

m′′

m′ +1

σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ(m) )) ⊢ s1 : σ3 [↓m2′
3

m′′

2

m′ +1

σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ(m) ))) ⊢ s2 : σ3 [↓m2′

m′ +1](↑m2′
2

3

m′′

m′′

m′′

2

1

1

m′ +1

](↑m2′

m′ +1](↑m2′
2

m′′

′

′

τ2 (m2 ) → m′2 (m2 +1) )′τ2 (m2 ) )m′ +1

σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ(m) ))) ⊢ App s1 s2 : σ3 [↓m2′
3′](m′2 (m2 +1) )が得られる。ここで、必要な代入を返すにあたり、σ3 , σ2 , σ1 を合成したものを返したくなるが、そのとき、以下の等式を示すことが必要になる。
m′′

m′′

m′ +1

σ[↓m3′ ](↑m3 Γ) = σ3 [↓m2′
3

3

m′ +1

](↑m2′

2

m′′

m′′

m′′

2

1

1

m′′

(σ2 [↓m2′ ](↑m2′ (σ1 [↓m1′ ](↑m1 Γ)))))

m′′3 = ((m′2 + 1) − m′2 ) + (m′′2 − m′1 ) + m′′1

ここで、σ は σ3 , σ2 , σ1 を合成したものである。これを示すには、型環境 Γ(m) のそれぞれの型 τ に
おいて
m′′
m′′
m′ +1
m′ +1
m′′
m′′
m′′
m′′
σ[↓m3′ ](↑m3 τ ) = σ3 [↓m2′ ](↑m2′ (σ2 [↓m2′ ](↑m2′ (σ1 [↓m1′ ](↑m1 τ )))))
3

3

2

2

1

1

が成り立つことを示し、この証明を各 τ に対して再帰的に与えてやれば良い。
ここで、σ は σ1 と σ2 と σ3 の合成であることから、これは「複数の代入を順に施すのは、代入を合成したものを１度に施すのと同じである」という意味であり、直感的にはこれらが等しいことは理解できる。
以下の手順により、これを証明することが出来る。

• 有限集合の型 Fin を不等式を用いて持ち上げる関数 inject≤ に関して推移律を示す。
• それを用いて、型の型変数を持ち上げる関数 liftFix≤ に関して推移律を示す。
• それを用いて、型に 2 つの代入を順に施すのと代入を合成したものを 1 度に施したものは同じであるということを示す。
代入の合成は、以下のように実装している。

• まず σ1 と σ2 を合成する場合、後ろの代入 σ2 を σ1 の型まで持ち上げ、持ち上げた σ2 を σ2′とする。
• σ2′ (のそれぞれの型と型変数の組) を σ1 の後ろに再帰的に追加する。
代入を持ち上げるとき、各要素の型と型変数を 1 ずつ持ち上げている。型を持ち上げるとき、型変数を持ち上げることが必要になるが、型変数を持ち上げるということは有限集合の型（すなわち型変数の型）Fin を持ち上げるということである。例えば、inject+’ m′ は Fin m を Fin (m′ + m) に持ち上げる関数である。これを用いて、liftFix という関数を型を「ちょうど m′ 個」持ち上げる関数として定義する。
しかし、型推論中、いくつのメタ変数を使うかを全て管理するのはとても煩雑である。むしろ、m ≤ m′′ である任意の m′′ まで持ち上げる形の方が後の証明がとても楽になる。それには inject+’
ではなく不等式を受け取ってその分だけ持ち上げる関数 inject≤ を全ての型変数に施すことで、不等式を受け取ったら型をその分だけ持ち上げる関数 liftFix≤ を定義する。
代入同士の合成では、この liftFix≤ を再帰的に用いて、代入を lift している。また、代入を実際に施す際も、liftFix≤ を用いて型を持ち上げてから、代入を施している。つまり、liftFix≤ の中で使われている inject≤ に関する推移律を示してやれば、証明はかなり長くなるが、上記の型環境が互いに等しいことを示すことが出来る。
また、ここの証明では、関数同士の同一性を示すため、Agda で用意されているデフォルトの公理に加え、外延性を仮定することが必要になる。

8

以上の証明を用いて型推論をまとめると、以下のようになる。
m′ +1

σ3 [↓m2′
3

m′ +1](↑m′2
2

m′ +1

m′ +1

m′′

m′′

m′′

2

1

1

m′′

m′′

m′′

2

1

](↑m2′

σ [↓

](↑

m2

は新しい型変数m′′2
m′2 +1
m′2′⊢ s1 : τ1 (m1 ) )))

m′′

′

m′′

m′ +1

σ[↓m3′ ](↑m3 τ ) = σ3 [↓m2′
3

3

3

m′ +1

](↑m2′

2

m′′

2

m′′

m′′

m′′

2

1

1

m′′

(σ2 [↓m2′ ](↑m2′ (σ1 [↓m1′ ](↑m1 τ )))))

m′′3 = ((m′2 + 1) − m′2 ) + (m′′2 − m′1 ) + m′′1
m′′

m′ +1

σ[↓m3′ ](↑m3 Γ(m) ) ⊢ App s1 s2 : σ3 [↓m2′
3

5′

σ2 [↓m2′ ](↑m2′ (σ1 [↓m1′ ](↑m1 Γ(m) ))(m1 ) ) ⊢ s2 : τ2 (m2 ) )
2
1
1
′
′)
′
m′′
m′′
m′ +1
m′ +1
.
(m
2
2
(σ2 [↓m′ ](↑m′ τ1 1 ))) = σ3 [↓m2′ ](↑m2′ τ2 (m2 ) → m′2 (m2 +1) )σ3 [↓m2′3
m′2 +13 m′
3′′ (m2 +1)m′′

(σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ(m) )3′](m′2 (m2 +1) )構文の拡張

これまでは型をコンストラクタを用いて構成していたが、この構成法だと新しい型（例えば直積型）などを加える際、型に対してパターンマッチを行って構成している mgu 関数や、型や型環境に対して lift や subst を行う関数を定義しなおさなければならず、型の拡張が面倒なものとなっていた。そこで今回は型を type discriptor を用いて表現する方法を採用した。

5.1

より一般的な型への拡張

単純型付き λ 計算に対する型推論のみが必要なのであれば、関数の型のみ扱えるような型推論を作れば良いが、いろいろな体系に対する型推論を作ろうと思えば多様な型を扱える必要がある。しかし、それぞれの体系ごとに別の型推論を実装し、その正当性を示すのは現実的ではない。そこで、
ここでは generic programming の考え方を取り入れて、ユーザが指定するいろいろな型を扱えるよ
うに全体を構築する。generic programming の中でも本稿で実装したのは Regular [6] である。
generic programming では、型の構成法を BNF に似た形で与える。例えば、単純型付き λ 計算の場合、型は次のように定義される。

τ = base | τ → τ
このような定義では、「または」を表す縦棒で選択肢が区切られ、各選択肢では列挙された要素で構成される。
（例えば τ → τ なら、ふたつの型から構成される。）そして、その要素は再帰的に型自身でも構わない。このような型を表現するため、generic programming では、次のような Desc 型のデータ構造を使う。
data Desc : Set1 wherebase : Desc_:+:_ : Desc → Desc → Desc_:*:_ : Desc → Desc → Desc
rec
: Desc

ここで base は適当な基底型（本稿では unit 型とする）、:+: は「または」、:*: は「かつ」を示し、rec はそこで再帰が起こることを示す。例えば、単純型付き λ 計算の型は、次のようなデータで定義する。
TypeDesc1 : Desc
TypeDesc1 = base :+: rec :*: rec

ここで最初の base が基底型を表し、次の rec :*: rec が τ → τ を表している。関数型の両辺は任意の型が来て良いため rec となっている。
これで型の定義を与えることが出来るようになったが、具体的な型を表現するためには、まず Descの Agda 上の表現（意味）を以下のように与える。

9

J_K : Desc → Set → Set
J base K X = ⊤J d1 :+: d2 K X = J d1 K X ⊎ J d2 K X
J d1 :*: d2 K X = J d1 K X × J d2 K X
J rec
KX=X

J D KX は、「再帰部分が X であるような Desc 型の値」を示す。この再帰部分 X に自分自身を入れる（再帰を閉じる）と、具体的に Desc 型の値を作ることが出来るようになる。再帰を閉じるには、
以下のデータを使う。
data Fix (D : Desc) (m : N) : Set where
F : J D K (Fix D m) → Fix D m
M : (x : Fin m) → Fix D m

ここで Fix D m 型の値は「型変数を m 個持つような D 型の値」を表す。F が具体的な値を作り出す構成子である。F の引数は J D K (Fix D m) となっているが、再帰部分に自分自身である Fix D mが入っているところに注目しよう。ここで、再帰を閉じることで任意に大きなデータを作ることが出来る。ここで、型変数を m 個持つ TypeDesc1 型の値（単純型付き λ 計算の型を表す型）を以下のように書くことにする。
Type1 : (m : N) → Set
Type1 m = Fix TypeDesc1 m

すると、例えば基底型は以下のように定義できる。
tbase1 : {m : N} → Type1 mtbase1 = F (inj1 tt)

また、関数型を作る関数を定義すると、さらに大きな型を定義できる。
_=>_ : {m : N} → Type1 m → Type1 m → Type1 m
t1 => t2 = F (inj2 (t1 , t2))
t1 : Type1 0
t1 = tbase1 => (tbase1 => tbase1)

ここで t1 は base → base → base を表す。
ここまでの例では、型のメタ変数は出て来なかったが、型推論を実装する際には任意の型に具体化可能なメタ変数が必要となる。それを表すのが Fix のもうひとつの構成子である M である。例
えばt1’ : Type1 2
t1’ = M zero => (tbase1 => M (suc zero))は、M zero と M (suc zero) のふたつのメタ変数を含む Type1 2 型の値である。
Fix を使って、任意の Desc 型に対応したデータを作れるようになったが、Fix で表現された値を使って計算するには fold の一般形を使う。リストに対する fold では、cons と nil に対応した処理を記述したが、Fix に対する fold では、F と M に対応する処理を記述する形になる。Fix に対する
fold は以下のように定義される。
{-# NO_TERMINATION_CHECK #-}fold : {D : Desc} → {m : N} → {X : Set} →(f-F : J D K X → X) → (f-M : Fin m → X) → Fix D m → X
fold {D} f-F f-M (F d) = f-F (fmap D (fold f-F f-M) d)fold f-F f-M (M x) = f-M x

10fold は、Fix D m 型の値を受け取ったら、その F 部分には f-F を適用し、M 部分には f-M を適用する。f-F や f-M は X 型の値を出力し、最終結果も X 型の値となる。f-F の第１引数の再帰部分がX となっていることに注意しよう。f-F が受け取る引数の再帰部分は、再帰的に計算をした結果となっている。実際、fold の定義の F d の場合を見ると、f-F の引数には fmap を使って fold f-F f-M
自身を再帰的に d に施した結果が渡されている。ここで、fmap は、Haskell の Functor にも見られる引数の関数を再帰部分に適用する関数で、以下のように定義される。
fmap : (D : Desc) → {X Y : Set} → (X → Y) → J D K X → J D K Y
fmap base f x = tt
fmap (D1 :+: D2) f (inj1 x) = inj1 (fmap D1 f x)
fmap (D1 :+: D2) f (inj2 x) = inj2 (fmap D2 f x)
fmap (D1 :*: D2) f (x1 , x2) = (fmap D1 f x1 , fmap D2 f x2)
fmap rec f x = f x – 再帰部分に f を適用する

このように fold は Fix D m 型のデータの構造に従って再帰的に計算を行う。従って fold の再帰の停止性はデータ構造の有限性から明らかである。しかし、プログラムの表面上は fold f-F f-M という再帰呼び出しが fmap に渡される形になっているため、Agda の停止性チェッカでは停止性を確認できない。そのため、fold 関数の定義では停止性チェックを行わないように指示している。
fold を使うと、例えば受け取った値のノード数を数えるには以下のようにする。
size-M : {m : N} → Fin m → N
size-M x = 1
size-F : {D : Desc} → J D K N → N
size-F {base} tt = 1
size-F {D1 :+: D2} (inj1 t) = size-F {D1} tsize-F {D1 :+: D2} (inj2 t) = size-F {D2} tsize-F {D1 :*: D2} (t1 , t2) = size-F {D1} t1 + size-F {D2} t2size-F {rec} t = t
size : {D : Desc} → {m : N} → Fix D m → N
size {D} = fold (size-F {D}) size-M

size-M は、メタ変数のサイズは 1 であることを、size-F は、base の大きさが 1 で、他は部分木の大きさの和であることを示している。この関数は任意の Desc に対して使うことができ、例えば先の t1’ なら size t1’ は 3 となる。
また、型のメタ変数の数を m’ 個増やす liftFix 関数は、fold を使って以下のように実装される。
– liftFix m’ t : t の中の型変数の数を m’ だけ増やす
liftFix : {D : Desc} → (m’ : N) → {m : N} → Fix D m → Fix D (m’ + m)
liftFix {D} m’ {m} t = fold F (M ◦ (inject+’ m’)) tt の中に出てくる全てのメタ変数に対して inject+’ m′ をかけている。inject+’ m′ は Fin m を Fin(m′ + m) に持ち上げる関数である。
inject≤ を使って m≤m′′ である任意の m′′ まで型を持ち上げる liftFix≤ 関数も、fold を用いて以下のように実装される。
– liftFix≤ m≤m’ t : t の中の型変数の数を m から m’ に増やす
liftFix≤ : {D : Desc} → {m m’ : N} → (m≤m’ : m ≤ m’) → Fix D m → Fix D m’
liftFix≤ m≤m’ t = fold F (M ◦ (λ x → inject≤ x m≤m’)) t

これらの liftFix, liftFix≤ を含む fold を使った関数はいずれも任意の Desc に対して動くことに注意しよう。このように generic に定義をしておくと、型推論をユーザの与えた任意の Desc に対して行うことが出来るようになる。

11

5.2

新しい構文と追加する型

構文を追加する例として、ここでは Cons, Fst, Snd を追加する。入力する term の構文として、以下を追加する。
Fst : WellScopedTerm n → WellScopedTerm n
Snd : WellScopedTerm n → WellScopedTerm nCons : WellScopedTerm n → WellScopedTerm n → WellScopedTerm n

また、出力する term の構文として、以下を追加する。
∏
Fst : {t1 t2 : Type m} → WellTypedTerm Γ (t1 ∏ t2) → WellTypedTerm Γ t1
Snd : {t1 t2 : Type m} → WellTypedTerm Γ (t1t2) → WellTypedTerm Γ t2∏
Cons : {t1 t2 : Type m} → WellTypedTerm Γ t1 → WellTypedTerm Γ t2 → WellTypedTerm Γ (t1t2)

本稿では、構文上、Agda の直積と区別するため、直積を × ではなく Π で表現していることに注意したい。
構文を拡張するにあたって、型と型規則を新たに加える。
型：= m | τ1 → τ2 | τ1 × τ2

τ

ここで、新たに直積型 τ1 × τ2 を加えている。
追加された型規則：
Γ ⊢ s 1 : τ1 Γ ⊢ s 2 : τ2
Γ ⊢ Cons s1 s2 : τ1 × τ2

Γ ⊢ s : τ1 × τ2
Γ ⊢ F st s : τ1

Γ ⊢ s : τ1 × τ2
Γ ⊢ Snd s : τ2

これらはそれぞれ、Cons、Fst、Snd に関する型規則である。

拡張された構文における型推論

6

前節では、generic programming と不等式の導入により、mgu 関数等を変更することなく、より簡単に構文を拡張することができた。本節では、拡張されたそれぞれの構文に対する型推論の実装を与えていく。

6.1

Cons

Cons の型規則は以下のとおりである。
Γ ⊢ s1 : τ1 Γ ⊢ s2 : τ2
Γ ⊢ Cons s1 s2 : τ1 × τ2
Cons s1 s2 の型推論では、まず s1 を型推論し、σ1 と型 τ1 、型変数 m′1 を得る。すると、以下の導出が得られる。
′
m′′m′′
σ1 [↓m1′ ](↑m1 Γ) ⊢ s1 : τ1 (m1 )1

つぎに、s2 を（s1 の型推論で得られた σ1 を適用した上で）型推論する。
m′′

m′′

m′′

2

1

1

m′′

′

σ2 [↓m′2 ](↑m2′ σ1 [↓m1′ ](↑m1 Γ)) ⊢ s2 : τ2 (m2 )つぎに、先ほどの s1 の式の両辺を σ2 で subst して、
m′′

m′′

m′′

2

1

1

m′′

′

σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ(m) ) ⊢ s1 : τ1 (m1 ) )

12

から

m′′

m′′

m′′

2

1

1

m′′

m′′

m′′

2

1

σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ)) ⊢ s1 : σ2 [↓m2′ ](↑m2′ τ1 )を得る。
すると、Cons の型規則が適用できて、
m′′

m′′

2

1

m′′

m′′

m′′

m′′

m′′

m′′

m′′

2

1

2

1

1

m′′

σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ)) ⊢ s1 : σ2 [↓m2′ ](↑m2′ τ1 ) σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ)) ⊢ s2 : τ2
1

m′′
m′′
m′′
m′′
m′′
m′′
σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ)) ⊢ Cons s1 s2 : σ2 [↓m2′ ](↑m2′ τ1 ) × τ2
2
1
2
1
1

が得られ、ここで σ を σ1 と σ2 の合成として
m′′′

m′′′

m′′

m′′

m′′

2

1

1

m′′

σ[↓m2′ ](↑m2 τ ) = σ2 [↓m2′ ](↑m2′ (σ1 [↓m1′ ](↑m1 τ )))
2

′′
′
′′
(m′′′
2 = (m2 − m1 ) + m1 ) と変形できれば、
m′′

m′′

m′′

2

1

1

m′′

m′′

m′′

m′′

m′′

m′′

2

1

2

1

1

m′′

σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ)) ⊢ s1 : σ2 [↓m2′ ](↑m2′ τ1 ) σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ)) ⊢ s2 : τ2
m′′′
m′′′
m′′
m′′
σ[↓m2′ ](↑m2 Γ) ⊢ Cons s1 s2 : σ2 [↓m2′ ](↑m2′ τ1 ) × τ2221となり、返ってくる代入として σ が得られる。
ここで、σ は σ1 と σ2 の合成であることから、これは「ふたつの代入を順に施すのは、代入を合成したものを１度に施すのと同じである」という意味であり、App の場合に用いた証明と同じもの
を用いて示す事ができる。
以上の型推論をまとめると、以下のようになる。
m′′

m′′

m′′

m′′

2
m′′
2
m′2
m′′′
2
m′2

1
m′′
2
m′1
m′′′
2

1
m′′
1
m′1

′

⊢ s1 : τ1 (m1 ) )σ2 [↓m2′ ](↑m2′ σ1 [↓m1′ ](↑m1 Γ(m) )(σ1 [↓

m′′′′](↑m1 Γ(m) ))(m1 ) ) ⊢ s2 : τ2 (m2 )

σ2 [↓

](↑

σ[↓

](↑m τ ) = σ2 [↓m2′ ](↑m2′ (σ1 [↓m1′ ](↑m1 τ )))

m′′

m′′

m′′

2

1

1

′′
′
′′
m′′′
2 = (m2 − m1 ) + m1
m′′′

m′′′

m′′

m′′

m′′

2

1

′

′

σ[↓m2′ ](↑m2 Γ(m) ) ⊢ Cons s1 s2 : σ2 [↓m2′ ](↑m2′ τ1 (m1 ) ) × τ2 (m2 )
2

6.2

Fst

Fst の型規則は以下のとおりである。
Γ ⊢ s : τ1 × τ2
Γ ⊢ F st s : τ1
Fst s の型推論ではまず s を型推論し、以下の導出を得る。
m′′

m′′

′

σ1 [↓m1′ ](↑m1 Γ) ⊢ s : τ (m1 )
1

m′ +2

′

′

また、新しい型変数 2 つ ↑m1′ +1 m′1 (m1 +1) と (m′1 + 1)(m1 +2) を用いると、s の型 τ1 は
m′ +2

1

′

′

↑m1′ +1 m′1 (m1 +1) × (m′1 + 1)(m1 +2) の形をしているはずなので unification を行い、成功した場合の1
み代入 σ2 と以下の等式 eq が得られる。
m′ +2
m′ +2
m′ +2
m′ +2
.
(m′ +1)(m′ +2)σ2 [↓m1′ ](↑m1′ τ ) = σ2 [↓m1′ ](↑m1′ +1 m′1 1× (m′1 + 1) 1 )
2

1

2

1

ここで、s の導出式の両辺に σ2 をかける。
m′ +2

σ2 [↓m1′

2

m′ +2](↑m1′

1

m′′

m′′

′

σ1 [↓m1′ ](↑m1 Γ(m) ) ⊢ s : τ (m1 ) )1すると、以下のようになる。
m′ +2

σ2 [↓m1′
2

m′ +2](↑m1′

1

m′′

m′′

m′ +2

σ1 [↓m1′ ](↑m1 Γ)) ⊢ s : σ2 [↓m1′
2

1

13

m′ +2

](↑m1′1τ)ここで、eq を適用すると、Fst の型規則が適用できて、
m′ +2

σ2 [↓m1′
2

m′ +2](↑m1′
1

m′′

m′′

m′ +2

σ1 [↓m1′ ](↑m1 Γ)) ⊢ s : σ2 [↓m1′
1

m′ +2

σ2 [↓m1′
2

m′ +2](↑m1′
1

2

m′′

m′ +2

′

′

](↑m1′ +1 m′1 (m1 +1) × (m′1 + 1)(m1 +2) )
1

m′′

m′ +2

σ1 [↓m1′ ](↑m1 Γ)) ⊢ F st s : σ2 [↓m1′
1

2

m′ +2

′

](↑m1′ +1 m′1 (m1 +1) )1が得られ、返り値として得られる代入 σ は、σ1 と σ2 を合成したものであり、
m′′

m′′

m′ +2

σ[↓m2′ ](↑m2 τ ) = σ2 [↓m1′
2

2

m′ +2

](↑m1′

m′′2 = ((m′1 + 2) − m′1 ) + m′′1

1

m′′

m′′

(σ1 [↓m1′ ](↑m1 τ )))1を満たすものである。ここで用いる証明は App で用いた「ふたつの代入を順に施すのは、代入を合成したものを 1 度に施すのと同じである」の証明と同じである。
以上の推論をまとめると以下のようになる。
m′ +2

m′ +2

m′′

m′′

′

σ1 [↓m1′ ](↑m1 Γ(m) ) ⊢ s : τ (m1 ) )
2
1
1
′
′
′)
m′1 +2m′1 +2
m′ +2
m′ +2
.
(m
σ2 [↓m′ ](↑m′ τ1 1 ) = σ2 [↓m1′ ](↑m1′ +1 m′1 (m1 +1) × (m′1 + 1)(m1 +2) )σ2 [↓m1′](↑m1′

2
′

1

2

′

1

m′1 (m1 +1) , (m′1 + 1)(m1 +2) は新しい型変数
m′′

m′′

m′ +2

σ[↓m2′ ](↑m2 τ ) = σ2 [↓m1′
2

2

m′ +2

](↑m1′

m′′

m′′

1

1

m′′2 = ((m′1 + 2) − m′1 ) + m′′1m′′

(σ1 [↓m1′ ](↑m1 τ )))

m′′

m′ +2

σ[↓m2′ ](↑m2 Γ(m) ) ⊢ F st s : σ2 [↓m1′
2

6.3

2

m′ +2

′

](↑m1′ +1 m′1 (m1 +1) )1

Snd

Snd の型規則は以下のとおりである。
Γ ⊢ s : τ1 × τ2
Γ ⊢ Snd s : τ2
Snd s に関しては、返される型が τ × τ ′ の τ ′ の方であるという部分のみ異なり、示すべき証明
は Fst s と同じである。
型推論は以下のようになる。
m′ +2

m′′

m′ +2

m′′

′

σ1 [↓m1′ ](↑m1 Γ(m) ) ⊢ s : τ (m1 ) )
2
1
1
′
′
′)
m′1 +2m′1 +2
m′ +2
m′ +2
.
(m
σ2 [↓m′ ](↑m′ τ1 1 ) = σ2 [↓m1′ ](↑m1′ +1 m′1 (m1 +1) × (m′1 + 1)(m1 +2) )σ2 [↓m1′](↑m1′

2
′

1

2

′

1

m′1 (m1 +1) , (m′1 + 1)(m1 +2) は新しい型変数
m′′

m′′

m′ +2

σ[↓m2′ ](↑m2 τ ) = σ2 [↓m1′
2

2

m′′2 = ((m′1 + 2) − m′1 ) + m′′1
m′′

m′ +2

](↑m1′

1

m′′

m′′

(σ1 [↓m1′ ](↑m1 τ )))
1

m′′

m′ +2

σ[↓m2′ ](↑m2 Γ(m) ) ⊢ Snd s : σ2 [↓m1′
2

7

まとめと今後の課題

7.1

まとめ

2

′

]((m′1 + 1)(m1 +2) )本研究では、既存研究である McBride [5] の手法を用いた正当性の証明がついた型推論器 [3] を
型変数を数ではなく不等式を用いて表現する方式に改良し、また型定義を Type Descriptor を用いてより一般的に改良することで、syntax の拡張と証明の簡略化を実現した。

14

7.2

今後の課題

今後の課題として、1 つ目はより syntax を拡張すること（例えば、 多相の Let 文など）である。
本論文では generic programming の考え方を使って任意の型を扱えるようにしたが、多相の let 文を入れようと思うと（オブジェクト言語レベルの）型変数（型パラメタ）が必要になる。しかし、今回、採用した generic programming は型パラメタを扱えない。これを扱うには PolyP [2] や Indexed
Functors [4] など型パラメタを扱えるものを使う必要がある。
2 つ目は、完全性の証明を加えることである。例えば現時点ではすべて nothing を返す infer 関数を実装することもできてしまう。つまり、型推論が失敗した時に nothing を返すのではなく、入力された構文に対応する型付けされた構文が存在しないという証明、式にすると¬(∃ w : WellTypedTerm (erase w ≡ s))を返す infer を実装することが必要になる。
謝辞 今回、コメントを下さった査読者の方々に感謝いたします。本研究は、JSPS 科研費 25280020の助成を受けたものです。

参考文献[1] Damas, L. and R. Milner “Principal type-schemes for functional programs,” Proceedings of the 9th
Annual ACM Symposium on Principles of Programming Languages, pp. 207–212 (1982).
[2] Jansson, P., and J. Jeuring “PolyP—a polytypic programming language extension," Proceedings of the
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 470–482 (1997).
[3] 門脇 香子, 浅井 健一「Agda による型推論器の定式化」第１７回プログラミングおよびプログラミング
言語ワークショップ論文集.(2015)[4] Löh, A. and J. P. Magalhães “Generic programming with indexed functors,” Proceedings of the ACM
SIGPLAN Workshop on Generic Programming (WGP’11), pp. 1–12 (2011).
[5] McBride, C. “First-order unification by structural recursion,” Journal of Functional Programming,Vol. 13, No. 6, pp. 1061–1075, Cambridge University Press (2003).
[6] Noort, T. van, A. R. Yakushev, S. Holdermans, J. Jeuring, and B. Heeren “A lightweight approach todatatype-generic rewriting,” Proceedings of the ACM SIGPLAN Workshop on Generic Programming(WGP’08), pp. 13–24 (2008).
[7] Norell, U. “Dependently typed programming in Agda,” In P. Koopman, R. Plasmeijer, and D. Swierstra, editors, Advanced Functional Programming (LNCS 5832), pp. 230–266 (2009).
[8] Norell, U. “Interactive Programming with Dependent Types,” Proceedings of the 18th ACM SIGPLAN
International Conference on Functional Programming (ICFP’13), invited talk, pp. 1–2 ( 2013).
[9] Nordström, B., K. Petersson, and J. M. Smith Programming in Martin-Löf ’s Type Theory, Oxford
University Press (1990).
[10] 住井 英二郎「MinCaml コンパイラ」コンピュータソフトウェア Vol. 25, No. 2, pp. 28–38 (2008).

15