項 t と文脈 Γ が与えられたとき、(Γ, t) の解が最低限充足せねばならない制約の集合を求めるアルゴリズムを示す。
このアルゴリズムは本質的には通常の型検査アルゴリズムと同じであるが、唯一異なるのは、制約の検査というより後の検討のために記録するだけということである。
定義 22.3.1- 制約集合 C は等式の集合 { Si = Ti i∈1..n } である。
- S と T の代入による具体化 σS と σT が同一になるとき、代入σ は等式 S = T を単一化するという。
- σ が C のすべての等式を単一化するとき、σ は C を単一化する（または充足する）という。
定義 22.3.2 制約型付け関係 Γ├ t : T |x C は
図22-1にて定義される。
Γ├ t : T |x C は、「制約Cが充足されるならば、項 t は Γ の前提の下で型 T を持つ」と読む。
また、|x は各部分導出において導入される型変数の集合を表している。
図22-1 制約型付け規則
| Γ├ x : T |ø {} | CT-Var |
| x:T ∈ Γ |
| Γ, x:T1 ├ t2 : T2 | x C | CT-Abs |
| Γ├ λx:T1. t2 : T1 -> T2 |x C |
| Γ├ t1 : T1 |x1 C1 | Γ├ t2 : T2 |x2 C2 | x1∩x2 = x1∩FV(T2) = X2∩FV(T1) = ø | X はフレッシュ | C' = C1∪C2∪{T1=T2 -> X} | CT-App |
| Γ├ t1 t2 : X |x1∪x2∪{X} C' |
| Γ├ t1 : T |x C | C' = C ∪ {T=Nat} | CT-Succ |
| Γ├ succ t1 : Nat |x C' |
| Γ├ t1 : T |x C | C' = C ∪ {T=Nat} | CT-Pred |
| Γ├ pred t1 : Nat |x C' |
| Γ├ t1 : T |x C | C' = C ∪ {T=Nat} | CT-IsZero |
| Γ├ iszero t1 : Bool |x C' |
| | CT-True |
| Γ├ true : Bool |ø {} |
| | CT-False |
| Γ├ false : Bool |ø {} |
| Γ├ t1 : T1 |x1 C1 | Γ├ t2 : T2 |x2 C2 | Γ├ t3 : T3 |x3 C3 | x1,x2,x3は重複しない | C' = C1∪C2∪C3∪{T1=Bool, T2=T3} | CT-If |
| Γ├ if t1 then t2 else t3 : T2 |x1∪x2∪x3 C' |
演習 22.3.3 あるS, x, Cに対して、結論が以下のようになるような制約型付け導出を構築せよ。
├ λx:X. λy:Y. λz:Z. (x z) (y z) : S |x C
解答例）
省略
制約型付け関係のアイデアは、t が Γ の下で型付け可能かどうかを、制約 C を集めるのと同時に（制約 C を共有しながら）結果の型 S を求める。その後に、C を充足する任意の代入 σ により、σS は t が持ちうる型になる。充足する代入が存在しなければ、型付け可能なように t を具現化することはできない。
例えば、項 t = λx:X->Y. x 0 に対する制約集合は [X -> Y = Nat -> Z] であり、結果の型 S は (X -> Y) -> Z となる。
この制約集合を満たす代入は以下の通り複数ある。
- σ = [X |-> Nat, Y |-> Z], σS = (Nat -> Z) -> Z
- σ = [X |-> Nat, Z |-> Bool, Y |-> Bool], σS = (Nat -> Bool) -> Bool
定義 22.3.4 Γ├ t : S | C とする。(Γ, t, S, C) の解とは、σ が C を充足し、かつσS = T となるような組 (σ, T) のことである。
文脈Γ と項 t が与えられたとき、Γ と t の型変数を具体化して正しい型付けを生成する方法には、二種類の表現がある。
(1) [宣言的な方法]
定義22.2.1の意味で、(Γ, t) のすべての解の集合として表現する。
(2) [アルゴリズム的な方法] 制約型付け関係を通じて、Γ├ t : S | C を満たす S と C を見つけることで、(Γ, t, S, C) の解の集合を得る。
この二つの表現は等価であることは以下の二段階で示される:
- (Γ, t, S, C) の解はすべて (Γ, t) の解でもある (定理 22.3.5)
- (Γ, t) の解はすべて、(Γ, t, S, C) の解に拡張できる (定理 22.3.7)
定理 22.3.5 [制約型付けの健全性] Γ├ t : S | C とする。もし (σ, T) が (Γ, t, S, C) の解なら、それは (Γ, t) の解でもある。
証明）
Γ├ t : S | C の制約型付け導出に関する帰納法による。最後に使った規則で場合分けをする。
1) CT-Var の場合 t = x x:S∈Γ C = {}
C は空であるから、単に σS = T である。T-Var により、σΓ├ x : T を得る。
2) CT-Abs の場合
...
以下省略
定義 22.3.6 x に含まれる変数のすべてに対して未定義で、他の変数には σ と同じように振る舞う代入を、σ\x と書く。
定理 22.3.7 [制約型付けの完全性] Γ├ t : S |x C とする。(σ, T) が (Γ, t) の解であり、かつ dom(σ) ∩ x = ø ならば、σ'\x = σ となるような (Γ, t, S, C) の解 (σ', T) が存在する。
証明）
制約型付け導出に関する帰納法による。
1) CT-Var の場合 t = x x:S∈Γ
仮定より、(σ, T) は (Γ, x) の解であるから、T = σS とわかる。つまり、(σ, T) は (Γ, x, S, {}) の解。
2) CT-Abs の場合
....
以下省略
系 22.3.8 Γ├ t : S | C とする。(Γ, t) の解が存在するとき、かつそのときに限り、(Γ, t, S, C) の解が存在する。
証明）
定理22.3.5 と 定理22.3.7 による
演習 22.3.9 製品レベルのコンパイラでは、フレッシュな型変数名の生成は "gensym" という関数の呼び出しに置き換えられる。この操作は、隠れたグローバル変数に対して副作用を持つため、形式的な論証が難しい。しかし、使われていない型変数名を適用規則を通じて「直列的に受け渡す」ことで、この過程を数学的に模倣することはできる。
F は異なる型変数名の列であるとし、制約生成関係を Γ├F t : T |F' C と書くことにする。フレッシュな型変数が必要なときは、F の最初の変数を取り出し、残りを F' として返す。
このアルゴリズムの規則を書き下せ。その規則と元の制約生成規則が適切な意味で等価になることを証明せよ。
規則）
| Γ├F t1 : T1 |F' C1 | Γ├F' t2 : T2 |F'' C2 | F'' = X, F''' | CT-App' |
| Γ├F t1 t2 : X |F''' C1 ∪ C2 ∪ {T1=T2->X} |
など
証明）
以下を示せば良い。
- [健全性] Γ├F t : T |F' C かつ Γや t に現れる変数がFに出現しないならば、Γ├ t : T |F\F' C
- [完全性] Γ├ t : T |x C ならば、xの名前の並び替えFが存在し、Γ├F t : T |ø C
演習 22.3.10 演習22.3.9 のアルゴリズムを ML で実装せよ。
解答例）
省略（付録に記載）
演習 22.3.11 一般的な再帰関数定義を扱うように制約生成アルゴリズムを拡張せよ。
解答例）
| Γ├ t1 : T1 |x1 C1 | X は x1,Γ,t1に現れない | CT-Rec |
| Γ├ fix t1 : X |x1∪{X} C1 {T1=X->X} |