前章では let 多相を学んだ。本章では、System F という強力な計算体系の下で、より一般的な多相性について考える。

id 関数を定義するとき、下のように各型に対しての id 関数を逐一定義するのは面倒。

• idNat = λx:Nat. x
• idBool = λx:Bool. x

コード中の異なる箇所で似た機能が実現されているとき、差分を抽象化して一つにまとめることは、一般的に常に有益である。

今の場合の差分は「型」にあるため、必要なのは以下の２点となる。

• 項から型を抽象化する機能
• 抽象化した項を具体的な型注釈で具体化する機能

一つのコードを複数の型で扱えるようにした型システムを、多相的な型システムと呼ぶ。
多相性にはいくつかの種類がある。

• パラメータ多相:
  型変数を用いて、一つのコードを総称的に型付けし、必要に応じて具体化できる。その具体化は全て同じ振る舞いをする。
• 非可述的多相（一級多相）:
  もっとも強力なパラメータ多相。本章で扱うもの。実用上では let 多相と呼ばれる。
• let 多相:
  多相性を let 束縛だけに限定し、多相的な値を引数として受け取ることを許さない。その代わりに、便利で自然な形の型再構築が可能。
• アドホック多相:
  異なる型の引数に対してそれぞれ異なる実装を持つ場合に必要となる多相性。「オーバーロード」では、関数適用ごとにその引数の型に基づいて、コンパイラや実行時システムが適切な実装を選択する。
• 内包的多相:
  アドホック多相をより強力にしたもの。実行時の型に関する制限された計算が可能になる。「アンボックス化」など。
• 部分型多相:
  15 章で紹介したもの。１つの項に複数の型を与えることを可能にする。

以上の多相性を一つの言語に盛り込むことは可能である。Standard ML は、パラメータ多相に加え、組み込みでオペレーターオーバーロードを実現している。

関数型プログラミング分野では、「多相性」というとほぼパラメータ多相を指すが、オブジェクト指向プログラミング分野では部分型多相を意味し、「パラメータ多相」のことはジェネリクスと呼ぶ。

本章で扱う体系は、System F と呼ばれる。
単純型付きラムダ計算 λ-> を拡張したものに当たるために「多相ラムダ計算」と呼ばれたり、Curry-Howard 同型を通じて二階直観論理に対応するために「二階ラムダ計算」と呼ばれることもある。

※二階直観論理とは、証明（項）だけでなく、述語（型）の量化も許す論理体系。

図23-1 に定義を示す。

System F
★ 項の定義

t	::=	x	変数
		λx:T. t	λ抽象
		t t	関数適用
		λX. t	型抽象*
		t [T]	型適用*

★ 値の定義

v	::=	λx: T. t	λ抽象値
		λX. t	型抽象値*

★ 型、文脈の定義は省略

★ 評価規則

t1 -> t1' E-TApp* t1 [T2] -> t1' [T2]

E-TAppTAbs* (λX. t12) [T2] -> [X |-> T2] t12

★ 型付け規則

Γ, X ├ t2 : T2 T-TAbs* Γ├ λX. t2 : ∀X. T2

Γ├ t1 : ∀X. T12 T-TApp* Γ├ t1 [T2] : [X |-> T2] T12

System F の体系の上で、いくつかの事例を提示する。

肩慣らし

id = λX. λx:X. x
=> id : ∀X. X -> X

id [Nat]
=> <fun> : Nat -> Nat

id [Nat] 0
=> 0 : Nat

double = λX. λf:X->X. λa:X. f (f a)
=> double : ∀X. (X -> X) -> X -> X

単純型付きラムダ計算では、多相的な自己適用 λx. x x という型無し項を型付けできなかった。（演習 9.3.2）
System F では x に多相型を与えて、適切に具体化することで、この項の型付けが可能になる。

selfApp = λx:∀X.X->X. x [∀X.X->X] x
=> selfApp : (∀X. X -> X) -> (∀X. X -> X)

自己適用の例として、double を使った四倍関数を作ってみる。

quardruple = λX. double [X->X] (double [X])
=> quardruple : ∀X. (X -> X) -> X -> X

演習 23.4.1 図23-1の型付け規則によって、上記の項の型を確認せよ。

証明）
省略

多相リスト

型構築子 List と以下のプリミティブを言語に持たせることを考えよう。

• nil : ∀X. List X
• cons : ∀X. X -> List X -> List X
• isnil : ∀X. List X -> Bool
• head : ∀X. List X -> X
• tail : ∀X. List X -> List X

このとき、多相的な map 関数は以下のように定義できる。

map	=	λX. λY. λf:X->Y.
		(fix (λm: List X -> List Y.
		λl: List X.
		if isnil [X] l then nil [Y]
		else cons [Y] (f (head [X] l)) (m (tail [X] l))))

演習 23.4.2 map が上記の型を持つか確認せよ。

証明）
省略


演習 23.4.3 多相的なリスト反転関数をかけ。
reverse : ∀X. List X -> List X

証明）

addLast	=	λX. λa:X.
		(fix (λm: List X -> List X.
		λl: List X.
		if isnil [X] l then cons [X] a (nil [X])
		else cons [X] (head [X] l) (m (tail [X] l))))
reverse	=	λX.
		(fix (λm: List X -> List X.
		λl: List X.
		if isnil [X] l then nil [X]
		else addLast [X] (m head [X] l) (m (tail [X] l))))

演習 23.4.4 単純な多相ソート関数をかけ。
sort : ∀X. (X -> X -> Bool) -> List X -> List X

証明）

insert	=	λX. λf:X->X->Bool. λa:X.
		(fix (λm: List X -> List X.
		λl: List X.
		if isnil [X] l then cons [X] a (nil [X])
		else if f a (head [X] l) then cons [X] a l
		else cons [X] (head [X] l) (m (tail [X] l))))
sort	=	λX. λf:X->X->Bool
		(fix (λm: List X -> List X.
		λl: List X.
		if isnil [X] l then nil [X]
		else insert [X] f (head [X] l) (m (tail [X] l))))

Church 表現

型無しラムダ計算では、Church 表現を用いてブール値・自然数を表現することができた。これと同じことを System F でもやってみる。

	|		|	λ->	|	System F	|
ーーーーー	+	ーーー	+	ーーーーーーーーーー	+	ーーーーーーーーーーーーーーーーーーーー	+
ブール値	|	型	|	-	|	CBool = ∀X. X -> X -> X	|
	|	tru	|	λt: λf: t	|	λX. λt:X. λf:X. t	|
	|	fls	|	λt: λf: f	|	λX. λt:X. λf:X. f	|
	|	not	|	-	|	λb:CBool. λX. λt:X. λf.X. b [X] f t	|
	|		|	-	|		|
自然数	|	型	|	-	|	CNat = ∀X. (X -> X) X -> X	|
	|	c0	|	λs. λz. z	|	λX. λs:X->X. λz:X. z	|
	|	c1	|	λs. λz. s z	|	λX. λs:X->X. λz:X. s z	|
	|	c2	|	λs. λz. s (s z)	|	λX. λs:X->X. λz:X. s (s z)	|
	|	c3	|	λs. λz. s (s (s z))	|	λX. λs:X->X. λz:X. s (s (s z))	|
	|	csucc	|	-	|	λn:CNat. λX. λs:X->X. λz:X. s (n [X] s z)	|
	|	cplus1	|	-	|	λm:CNat. λn:CNat. m [CNat] csucc n	|

演習 23.4.5 型 CBool の引数を２つ受け取り、論理積を返す and をかけ。

証明）
and = λb1:CBool. λb2:CBool. λX. λt:X. λf.X. b1 b2 f

演習 23.4.6 Church 数 c0 に適用されたときは tru、さもなくば fls を返す 関数 iszero をかけ。

証明）
iszero = λn:CNat. n [CBool] (λx:CBool. fls) tru


演習 23.4.7 以下が正しく型付けされていて、乗算と冪乗算になっていることを確認せよ。
times = λm:CNat. λn:CNat. λX. λs:X->X. n [X] (m [X] s)
=> times : CNat -> CNat -> CNat

cexp = λm:CNat. λn:CNat. λX. n [X->X] (m [X])
=> cexp : CNat -> CNat -> CNat

証明）
省略



...

定理 23.5.1 [保存] Γ├ t : T かつ t -> t' ならば Γ├ t' : T

定理 23.5.2 [進行] t が閉じた、正しく型付けされた項ならば、t は値か、ある t' が存在して t -> t'

System F は、λ-> と同様に正規化の性質、つまり正しく型付けされたプログラムの評価は停止する。

定理 23.5.3 [正規化] 正しく型付けされた System F の項は正規化可能である。

System F の項から全ての型注釈を取り払い、型無しラムダにする型消去関数 erase を定義できる。

...
erase(λX. t2)	=	erase(t2)
erase(t1 [T2])	=	erase(t1)

型無しラムダ計算の項 m から、erase(t) = m になるような System F で正しく型付けされる項 t を見つける問題を 型再構築問題という。

定理 23.6.1 型再構築問題は決定不能である。

System F では完全な型再構築だけでなく、部分的な型再構築もさまざまなものが決定不能であるとわかっている。

定理 23.6.2 項 s が与えられたとき、s よりも多く型適用・型注釈を持つような、System F の正しく型付けされた項 t が存在するかどうかは決定不能である。

演習 23.6.3 正規化可能性は、型無し項 omega = (λx. x x) (λy. y y) が System F で型付けできないことを意味している。omega の簡約は決して簡約化に至らないからである。一方で、この事実は「組み合わせ」的に証明することができる。

1. System F の項が、型抽象でも型適用でもない場合、その項は「露出している」という。
   t がなんらかの文脈で型付け可能で、かつ erase(t) = m であるならば、ある露出した項 s が存在して、erase(s) = m かつ s は 同じ文脈かあるいは拡張された文脈で正しく型付けされる。このことを示せ。
2. erase(t) = m かつ Γ├ t : T ならば、λ. (u []) という形であるような s が存在し、erase(s) = m かつ Γ├ s : T であることを示せ。ただし は 型変数の列、 は型の列、u は 露出した項である。
3. 略
4. 略
5. 略
6. 略
7. omega は System F で型付け不能であることを示せ。

証明）
あとで

多相的な言語の多くは、型消去意味論を採用している。この意味論の下では、型検査のあとで型をすべて消去した型無し項を機械語でコンパイルしたりする。
この型消去は、System F に例外を投げるプリミティブ error を追加したとき、注意が必要である。

let f = (λX. error) in 0

上記の項は型を消去すると

let f = error in 0

となって、意図せず例外を投げてしまうことになる。このことから、実は型抽象は意味論的に重要な役割を果たすことがわかる。

この食い違いは、erase 関数を以下のように改めることで解決できる。

...
erase' (λX. t2)	=	λ_. erase' (t2)
erase' (t1 [T2])	=	erase' (t1) dummyv

以下の定理より、型消去と評価はどちから行ってもよいことがわかる。

定理 23.7.2 erase'(t) = u のとき、以下のどちらか一方が成立する。

1. それぞれの評価関係によって t と u がともに正規形
2. t -> t' かつ u -> u' で、erase'(t') = u' を満たす

let 多相は Sysetem F を以下のように一部制限したものと見なせる。

• 型変数は量子化のない型（単型）の中だけで有効
• 量化された型が矢印の左側に現れることを許さない （例：(∀X. ...) -> Nat など

また、他の System F の制限として、ランク２多相なるものなどがある。

たいしたことが書いてないので省略。

System F の多相性はしばしば非可述的であるといわれる。これは、定義されているそのもの自身を定義域とした量子化を定義に含むということである。
例えば、型 T = ∀X. X -> X の型変数X は任意の型の上を受け入れる。これは T 自身も含む。

λx:T. x [T->T] x

一方、ML に見られる多相性はしばしば可述的である。量化の値域が単型に制限されているためである。

ラッセルのパラドックス：
R = { x | x ∉ x } なる集合の集合を考える。

• R ∈ R ならば、R の定義から R は R自身 を含まないはずであるから、矛盾。
• R ∉ R ならば、R の定義から R は R自身 を含むはずなので、矛盾。

このパラドックスは、所属条件の x を、わざわざ x 自身の所属条件によって定義してしまったのが起因。
Russel は、このような所属条件を 非可述的 と呼び、類を定義する手段として、認めないことにした。これによって、パラドックスは取り除かれた。