koba/class/soft-kiso/ 1 λ if λx.λy.y false 0 λ typed λ-calculus λ λ 1.1 λ λ, syntax τ (types) ::= b τ 1 τ 2 τ 1

「ソフトウェア基礎科学」補助資料

∗

http://www.kb.ecei.tohoku.ac.jp/˜koba/class/soft-kiso/

小林 直樹

1

型システムの初歩

型なし

λ

計算では，いろいろなデータ（ブール値，整数，組など）や制御（if文，再帰）がλ項 として表現できるが，一方で，その自由度ゆえに，プログラミング言語としてみた場合には不適切 な面も多い．例えば，一つのλ項がいろいろな意味に解釈できてしまう（例えば

λx.λy.y

はブール 値の

false

としても解釈できるし，整数の

0

としても解釈できる）．そこで，型つき

λ

計算（typed

λ-calculus

）では各項にその項がどのような値かを表す「型」を与え，各項（データ）が意図した型 で扱われるように「型システム」によって許される項の集合を制限する．以下では，まず型付き

λ

計算の最も単純なものである，単純型付き

λ

計算について解説する．

1.1

単純型つき

λ

計算

1.1.1

構文 型と

λ

→,×項の

syntax

を次のように定義する．

τ (types)

::= b

| τ

₁

→ τ

₂

| τ

₁

× τ

₂

M (terms)

::= c

τ

| x | M

₁

M

₂

| λx : τ.M | (M

₁

, M

₂

)

| fst(M) | snd(M)

メタ変数

b

は、基底型とよばれる型（整数型

int

、ブール型

bool

など）の集合を動くものとする．

型

τ

₁

× τ

₂は，型

τ

₁の値と型

τ

₂の値とのペアの型を表す．例えば，

(1, true)

は，型

int

× bool

を持 つ． 項の構成子には，型なし

λ

計算に比べて，定数項

c

τ など，いくつか追加してある1．メタ変数

c

τ は，

τ

型の定数を表す．ただし，ここでは定数の型

τ

は，

b

，

b

₁

→ b

₂

, b

₁

×b

₂

→ b

のいずれかのみ であるとし，型

b

₁

→ b

₂の定数

c

b1→b2_には，型

_b

_{1の定数の集合から型}

_b

_{2の定数の集合への（全）} 関数

[[c

b1→b2

_]]

_{が存在するものとする．同様に，型}

_b

₁

× b

₂

→ b

_の定数

_c

b1×b2→b_には型

_b

_{1の定数と} 型

b

₂の定数のペアの集合から型

b

の定数の集合への関数

[[c

b1×b2→b

_]]

_{が存在するものとする．（型}

_b

の定数

c

bには，構文と意味を同一視して，

c

b自身を集合

b

の要素とみなすことにする） ∗_{講義内容とは必ずしも一致しないので，講義をきちんと聞くこと} 1_{これらは必須ではないが，型なしλ計算と異なり，整数やブール値などをλ項として表現してしまうと，違う種類の} データに同じ型がつけられてしまうので，それらを定数として扱う．例えばブール値のfalseと自然数の0は型なしλ計 算では同じλx.λy.xとなってしまう．

c

τ において，型

τ

が明らかな場合には，省略して単に

c

と書く．例えば整数

1

int は単に

1

と書く． λ抽象には，

λx : τ.M

のように，変数

x

に渡されるべき値の「型」を注釈として書くことにす る（これは，

C

言語や

Java

言語などの変数宣言に対応する）．後で述べるように，実は単純型付 きλ計算の場合にはこれらの型は自動的に推論可能であるので，プログラマは省略することができ る．（実際，

ML

という関数型言語では，変数の型宣言をしなくてもよい） 項

(M

₁

, M

₂

)

は，

M

₁（の値）と

M

₂（の値）のペアを表す．

fst (M )

はペア

M

の第一要素を，

snd (M )

はペア

M

の第二要素を取出す．

1.1.2

操作的意味 ここでは，

call-by-value

戦略にしたがった操作的意味を下に与える．代りに

call-by-name

戦略 を用いても，後の型システムの議論にはほとんど影響はない．

V (value) ::= c

τ

| λx.M | (V

₁

, V

₂

)

(λx.M )V

−→

_cbv

[V /x]M

(R-Beta)

c

b1→b

_c

b1 1

−→

cbv

[[c

b1→b

]] (c

b11

)

(R-Const1)

c

b1×b2→b

_(c

b1 1

, c

b22

)

−→

cbv

[[c

b1×b2→b

]] (c

b11

, c

b22

)

(R-Const2)

M

−→

_cbv

M



M N

−→

_cbv

M



N

(R-App1)

N

−→

_cbv

N



V N

−→

_cbv

V N



(R-App2)

M

₁

−→

_cbv

M

₁

(M

₁

, M

₂

)

−→

_cbv

(M

₁

, M

₂

)

(R-Pair1)

M

₂

−→

_cbv

M

₂

(V, M

₂

)

−→

_cbv

(V, M

₂

)

(R-Pari2)

M

−→

_cbv

M



fst (M )

−→

_cbv

fst (M



)

(R-Fst1)

fst (V

₁

, V

₂

)

−→

_cbv

V

₁

(R-Fst2)

M

−→

_cbv

M



snd (M )

−→

_cbv

snd (M



)

(R-Snd1)

snd (V

₁

, V

₂

)

−→

_cbv

V

₂

(R-Snd2)

1.1.3

型システム

λ

→,×においては、上で定義した

syntax

によって構成されるすべての

term

に興味があるわけで はない．すなわち、対象とするのは、上の

syntax

によって構成され、かつ「型に関する整合性があ る」項のみである．例えば、

(λx : int .x)true

という項は、引数として整数を要求している関数に ブール値を適用しようとしているので型に関して整合性がとれていない 「型に関する整合性がある」ということを

formal

に表すために、３項関係

“Γ

 M : τ”

を考 える．「型環境」

Γ

は、変数の有限集合から型への写像である．

“Γ

 M : τ”

は、「型環境

Γ

の もとで、

M

は型

τ

をもつ」と読む．その意図は，「各変数に型環境

Γ

に従った型の値が束縛され ているもとで

M

を評価すると，（存在するならば）評価結果は型

τ

の値である」という意味であ る．この関係は以下のような（型つけ規則と呼ばれる）規則によって

inductive

に定義される．規 則

T-Var

や

T-Abs

の

Γ, x : τ

は，型環境

Γ

の

x

に対応する値を

τ

に置き換えて（または追加して） 得られる型環境を表す．

Γ

 c

τ

: τ

(T-Const)

Γ, x : τ

 x : τ

(T-Var)

Γ

 M

₁

: τ

₁

→ τ

₂

Γ

 M

₂

: τ

₁

Γ

 M

₁

M

₂

: τ

₂

(T-App)

Γ, x : τ

₁

 M : τ

₂

Γ

 λx : τ

₁

.M : τ

₁

→ τ

₂

(T-Abs)

Γ

 M

₁

: τ

₁

Γ

 M

₂

: τ

₂

Γ

 (M

₁

, M

₂

) : τ

₁

× τ

₂

(T-Pair)

Γ

 M : τ

₁

× τ

₂

Γ

 fst(M) : τ

₁

(T-Fst)

Γ

 M : τ

₁

× τ

₂

Γ

 snd(M) : τ

₂

(T-Snd)

Γ

 M : τ

が上のルールによって導ける時、「

M

は型環境

Γ

のもとで型づけ可能

(well-typed)

で ある」という．

Remark 1.1:

上の導出において，束縛変数のつけかえ（

α

変換）によって得られる項は同一のも のとみなし，束縛変数の名前は必要に応じて名前のつけかえを行うものとする．例えばの型

λx:int .λx:

bool .x

は以下のように導出する．

x : int , y : bool

 y : bool

x : int

 λy : bool.y(= λx : bool.x) : bool → bool

∅  λx : int.λx : bool.x : int → bool → bool

Exercise

次の各

term

について、

Γ

 M : τ

を満たす組

Γ, τ

は存在するか？もし存在するなら ばその組を一つあげよ．

1. λx : int .yx

2. xx

3. λz : (int

→ int → int).zxy

4. (xy)(xz)

5. (yx)(zx)

任意の型環境

Γ

と項

M

について、

Γ

 M : τ

を満たす

τ

は

unique

であることが次の定理から わかる（これは一般の型システムでは必ずしも成り立たない）．

Theorem 1.2: Γ

 M : τ

₁かつ

Γ

 M : τ

₂ならば

τ

₁

= τ

₂

.

Exercise

上の定理を証明せよ．

1.1.4

型システムの健全性

(Type Soundness)

λ

項をプログラムとみた場合，本来関数であるべきところに整数がきたり（例：

1(2)），定数関

数に要求されているのとは違う引数が与えられたり（例：

+

int×int→int

(true, 1)），

fst

や

snd

にペ アでないものが与えられたり（例：

fst (1)

）しては困る．通常の型システムはそのような「実行時 型エラー」が起こらないように設計されている2．型システムで型づけされた閉じた項（自由変数を 含まない項，プログラム）は実行時型エラーを起こさないことが保証されているとき，その型シス テムは（操作的意味に対して）健全であると言う．

1.1.3節で定義した型システムも健全である．そのことを以下で確認しよう．まず，「実行時型エ

ラー」は，

1.1.2節の操作的意味では，「値になっていないのに，適用すべき規則がない状態」とし

てとらえることができる．実際，

fst (1)

のような項については，適用できる規則がないことに注意 してほしい． 型システムの健全性は，以下の２つの性質によって保証される．一番目の性質（定理

1.3）は，プ

ログラム

M

が型づけ可能であり，値でないならば，まだ簡約が行えることを表す．二番目の性質 （定理

1.4, subject reduction

とも呼ばれる）は，型づけが簡約によって保存されることを表す．こ れらの性質から，プログラム

M

が型づけ可能であれば，

M

が値に簡約されるまでは簡約をつづけ て行うことができる（系

1.10），つまり実行時型エラーは決して起こらないことが言える．

Theorem 1.3 [Progress]:

もし

∅  M : τ

かつ

M

が値でないならば，ある

M

が存在して

M

−→

_cbv

M

が成り立つ．

Proof:

M

の構造に関する帰納法により示す．

• M = c

τ_のとき．

_M

_{は値であるので明らか．} 2_{C言語のようにそうでないものも存在する}

• M = x

のとき．

∅  M : τ

は成り立たないので明らか．

• M = M

1

M

2のとき．

∅  M : τ

であるとすると，ある

τ

₁が存在して

∅  M

₁

: τ

₁

→ τ

かつ

∅  M

2

: τ

1．

M

₁が値でないならば，帰納法の仮定より，

M

₁

−→

_cbv

M

₁ を満たす

M

₁ が存 在するので，

M



= M

₁

M

₂とおけば，

M

−→

_cbv

M

．

M

₁が値である場合，型づけ規則よ り，

M

₁

= c

τ1→τ _または

_M

₁

_{= λx.M}

 1．

M

2が値であるかどうかにより場合分けを行う．

– M

₂が値でない場合: 帰納法の仮定より，

M

₂

−→

_cbv

M

₂ を満たす

M

₂ が存在するので，

M



= M

₁

M

₂ とお けば

M

−→

_cbv

M

．

– M

₂が値である場合：

M

₁

= λx.M

₁ のときは，

M



= [M

₂

/x]M

₁ とおけば，規則

R-Beta

より

M

−→

_cbv

M

．

M

₁

= c

τ1→τ _{のとき．定数の型に関する仮定から，}

_τ

₁

→ τ = b

₁

× b

₂

→ b

_または

_τ

₁

→

τ = b

₁

→ b

．前者の場合，

∅  M

₂

: b

₁

× b

₂かつ

M

₂が値なので，

M

₂

= (c

b1 1

, c

b22

)．

よって，

M



= [[c

b1×b2→b

_{]] (c}

b1 1

, c

b22

)

とおけば，規則

R-Const2

より，

M

−→

_cbv

M

． 後者の場合，

∅  M

₂

: b

₁かつ

M

₂が値なので，

M

₂

= c

b₁1．よって，

M



= [[c

b1→b

_]]

(c

b₁1

)

とおけば規則

_R-Const1

より，

M

−→

_cbv

M

．

• M = λx : τ.M

1のとき．

M

は値なので明らか．

• M = (M

1

, M

2

)

のとき．

∅  M : τ

かつ

M

が値でない（つまり

M

₁または

M

₂のいずれかは 値でない）と仮定する．型づけ規則より，

τ = τ

₁

×τ

₂，

∅  M

₁

: τ

₁，かつ

∅  M

₂

: τ

₂．

M

₁ が値でないとき，帰納法の仮定より，

M

₁

−→

_cbv

M

₁ を満たす

M

₁ が存在し，

M



= (M

₁

, M

₂

)

とおけば

M

−→

_cbv

M

が成り立つ．

M

₁が値であり，

M

₂が値でないときは帰納法の仮定 より，

M

₂

−→

_cbv

M

₂ を満たす

M

₂ が存在し，

M



= (M

₁

, M

₂

)

とおけば規則

_R-Pair2

より

M

−→

_cbv

M

が成り立つ．

• M = fst(M

1

)

のとき．型づけ規則より，

∅  M : τ

ならば，

∅  M

₁

: τ

× τ

₂．

M

₁が値 でなければ，帰納法の仮定より

M

₁

−→

_cbv

M

₁ を満たす

M

₁ が存在し，

M



= fst (M

₁

)

とお けば，

M

−→

_cbv

M

が成り立つ．

M

₁が値ならば，型づけ規則より，

M

₁

= (V

₁

, V

₂

)．よっ

て，

M



= V

₁とおけば，規則

_R-Fst2

より

M

−→

_cbv

M

．

• M = snd(M

1

)

のとき．

M = fst (M

₁

)

の場合と同様．

Theorem 1.4 [

型保存定理

(Type Preservation)]:

もし

Γ

 M : τ

かつ

M

−→

_cbv

M

なら ば，

Γ

 M



: τ

が成り立つ．

上の型保存定理の証明の前に，補題を用意する．下で

Γ

⊆ Γ

は型環境

Γ, Γ

を集合としてみたと

きの包含関係，つまり

∀x.∀τ.(Γ(x) = τ ⇒ Γ



(x) = τ )

を表す．

Lemma 1.5 [weakening]: Γ

 M : τ

かつ

Γ

⊆ Γ

ならば，

Γ



 M : τ

．

Exercise 1.6:

上の補題を証明せよ．

Lemma 1.7 [substitution lemma]: Γ

 M

₁

: τ

₁かつ

Γ, x : τ

₁

 M

₂

: τ

₂ならば，

Γ



[M

₁

/x]M

₂

: τ

₂が成り立つ．

Proof:

M

₂の構造に関する帰納法．代表的な場合についてのみ示す．

• M

2

= x

のとき．

[M

₁

/x]M

₂

= M

₁より明らか．

• M

2

= y(

= x)

のとき．

[M

₁

/x]M

₂

= y．

Γ, x : τ

₁

 M

₂

: τ

₂ならば

Γ(y) = τ

₂なので，

Γ

 [M

₁

/x]M

₂

: τ

₂．

• M

2

= λy : τ

21

.M

2 のとき．

Γ, x : τ

1

 M

2

: τ

2より，

Γ, x : τ

₁

, y : τ

₂₁

 M

₂

: τ

₂₂か つ

τ

₂

= τ

₂₁

→ τ

₂₂．

Lemma 1.5より，

Γ, y : τ

₂₁

 M

₁

: τ

₁なので，帰納法の仮定より，

Γ, y : τ

₂₁

 [M

₁

/x]M

₂

: τ

₂₂が成り立つ．

T-Abs

より，

Γ

 λy : τ

₂₁

.[M

₁

/x]M

₂

: τ

₂₁

→ τ

₂₂， つまり

Γ

 [M

₁

/x]M

₂

: τ

₂．

Exercise 1.8:

上の証明で，他の場合について示して証明を完成させよ．

Proof of Theorem 1.4:

M

−→

_cbv

M

の導出に関する帰納法．最後の規則により場合わけを 行う．以下は代表的な場合に付いてのみ示す．

• R-Beta

の場合．

M = (λx.M

₁

)M

₂かつ

M



= [M

₂

/x]M

₁．

Γ

 M : τ

より，

Γ, x : τ

₁



M

₁

: τ

かつ

Γ

 M

₂

: τ

₁．

Lemma 1.7より，

Γ

 M



: τ

が成り立つ．

• R-Const1

の場合．

M = c

b1→b

_c

b1 1 かつ

M



= [[c

b1→b

]] (c

1b1

) = c

b2かつ

τ = b

．

T-Const

よ り，

Γ

 M



: τ

．

• R-App1

の場合．

M = M

₁

M

₂かつ

M



= M

₁

M

₂かつ

M

₁

−→

_cbv

M

₁．

Γ

 M : τ

よ り，

Γ

 M

₁

: τ

₁

→ τ

かつ

Γ

 M

₂

: τ

₁．帰納法の仮定より，

Γ

 M

₁

: τ

₁

→ τ

．よっ て，

T-App

より，

Γ

 M



: τ

．

Exercise 1.9:

上の証明で，他の場合について示して証明を完成させよ．

Corollary 1.10 [Type Soundness]:

もし

∅  M : τ

かつ

M

−→

∗_cbv

M



−→

_cbvならば，

M



は値である．

1.1.5

Strong Normalization

λ

→,×においては、型づけ可能な項は、どんな順序で

β-reduction

（call-by-value 戦略

−→

_cbvに

限る必要はない）を施しても必ず有限ステップで

normal form

に簡約できることが保証されてい

る．

Theorem 1.11 [strong normalization]: Γ

 M : τ

ならば、無限の

β

簡約列

M

−→ M

β ₁

−→

β

M

₂

−→ · · ·

β は存在しない．

証明は

[2]

を参照せよ．

注 上の

strong normalization

に関する定理は、非常によい性質である反面、

λ

→,×の表現力が弱

いことを意味する（total functionしか表現できない）．実際のプログラミング言語として用いると

きには，

strong normalization

の性質はあきらめ，

fixed point operator fix

(τ1→τ2)→(τ1→τ2)_を定

数として導入して再帰を表現できるようにする．

1.1.6

型推論と

Principal Typing

λ

→,×をプログラミング言語としてとらえた場合、

λx : τ.M

のように、各関数の引数について型

を宣言するのは面倒である．そこで、型宣言を省略した以下のような言語を考え、

e (terms)

::= c

τ

| x | e

₁

e

₂

| λx.e | (e

₁

, e

₂

)

| fst(e) | snd(e)

e

から、

Γ

 M : τ

を満たす

Γ, M, τ

（

M

は

e

に型宣言を付加して作られる項）を自動的にみつ けることは可能だろうか？

e

の形によっては、そのような

Γ, M, τ

の組は無限に存在する．例えば

e = x

とすると、任意の

τ

について

x : τ

 M : τ

が成り立つ．同様に、

e = λx.x

とすると任 意の

τ

について

∅  λx : τ.x : τ → τ

が成り立つ．このように無限の数の組を一つ一つ列挙する のは

reasonable

ではない．ところが幸い、型の

syntax

を若干変更すれば、

Γ

 M : τ

をみたす

Γ, M, τ

の中で、「最も一般的な」ものが一つ存在することがわかる． 型の

syntax

に、次のように型変数を導入する．

τ (types)

::= α (type variables)

| b | τ

₁

→ τ

₂

| τ

₁

× τ

₂

λ

→,×項

M

からすべての型宣言をとりさってできる（型なし）項を

Erase(M )

と書くことにする．

与えられた

e

に対して、上で述べた「最も一般的な」

Γ, M, τ

とは次のように定義できる．

Definition 1.12 [principal typing]: (Γ, M, τ )

は以下の条件を満たす時、（型なし）項

e

の

prin-cipal typing

であるという．

1. Erase(M ) = e

2. Γ

 M : τ

3. Γ



 M



: τ



, Erase(M



) = e

を満たす任意の

Γ



, M



, τ

について、次の条件を満たす型変数

(a) θΓ

⊆ Γ



(b) θM = M



(c) θτ = τ

 すなわち、

Γ, M, τ

は、（１）正しい型つけであり、（２）すべての正しい型つけは型変数への代 入および余分な型環境の付加によってえられ, かつ（３）逆に型変数への代入および余分な型環境 の付加によってえられる組はすべて正しい型つけである（これは上の条件には入っていないが型つ け規則から直ちにいえる）とき、

principal typing

であると呼ばれる．

λ

→,×については

principal typing

は単一化（unification）アルゴリズム

mgu

3を用いて以下のよ うに容易に求めることができる．

P T (c

τ

)

= (

∅, c

τ

, τ )

P T (x)

= (x : α, x, α) where α is fresh

P T (e

₁

e

₂

)

= let

(Γ

₁

, M

₁

, τ

₁

) = P T (e

₁

)

(Γ

₂

, M

₂

, τ

₂

) = P T (e

₂

)

θ = mgu(

{(τ

₁

, τ

₂

→ α)} ∪ {(Γ

₁

(x), Γ

₂

(x))

| x ∈ dom(Γ

₁

)

∩ dom(Γ

₂

)

})

where α is fresh

in ((θΓ

₁

)

∪ (θΓ

₂

), θ(M

₁

M

₂

), θα)

P T (λx.e)

= let

(Γ, M, τ ) = P T (e)

in if x

∈ dom(Γ)

then (Γ

\x, λx : Γ(x).M, Γ(x) → τ)

else (Γ, λx : α.M, α

→ τ)

where α is fresh

P T ((e

₁

, e

₂

))

= let

(Γ

₁

, M

₁

, τ

₁

) = P T (e

₁

)

(Γ

₂

, M

₂

, τ

₂

) = P T (e

₂

)

θ =

{(Γ

₁

(x), Γ

₂

(x))

| x ∈ dom(Γ

₁

)

∩ dom(Γ

₂

)

})

in ((θΓ

₁

)

∪ (θΓ

₂

), θ((M

₁

, M

₂

)), θ(τ

₁

× τ

₂

))

P T (fst (e))

= let

(Γ, M, τ ) = P T (e)

θ = mgu(

{(τ, α × β)}

where α,β are fresh

in (θΓ, θ(fst (M )), θα)

P T (snd (e))

= let

(Γ, M, τ ) = P T (e)

θ = mgu(

{(τ, α × β)}

where α,β are fresh

in (θΓ, θ(snd (M )), θβ)

3_{型のペアの有限集合{(τ}

11, τ12), . . . , (τn1, τn2)}を受け取り，等式τ11 = τ12, . . . , τn1 = τn2の最汎単一化子(most

Exercise

上のアルゴリズムに従って、

principal typing

を求めるプログラムを作成せよ．（ML または

Prolog

を使うと楽である）

1.2

Polymorphism

λ

→,×においては、各変数には特定の型の値しか束縛することができない．これは、プログラムの 再利用性の点において非常に都合がわるい．例えば、恒等関数はどんな型についても

λx.x

と書け るはずなのに、それぞれの型ごとに

λx : τ.x

を用意しなければならない．このような欠点を克服 するため、これまでに多くの型システムの改良が提案・研究されてきている（一般に、上のように 各部分式が単一の型の値としてしか用いることができないような型システムを単相

(monomorphic)

型システム、以下で述べる改良のように複数の型の値として用いることができるようなものを多相

(polymorphic)

型システムと呼ぶ）．ここではそれらのうちの代表的なものとして

ML

で用いられ ている

parametric polymorphism

について紹介する．

1.2.1

λ

→,∀ 上で例に考えた恒等関数

λx : τ.x

がどのようにしたら再利用できるかを考えよう．（型を明示的 に指定しないで単に

λx.x

と書き、型推論によって文脈に応じて

λx : τ.x

と型を再構成すればよい と思うかもしれないがこれはうまくいかない．

(λx.xx)(λx.x)

が型づけできないことからわかるよ うに、

λ

→,×の枠組の中で考えているかぎり、一つの式を複数の型の値として用いることはできな い．） ここで、各型用の恒等関数は

λx : τ.x

中の

τ

の部分だけが異なることに着目しよう．そこで、型 変数に関する

λ

抽象を許すことにすれば、

λx : τ.x

は、

(Λα : U

₁

.λx : α.x)τ

のように表すことがで きる．したがって、

Id = Λα : U

₁

.λx : α.x

とおけば、各

Id

_τ

= λx : τ.x

は，

Id

の型

τ

への適用

Id[τ ]

によって得られ、

Id

の部分が共有でき ることになる．同様にして、２つの関数を合成する関数

compose

は、

compose = Λα : U

₁

.Λβ : U

₁

.Λγ : U

₁

.λf : β

→ γ.λg : α → β.λx : α.f(g(x))

と書ける．上で

U

₁と書いたのは「型の型」のようなものであり、

τ : U

₁によって「

τ

は型である」 ことを表す．意味的には、

U

₁は次によって定義される型の集合と考えればよい．

τ ::= α

| b | τ

₁

→ τ

₂

| τ

₁

× τ

₂

Id

や

compose

の「型」はどのように表せばよいだろうか？それらは

U

₁の要素によって表すことは できず、新たに型に関する構成子を導入する必要がある．

Id

はあらゆる型

τ

について

τ

→ τ

とい う型の値を返すので、

∀α : U

₁

.(α

→ α)

のように書く． 同様にして、

compose

の型は

∀α : U

1

.

∀β : U

₁

.

∀γ : U

₁

.((β

→ γ) → (α → β) → α → γ)

と表すことができる．

U

₁に

∀α

₁

: U

₁

.

· · · ∀α

_n

: U

₁

.τ

の形の型を追加した型の集合を

U

₂と書くこと にし、

U

₂の型を表すメタ変数として

σ

を用いる．

Remark 1.13: U

₂は、以下によって定義される型の集合

U

（後述の

impredicative polymorphism

を参照．）とは異なることに注意せよ．

τ ::= α

| b | τ

₁

→ τ

₂

| τ

₁

× τ

₂

| ∀α : U.τ

例えば，

(

∀α.α) → (∀α.α)

は

U

₂の型ではない． 以上にしたがって項の

syntax,

型つけ規則を定義すると以下のようになる．（:U₁は省略する．ま た，ペアの構成子は本質的でないので省略する）

Definition 1.14 [λ

→,∀

-term]:

M ::= c

σ

| x | M

₁

M

₂

| λx : τ.M | Λα.M | M[τ]

Γ

 c

σ

: σ

(TPoly-Const)

Γ, x : σ

 x : σ

(TPoly-Var)

Γ

 M

₁

: τ

₁

→ τ

₂

Γ

 M

₂

: τ

₁

Γ

 M

₁

M

₂

: τ

₂

(TPoly-App)

Γ, x : τ

₁

 M : τ

₂

Γ

 λx : τ

₁

.M : τ

₁

→ τ

₂

(TPoly-Abs)

Γ

 M : σ

α not free in Γ

Γ

 Λα.M : ∀α.σ

(TPoly-∀-Intro)

Γ

 M : ∀α.σ

Γ

 M[τ] : [τ/α]σ

(TPoly-∀-Elim)

1.2.2

λ

→,∀,let さて、

λ

→,∀自身は、多相関数を用いる上で不十分である．例えば、

untyped λ-calculus

の

(λx.xx)(λx.x)

に相当する

term

は、一見

(λx :

∀α.(α → α).(x[τ → τ])(x[τ]))(Λα.λx : α.x))

のように表せばいいように見えるが、

λx :

∀α.(α → α).(x[τ → τ])(x[τ])

の部分は、

∀α.(α → α)

の値をとって

τ

→ τ

の型の値を返す関数となり、それを表す型が存在しない（(

∀α.(α → α)) →

(τ

→ τ)

はもはや

U

₁の型でも

U

₂の型でもないことに注意）．これに対する解決策としては以下の ２通りが考えられる．

•

型の集合を拡張し、

σ ::= α

| b | σ

₁

→ σ

₂

| ∀α.σ

のように定義する．

∀α.σ

のように型全体に関して言及した型もまた型として扱われるので、 型の意味はもはや単純な集合論ではとらえることができない．このような多相型システムは

impredicative polymorphsim

とよばれ、

Girard

と

Reynolds

によって独自に提案され、そ の後盛んに研究されている．

•

新しい項の

construct

を導入し、部分的に多相性を導入する．これがプログラミング言語

ML[1]

で用いられている方法である． ここでは後者の方法を解説する．まず項の

syntax

を次のように

let

式を導入して拡張する．

M ::= x

| M

₁

M

₂

| λx : τ.M | Λα.M | M[τ] | let x : σ = M

₁

in M

₂

end

そして、次の

let

式に対する型つけ規則を追加する．

Γ

 M

₁

: σ

Γ, x : σ

 M

₂

: τ

Γ

 let x : σ = M

₁

in M

₂

end : τ

(TPoly-Let)

ここで、

x

が

M

₂の中で

U

₂の型

σ

の値として用いることができることに注意．したがって、

let

で

bind

された変数はその

body

中で

polymorphic

に用いることができる．これによって上記の例は、

let x :

∀α.(α → α) = Λα.λx : α.x in (x[τ → τ])(x[τ]) end

と記述できる．一方、

λ

抽象によって

bind

された変数は、あいかわらず

monomorphic

にしか用い ることができない．

1.2.3

λ

→,∀,letに関する型推論

λ

→の時と同じく、型推論の問題は、「型に関する記述を取り除いた項

e

から、

Γ

 M : σ, Erase(M) =

e

を満たす３つ組

(Γ, M, σ)

を求める」こととして定義できる．「型なし項」の

syntax

および型を 取り除く変換

Erase

は次のように定義できる．

e ::= x

| e

₁

e

₂

| λx.e | let x = e

₁

in e

₂

end

Erase(x)

= x

Erase(M

₁

M

₂

)

= Erase(M

₁

)Erase(M

₂

)

Erase(λx : τ.M )

= λx.Erase(M )

Erase(Λα.M )

= Erase(M )

Erase(M [τ ])

= Erase(M )

Erase(let x : σ = M

₁

in M

₂

end)

= let x = Erase(M

₁

) in Erase(M

₂

) end

型なし項の

syntax

は

ML

の核部分の言語であり、したがって、

ML

における型推論の問題は、ま さに

λ

→,∀,letに対する型推論の問題としてとらえることができる． さて、

λ

→,∀,letに対する型推論は

λ

→,×に対するそれほど単純ではない．それをみるために、型 つけ規則の中の項

M

を

Erase(M )

で置き換えた規則を考えよう．

Γ

 e : σ

α not free in Γ

Γ

 e : ∀α.σ

(T-ML-∀-Intro)

Γ

 e : ∀α.σ

Γ

 e : [τ/α]σ

(T-ML-∀-Elim)

· · ·

上に示した一部の規則からわかるように、

λ

→,×の場合と異なり、もはや一つの型なし項の形に対 して適用できる型つけ規則が複数存在する．したがって、もとの項

M

に対する型つけがどの規則か ら導かれたのかをしることができない．ところが、以下に示すように、

T-ML-∀-Intro, T-ML-∀-Elim

が 限られた場所でしか適用できないことを利用して、上の規則の集合と等価であり、かつそれぞれの 項の形に対して適用できる規則が一つしかないような規則に変形できる． まず、

T-ML-∀-Elim

の出現場所を考えてみよう．すると、仮定部分が

U

₂の型なので、

T-ML-∀-Elim

が 適用される前のルールは、結論部に

U

₂の型をもつものでなければならない．したがって、

TPoly-Var

あるいは

T-ML-∀-Elim, T-ML-∀-Intro

のいずれかである．ところが、直前が

T-ML-∀-Intro

の 場合には導出木は

· · ·

Γ

 e : σ

Γ

 e : ∀α.σ

Γ

 e : [τ/α]σ

の形になっているので、部分導出木

· · ·

Γ

 e : σ

中の

α

を

τ

で置き換えてできる導出木

· · ·

Γ

 e : [τ/α]σ

で置き換えることができる．したがって、「

T-ML-∀-Elim

は、

TPoly-Var

のあとに連続して適 用されるのみである」と制限することができる．同様にして，「

T-ML-∀-Intro

は，

TPoly-Let

の 直前に左側の条件部を導出するのに用いられるのみ」と制限することができる．以上から、

λ

→,∀,let の（型なし項に対する）型つけ規則は、以下のものと（Γ

 e : τ

という形の

type judgement

につ いては）等価であることがわかる．

Γ, x :

∀α.τ



 x[τ] : [τ/α]τ



(T-ML-Var)

Γ

 M

₁

: τ

₁

→ τ

₂

Γ

 M

₂

: τ

₁

Γ

 M

₁

M

₂

: τ

₂

(T-ML-App)

Γ, x : τ

₁

 M : τ

₂

Γ

 λx : τ

₁

.M : τ

₁

→ τ

₂

(T-ML-Abs)

Γ

 M

₁

: τ

₁

Γ, x :

∀α.τ

₁

 M

₂

: τ

₂

{α}

は

τ

₁に出現するが

Γ

には出現しない型変数の集合

実は

λ

→,∀,letそのものに対しては

λ

→,×で考えたような

principal typing

は存在しない．ところ が、型推論の問題を適当に限定することで、

principal typing

が存在するようにできる．すなわち、

e

から、

(Γ, M, σ)

を求める上で、

Γ, σ

を「

U

₁の型しか含まない」と限定すると、任意の

e

に対し て最も一般的な

(Γ, M, σ)

が常に存在する．閉じた項については、型環境が空でよいので、そのよ うな限定した仮定のもとでの最も一般的な

M, τ

は、もともとの

λ

→,∀,letにおけるそれに一致する． 限定した仮定のもとでの

principal typing

およびそれを求めるアルゴリズムは以下のようになる． アルゴリズムの引数

A

には，途中で求まった，

let

式で束縛された変数の

U

₂の型が格納される．

e

の

principal typing

を求めるには，

P T (e,

∅)

を計算すればよい．

P T (c

∀α.τ

, A) = (

∅, c

∀α.τ

[

β], [

β/

α]τ )

where 

β are fresh.

P T (x, A)

= if A(x) =

∀α.τ then (x : ∀α.τ, x[β], [β/α]τ)

where 

β are fresh.

else(

{x : α}, x, α) where α is fresh

P T (e

₁

e

₂

, A)

= let

(Γ

₁

, M

₁

, τ

₁

) = P T (e

₁

, A)

(Γ

₂

, M

₂

, τ

₂

) = P T (e

₂

, A)

θ = mgu(

{(τ

₁

, τ

₂

→ α)}) ∪ {(Γ

₁

(x), Γ

₂

(x))

| x ∈ dom(Γ

₁

)

∩ dom(Γ

₂

)

})

where α is fresh

in ((θΓ

₁

)

∪ (θΓ

₂

), θ(M

₁

M

₂

), θα)

P T (λx.e, A)

= let

(Γ, M, τ ) = P T (e, A)

in if x

∈ dom(Γ)

then (Γ

\x, λx : Γ(x).M, Γ(x) → τ)

else (Γ, λx : α.M, α

→ τ)

where α is fresh

P T (let x = e

₁

in e

₂

end, A)

= let

(Γ

₁

, M

₁

, τ

₁

) = P T (e

₁

, A)

(Γ

₂

, M

₂

, τ

₂

) = P T (e

₂

, A

∪ {x : ∀α.τ

₁

})

where 

α appears in τ

₁

but not in Γ

₁

θ = mgu(

{(Γ

₁

(y), Γ

₂

(y))

| x ∈ dom(Γ

₁

)

∩ dom(Γ

₂

)

})

in ((θΓ

₁

)

∪ (θ(Γ

₂

\x)), θ(let x : ∀α.τ

₁

= Λ

αM

₁

in M

₂

end), θτ

₂

)

参考文献

[1] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of

Stan-dard ML (Revised). The MIT Press, 1997.