まず，ML2 の式に対しての型推論を考える．ML2では，
トップレベル入力として，式だけでなくlet宣言を導入したが，ここではひとまず
式についての型推論のみを考え，let宣言については最後に扱うことにする．
ML2の文法は(記法は多少異なるが)以下のようであった．
| e |
::= |
x | n | true |
false | e1 op e2 |
if e1 then e2 else e3 |
| |
| |
let x = e1 in e2 |
| op |
::= |
+ | * | < |
τ ::= int | bool
さて，型推論のアルゴリズムを考える前に，そもそも「式 e が型 τ
を持つ」という関係がどのような時に成立するかを正確に記述したい．
例えば「式 1+1 は型 int を持つ」だろうが，
「式 if 1 then 2+3 else 4 は型 int を持つ」は
成立しないと思われる．この，「式 e が型 τ を持つ」
という判断を型判断(type judgment)と呼び，e : τ
と略記する．
しかし，一般に式には変数が現れるため，例えば単に x が int
を持つか，といわれても判断することができない．このため，変数に対しては，そ
れが持つ型を何か仮定しないと型判断は下せないことになる．この，変数に
対して仮定する型に関する情報を型環境(type environment)(メタ変
数Γ)と呼び，変数から型への部分関数で表される．これを使えば，
変数に対する型判断は，例えば
Γ(x) = int の時 x: int である
と言える．このことを考慮に入れて，型判断は，Γ⊢ e : τ と記述し，
型環境 Γ の下で式 e は型 τ を持つ
と読む．⊢ は数理論理学などで使われる記号で「〜という仮定の下で判
断〜が導出・証明される」くらいの意味である．インタプリタが(変数を含む)
式の値を計算するために環境を使ったように，型推論器が式の型を計算するた
めに型環境を使っているとも考えられる．
型判断は，型付け規則(typing rule)を使って導出される．
型付け規則は一般に
[<規則名>]
<型判断1> ⋯<型判断n>
<型判断>
という形で書かれ，横線の上の<型判断1>,...,
<型判断n>を規則の前提(premise)，
下にある<型判断>を規則の結論(conclusion)と呼ぶ．
例えば，以下は加算式の型付け規則である．
[T-Plus]
Γ⊢e_1 : intΓ⊢e_2 : int
Γ⊢e_1 + e_2 : int
この，型付け規則の直感的な意味(読み方)は，
前提の型判断が全て導出できたならば，結論の型判断を導出してよい
ということである．型判断は，具体的な型環境，式，型に関して，導出するも
のなので，より厳密には，規則を使うという場合には，まず，規則に現れる，
Γ, e1 などのメタ変数を実際の型環境，式などで具体化して使
わなければいけない．例えば，� ⊢ 1 : int という型判
断が既に導出されていたとしたら(� は空の型環境を表す)，この
規則の Γ を � に，e1, e2 をともに，
1に具体化することによって，規則のインスタンス，具体例(instance)
[T-Plus]
�⊢1 : int�⊢1 : int
�⊢1+1 : int
が得られる．そこで，この具体化された規則を使うと，型判断� ⊢
1+1 : int が導出できる．ちなみに，一般に何もないところから，あ
る型判断を導出するには，前提が無い型付け規則から始めることになる．
以下に，ML2の型付け規則を示す．
[T-Var]
(Γ(x) = τ)
Γ⊢x : τ
[T-Int]
Γ⊢n : int
[T-Bool]
(b = true または b = false)
Γ⊢b : bool
[T-Plus]
Γ⊢e_1 : intΓ⊢e_2 : int
Γ⊢e_1 + e_2 : int
[T-Mult]
Γ⊢e_1 : intΓ⊢e_2 : int
Γ⊢e_1 * e_2 : int
[T-Lt]
Γ⊢e_1 : intΓ⊢e_2 : int
Γ⊢e_1 < e_2 : bool
[T-If]
Γ⊢e_1 : boolΓ⊢e_2 : τΓ⊢e_3 : τ
Γ⊢if e_1 then e_2 else e_3 : τ
[T-Let]
Γ⊢e_1 : τ_1 Γ, x:τ_1 ⊢e_2 : τ_2
Γ⊢let x = e_1 in e_2 : τ_2
規則T-Letに現れる Γ, x:τ は Γ に x は
τ であるという情報を加えた拡張された型環境で，より厳密な定義と
しては，
|
dom(Γ, x:τ) = dom(Γ) ∪ {x} |
|
|
| (Γ, x:τ)(y) = |
�
�
� |
| τ |
(if x=y) |
| Γ(y) |
(otherwise) |
|
|
|
以上を踏まえると，型推論アルゴリズムの仕様は，以下のように考えることができる．
入力: 型環境 Γ と式 e
出力: Γ⊢ e : τ という型判断が導出できるような型 τ
さて，このような仕様を満たすアルゴリズムを，どのように設計したらよいの
かについては，型付け規則が指針を与えてくれる．どういうことかというと，
型付け規則を下から上に読むことによってアルゴリズムが得られるのである．
例えば，T-Int は入力式が整数リテラルならば，型環境に関わらず，
intを出力する，と読むことができるし，T-Plusは，部分式の型を求め
て，それが両方とも intであった場合には int型を出力すると読むことが
できる．
Exercise 1 [必修課題]
図11, 図12に示すコードを参考にして，型推論アル
ゴリズムを完成させよ． (ソースファイルとして typing.ml を追加するので，
make depend の実行を一度行うこと．)
Makefile:
OBJS=syntax.cmo parser.cmo lexer.cmo \
environment.cmo typing.cmo eval.cmo main.cmo
|
syntax.ml:
type ty =
TyInt
| TyBool
let pp_ty = function
TyInt -> print_string "int"
| TyBool -> print_string "bool"
|
main.ml:
open Typing
let rec read_eval_print env tyenv =
print_string "# ";
flush stdout;
let decl = Parser.toplevel Lexer.main (Lexing.from_channel stdin) in
let ty = ty_decl tyenv decl in
let (id, newenv, v) = eval_decl env decl in
Printf.printf "val %s : " id;
pp_ty ty;
print_string " = ";
pp_val v;
print_newline();
read_eval_print newenv tyenv
let initial_tyenv =
Environment.extend "i" TyInt
(Environment.extend "v" TyInt
(Environment.extend "x" TyInt Environment.empty))
let _ = read_eval_print initial_env initial_tyenv
|
Figure 11: ML2 型推論の実装 (1)
typing.ml:
open Syntax
exception Error of string
let err s = raise (Error s)
(* Type Environment *)
type tyenv = ty Environment.t
let ty_prim op ty1 ty2 = match op with
Plus -> (match ty1, ty2 with
TyInt, TyInt -> TyInt
| _ -> err ("Argument must be of integer: +"))
...
| Cons -> err "Not Implemented!"
let rec ty_exp tyenv = function
Var x ->
(try Environment.lookup x tyenv with
Environment.Not_bound -> err ("variable not bound: " ^ x))
| ILit _ -> TyInt
| BLit _ -> TyBool
| BinOp (op, exp1, exp2) ->
let tyarg1 = ty_exp tyenv exp1 in
let tyarg2 = ty_exp tyenv exp2 in
ty_prim op tyarg1 tyarg2
| IfExp (exp1, exp2, exp3) ->
...
| LetExp (id, exp1, exp2) ->
...
| _ -> err ("Not Implemented!")
let ty_decl tyenv = function
Exp e -> ty_exp tyenv e
| _ -> err ("Not Implemented!")
|
Figure 12: ML2 型推論の実装 (2)
ここでの実装のために，集合演算を実装した
モジュールである Set (set.ml, set.mli)を使用する．これも，
http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/class/isle4/src/ からダウンロードしておくこと．
(Objective Caml の標準ライブラリと名前が同じなので，ダウンロードして
おかないとコンパイル時に意味不明のエラーが発生する恐れがある．)
次に，fun式，関数適用式
e ::= ⋯ | fun x → e | e1 e2
について考える．関数の型は τ1 → τ2 とすると，
型の定義は以下のように変更される．
τ ::= int | bool | τ1 → τ2
そして，これらの式に関して型付け規則は以下のように与えられる．
[T-Abs]
Γ, x:τ_1 ⊢e : τ_2
Γ⊢fun x →e : τ_1 →τ_2
[T-App]
Γ⊢e_1 : τ_1 →τ_2 Γ⊢e_2 : τ_1
Γ⊢e_1 e_2 : τ_2
規則T-Absは，関数本体 e が，引数 x が τ1 を持つという仮定の
下で τ2 型を持つならば，fun x → e は
τ1 → τ2 型である，と読める．また，規則T-Appは，
e1の型が，そもそも関数型であり，かつ，その引数型とe2の型が一
致している場合に，適用式全体にe1の返り値型がつくことを示している．
この規則について，前節と同様に，規則を下から上に読むことでアルゴリズムを
与えようとすると T-Absで問題が生じる．というのも，e の型を調
べようとする時に x の型として何を与えてよいかわからないためである．
簡単な例として，fun x → x+1という式を考
えてみよう．これは，int → int 型の関数であることは「一目で」
わかるので，一見，xの型を int として推論を続ければよさそうだ
が，問題は，本体式であるx+1を見るまえには，x の型が
int であることがわからない，というところにある．
| 4.2.2 |
型変数，型代入と型推論アルゴリズムの仕様 |
|
この問題を解決するために，「今のところ正体がわからない未知の型」
を表す型変数(type variable)を導入する5．
τ ::= α | int | bool | τ1 → τ2
そして，型推論アルゴリズムの出力として，入力(正確には型環境中)に現れる
型変数の「正体が何か」を返すことにする．上の例だと，とりあえず x
の型は α などと置いて，型推論を続ける．推論の結果，x+1
の型は int である，という情報に加え α = int
という「型推論の結果αはint であることが判明しました」とい
う情報が返ってくることになる．最終的にT-Absより，全体の型は
α → int ，つまり，int → int で
あることがわかる．また，fun x →
fun y→ x yのような式を考えると，
以下のような手順で型推論がすすむ．
-
xの型を α と置いて，本体，つまり fun
y→ x yの型推論を行う．
- yの型を別の型変数 β と置いて，本体，つまり x
y の型推論を行う．
- x y の型推論の結果，この式の型が(さらに別の型変数) γ
であり，α = β → γ であることが判明する．
さらに詳しい，型推論の処理については後述するが，
ここで大事なことは，とりあえず未知の型として用意した型変数の正体
が，推論の過程で徐々に明らかになっていくことである．
ここまで述べたことを実装したのが図13である．ここでは型
変数は整数を使って表現している．関数 fresh_tyvar は fresh_tyvar ()
とすることで，新しい未使用の型変数を生成する．これは，T-Absのよう
に未知の型を「とりあえず α とおく」際に使われる．
上述の型変数とその正体の対応関係を，型代入(type substitution)と
呼ぶ．型代入(メタ変数として Sを使用する．)は，型変数から
型への(有限)写像として表される．以下では， Sτ で τ 中
の型変数を S を使って置き換えたような型， SΓ で，
型環境中の全ての型に S を適用したような型環境を表す．
Sτ， SΓ はより厳密には以下のように定義される．
| S α |
= |
�
�
� |
| S(α) |
if α ∈ dom( S) |
| α |
otherwise |
|
|
| S int |
= |
int |
| S bool |
= |
bool |
| S (τ1 → τ2) |
= |
Sτ1 → Sτ2 |
| |
| dom( SΓ) |
= |
dom(Γ) |
| ( SΓ)(x) |
= |
S(Γ(x)) |
型代入を使って，新しい型推論アルゴリズムの仕様は以下のように与えられる．
入力: 型環境 Γ と式 e
出力: SΓ⊢ e : τ を結論とする判断が存在するような型 τ
と代入 S
Exercise 2 [必修課題]
図13中の pp_ty，freevar_ty を完成させよ．
freevar_ty は，与えられた型中の型変数の集合を返す関数で，型は
val freevar_ty : ty -> tyvar Set.t
とする．型 'a Set.t は(実験WWWページにある) set.mli で定義されている
'aを要素とする集合を表す型である．
Exercise 3 [必修課題]
型代入に関する以下の型，関数を typing.ml 中に実装せよ．
type subst
val empty_subst : subst
val atomic_subst : tyvar -> ty -> subst
val subst_type : subst -> ty -> ty
val subst_tenv : subst -> tyenv -> tyenv
val (@@) : subst -> subst -> subst
但し，empty_subst は空の型代入であり，atomic_subst id ty は型変数 id を
ty に写す(だけの)型代入を返す．subst_type subst ty や subst_tenv subst tyenv は型代入 subst を型 ty や型環境 tyenv
に適用した結果を返す．例えば，
let alpha = fresh_tyvar () in
subst_type (atomic_subst alpha TyInt) (TyFun (alpha, TyBool))
の値は TyFun (TyInt, TyBool) になり，
let alpha = fresh_tyvar () in
let beta = fresh_tyvar () in
subst_type (atomic_subst alpha TyBool)
(subst_type (atomic_subst beta (TyFun (TyVar alpha, TyInt))) (TyVar beta))
の値は TyFun (TyBool, TyInt) になる．subst1 @@ subst2 は代入の合
成を示しており，
subst_type (subst1 @@ subst2) ty
と
subst_type subst1 (subst_type subst2 ty)
の値が等しくならなければいけない．例えば，
let alpha = fresh_tyvar () in
let beta = fresh_tyvar () in
subst_type (atomic_subst alpha TyBool
@@ atomic_subst beta (TyFun (TyVar alpha, TyInt))) (TyVar beta)
の値は TyFun (TyBool, TyInt) になる．
Makefile:
OBJS=set.cmo syntax.cmo parser.cmo lexer.cmo \
environment.cmo eval.cmo main.cmo
|
syntax.ml:
...
type tyvar = int
type ty =
TyInt
| TyBool
| TyVar of tyvar
| TyFun of ty * ty
(* pretty printing *)
let pp_ty = ...
let fresh_tyvar =
let counter = ref 0 in
let body () =
let v = !counter in
counter := v + 1; v
in body
let rec freevar_ty ty = ... (* ty -> tyvar Set.t *)
|
Figure 13: ML3 型推論の実装(1)
型付け規則を眺めてみると，T-IfやT-Plusなどの
規則は「条件式の型は boolでなくてはならない」「then節と
else節の式の型は一致していなければならない」「引数の型は intで
なくてはならない」という制約を課していることがわかる．ML2に対す
る型推論では，... = TyInt といった型(定義される言語の型を表現した値)
の比較を行うことで，こういった制約が満たされていることを検査していた．
しかし，部分式の型として，型変数が含まれる可能性がでてくるため，
そういった制約の検査には，このような単純比較は不十分である．
例えば，fun x → 1+x という式の型推論過程
を考えてみる．上で述べたように，まず，x の型を型変数
α とおいて，1+xの型推論をすることになる．
まず，部分式の型推論をするわけだが，この場合，それぞれの部分式
1, xの型は，
intと α となる．しかし，後者の型が intではない(単純比
較に失敗する)からといって，この式に型がつかないわけではない．
ここでわかることは「未知だったαは実はint である」
ということである．つまり，型に関する制約を課している部分で未知の型の
正体が求まるのである．この例の場合の処理は単純だが，
T-Ifでthen節とelse節の式の型が一致することを
検査するためには，より一般的な，
与えられたふたつの型 τ1, τ2 に対して，
S τ1 = Sτ2 なる S を求める
という問題を解かなければいけない．このような問題は単一化(unification)問題と呼ばれ，型推論だけではなく，
計算機による自動証明などにおける基本的な問題として知られている．
例えば，α, int は S(α) = int なる
型代入 Sにより単一化できる．また，α → bool と
(int → β) → β は S(α) =
int → bool かつ S(β) = bool なる
S により単一化できる．
単一化問題は，対象(ここでは型)の構造や変数の動く範囲によっては，
非常に難しくなるが，ここでは，型が単純な木構造を持ち，型代入も単に
型変数に型を割当てるだけのもの(一階の単一化(first-order
unification)と呼ばれる)なので，解である型代入を求めるアルゴリズムが
存在する．(しかも，求まる型代入がある意味で「最も良い」解であることが
わかっている．)ふたつの型を入力とし型代入を返す，単一化のアルゴリズム
は，以下のように与えられる．
|
|
| U(τ,τ) |
= |
� |
| U(α,τ) |
= |
�
�
� |
| [τ↦α] |
(α ∉FTV(τ)) |
| error |
(その他) |
|
|
| U(τ,α) |
= |
�
�
� |
| [τ↦α] |
(α ∉FTV(τ)) |
| error |
(その他) |
|
|
| U(τ11 → τ12,τ21 → τ22) |
= |
U( Sτ12, Sτ22)
( S = U(τ11,τ21)) |
| U(τ1,τ2) |
= |
error (その他の場合) |
|
Exercise 4 [必修課題]
単一化アルゴリズムにおいて，α ∉FTV(τ) という条件
はなぜ必要か考察せよ．
以上を総合すると，ML3のための型推論アルゴリズムが得られる．
例えば，e1+e2 式に対する型推論は，T-Plus規則を
下から上に読んで，
-
Γ, e1 を入力として型推論を行い， S1, τ1 を得る．
- S1Γ, e2 を入力として型推論を行い， S2,
τ2 を得る．
- S2τ1 と int を単一化し，型代入 S3を得る．
- S3τ2 と int を単一化し，型代入 S4を得る．
- S4 ∘ S3 ∘ S2 ∘ S1 と int を出力
として返す．
となる．部分式の型推論や単一化で得られた型代入は部分的な解を与えているので，
残りの処理を行う前に適用していることに注意せよ．(関数型に対する
単一化の処理と同様である．)
Exercise 5 [必修課題]
他の型付け規則に関しても同様に型推論の手続きを考え，
図14を参考にして，型推論アルゴリズムの実装を完成させよ．
Exercise 6 [難易度 2]
再帰的定義のための let rec 式の型付け規則は以下のように与えられる．
[T-LetRec]
Γ, f: τ_1 →τ_2, x: τ_1 ⊢e_1 : τ_2 Γ, f:τ_1 →τ_2 ⊢e_2 : τ
Γ⊢let rec f = fun x →e_1 in e_2 : τ
型推論アルゴリズムが let rec 式を扱えるように拡張せよ．
Exercise 7 [難易度 2]
以下は，リスト操作に関する式の型付け規則である．リストには要素の型を
τ として τ list という型を与える．
[T-Nil]
Γ⊢[] : τ list
[T-Cons]
Γ⊢e_1 : τΓ⊢e_2 : τ list
Γ⊢e_1 :: e_2 : τ list
[T-Match]
Γ⊢e_1 : τ list Γ⊢e_2 : τ' Γ, x: τ, y:τ list ⊢e_3 : τ'
Γ⊢match e_1 with [] →e_2 |
x :: y →e_3 : τ'
型推論アルゴリズムがこれらの式を扱えるように拡張せよ．
typing.ml:
let rec unify ty1 ty2 = ...
let ty_prim op ty1 ty2 = match op with
Plus ->
let subst1 = unify ty1 TyInt in
let subst2 = unify (subst_type subst1 ty2) TyInt in
(subst2 @@ subst1, TyInt)
| ...
let rec ty_exp tyenv = function
Var x ->
(try (empty_subst, Environment.lookup x tyenv) with
Environment.Not_bound -> err ("variable not bound: " ^ x))
| ILit _ -> (empty_subst, TyInt)
| BLit _ -> (empty_subst, TyBool)
| BinOp (op, exp1, exp2) ->
let (subst1, ty1) = ty_exp tyenv exp1 in
let (subst2, ty2) = ty_exp (subst_tenv subst1 tyenv) exp2 in
let (subst3, ty) = ty_prim op (subst_type subst2 ty1) ty2 in
(subst3 @@ subst2 @@ subst1, ty)
| IfExp (exp1, exp2, exp3) -> ...
| LetExp (id, exp1, exp2) -> ...
| FunExp (id, exp) ->
let domty = TyVar (fresh_tyvar ()) in
let subst, ranty =
ty_exp (Environment.extend id domty tyenv) exp in
(subst, TyFun (subst_type subst domty, ranty))
| AppExp (exp1, exp2) -> ...
| _ -> Error.typing ("Not Implemented!")
|
Figure 14: ML3 型推論の実装(2)
前節までの実装で実現される型(システム)は単相的であり，ひとつの変数を
あたかも複数の型を持つように扱えない．例えば，
let f = fun x → x in
if f true then f 2 else 3;;
のようなプログラムは，f が，ifの条件部ではbool → bool
として，また，then節では int → int として使われてい
るため， 型推論に失敗してしまう．本節では，
上記のプログラムなどを受理するよう let 多相を実装する．
Objective Caml で let f = fun x -> x;; とすると，その型は 'a -> 'a である
と表示される．しかし，ここで現れる型変数 'a は，後でその正体が判明す
る(今のところは)未知の型を表しているわけではなく，「どんな型にでも置き
換えてよい」ことを示すための，いわば「穴ボコ」につけた名前である．その
ために，'a を int で置き換えて int->int として
扱って整数に適用としたり，'a を置き換えて bool->bool として真偽値
に適用したりすることができる．このような型変数の役割の違いを
表すために，任意の型に置き換えてよい変数は，型の前に ∀
α. をつけて未知の型を表す変数と区別する．このような表現を
型スキーム(type scheme)と呼ぶ．例えば ∀ α.
α → α は型スキームである．型は ∀ α.
がひとつもついていない型スキームと考えられるが，型スキームは一般に型ではない．
例えば，(∀ α.α) → (∀ α.α)のような
表現は型とは見做されない．(型スキームを型として扱えるようなプログラミ
ング言語も存在するが，素朴に同一視すると型推論ができなくなってしまう．)
型スキームは σ で表す．型と型スキームの定義は以下の通りである．
| τ |
::= |
α | int | bool | τ1 → τ2 |
| σ |
::= |
τ | ∀ α.σ |
次に，型スキームをもとに型付け規則がどのようになるか考えてみる．
まず，一般に let で定義された変数は型スキームを持つので，
型環境は型から型スキームへの写像となる．そして，まず
変数の型付け規則は以下のように書ける．
[T-PolyVar]
(Γ(x) = ∀α_1,...,α_n. τ)
Γ⊢x : [α_1↦τ_1,...,α_n↦τ_n]τ
この規則は，変数の型スキーム中の ∀ のついた型変数は任意の型
に置き換えてよいことを，型代入
[α1↦τ1,…,αn↦τn]を使って表現し
ている．例えば，Γ(f) = ∀
α.α → α とすると，
Γ⊢ f : int → int
や
Γ⊢ f : (int → int ) → (int → int )
といった型判断を導出することができる．さて，letに関しては，大まかには
以下のような規則になる．
[T-PolyLet']
Γ⊢e_1 : τ_1 Γ, x:∀α_1.⋯∀α_n. τ_1 ⊢e_2 : τ_2
Γ⊢let x = e_1 in e_2 : τ_2
これは，e1の型から型スキームを作って，それを使って e2 の
型付けをすればいいことを示している．さて，残る問題はα1,…,αn
としてどんな型変数を選べばよいかである．もちろん，τ1に現れる
型変数に関して ∀ をつけて，「未知の型」から「任意の型」に
役割変更をするのだが，どんな型変数でも変更してよいわけではない．
役割変更してよいものはΓ に自由に出現しない
ものである．Γ 中に(自由に)現れる型変数は，
その後の型推論の過程で正体がわかって特定の型に置き換えられる可能性があるので，
任意におきかえられるものとみなしてはまずいのである．というわけで，
正しい型付け規則は，付帯条件をつけて，
[T-PolyLet]
Γ⊢e_1 : τ_1 Γ, x:∀α_1.⋯∀α_n. τ_1 ⊢e_2 : τ_2
(α1,…,αn は τ1
に自由に出現する型変数で Γ には自由に出現しない)
Γ⊢let x = e_1 in e_2 : τ_2
となる．図16の関数 closure が， τ1 と Γ
から条件を満たす型スキームを計算する関数である．(ids が上での
α1,…,αnに 対応する．)
型推論の過程において(型環境中の)型スキームに対して型代入を作用させるこ
とがある．この際，自由な型変数と束縛された型変数をともにtyvar型の値
(実際は整数)で表現しているために，型スキームへの代入の定義は多少気をつ
ける必要がある．というのは，置き換えた型中の自由な型変数と，束縛されて
いる型変数が同じ名前で表現されている可能性があるためである．
例えば，型スキーム ∀ α. α → β に
S(β) = α → int
であるような型代入を作用させることを考える．この代入は，β
を未知の型を表す α を使った型で置き換える
ことを示している．しかし，素朴に型スキーム中の β を
置き換えると，∀ α.α → α → int
という型スキームが得られてしまう．この型スキームでは，代入の前は，
未知の型を表す型変数であった，二番目のαまでが
任意に置き換えられる型変数になってしまっている．このように，代入によって
型変数の役割が変化してしまうのはまずいので避けなければいけない．
このような変数の衝突問題を避けるための，ここで取る解決(回避)策は
束縛変数の名前替え，という手法である6．
これは，例えば ∀ α.α → α と
∀β.β → β が(文字列としての見かけは違っても)意味的には同じ型スキームを表している7ことを
利用する．つまり，代入が起こる前に，新しい型変数を使って
一斉に束縛変数の名前を替えてしまって衝突が起こらないようにするのである．
上の例ならば，まず，∀ α.α → β を
∀ γ.γ → β として，その後に β を
α → int で置き換え，
∀ γ.γ → α → int を得ることになる．
このような変数の名前替えを伴う代入操作の実装を図16に示す．
rename_tysc，subst_tysc がそれぞれ型スキームの名前替え，代入の
ための関数である．
ここまでのところが理解できれば，実は型推論アルゴリズム自体に関して
影響を受けるところは少ない．実際に大きな影響をうけるのは，
変数の処理と let の処理である．変数の処理に関しては，型変数に代入する
型(型付け規則中の τ1,…,τn)は未知なので，
新しい型変数を用意してそれらを代入することになる．(図16
のコードでは，名前替えの関数を利用してそれを実現している．)
Exercise 8 [難易度 2]
図15, 16 を参考にして，多相的let
式・宣言ともに扱える型推論アルゴリズムの実装を完成させよ．
Exercise 9 [難易度 1]
以下の型付け規則を参考にして，再帰関数が多相的に扱えるように，型推論機能を
拡張せよ．
[T-PolyLetRec]
Γ, f: τ_1 →τ_2, x: τ_1 ⊢e_1 : τ_2 Γ, f:∀α_1,...,α_n.τ_1 →τ_2 ⊢e_2 : τ
(α1,…,αn は τ1 もしくは τ2 に自由に出現する型変数で Γ には自由に出現しない)
Γ⊢let rec f = fun x →e_1 in e_2 : τ
Exercise 10 [難易度 3]
Objective Caml では，「: <型>」という形式で，式や宣言された変数の型を
指定することができる．この機能を扱えるように処理系を拡張せよ．
Exercise 11 [難易度 3]
型推論時のエラー処理を，プログラマにエラー箇所がわかりやすくなるように
改善せよ．
syntax.ml
(* type scheme *)
type tysc = TyScheme of tyvar list * ty
let tysc_of_ty ty = TyScheme ([], ty)
let freevar_tysc tysc = ...
|
main.ml
...
let rec read_eval_print env tyenv =
print_string "# ";
flush stdout;
let decl = Parser.toplevel Lexer.main (Lexing.from_channel stdin) in
let (newtyenv, ty) = ty_decl tyenv decl in
let (id, newenv, v) = eval_decl env decl in
Printf.printf "val %s : " id;
pp_ty ty;
print_string " = ";
pp_val v;
print_newline();
read_eval_print newenv newtyenv
|
Figure 15: 多相的letのための型推論の実装(1)
typing.ml
type tyenv = tysc Environment.t
let rec freevar_tyenv tyenv = ...
let closure ty tyenv =
let ids = Set.diff (freevar_ty ty) (freevar_tyenv tyenv) in
TyScheme (Set.to_list ids, ty)
...
let rec subst_type subst = ...
let rename_tysc tysc =
let TyScheme (ids, ty) = tysc in
let newids = List.map (fun _ -> fresh_tyvar()) ids in
let subst_list = List.map2
(fun id newid -> atomic_subst id (TyVar newid))
ids newids in
let subst = List.fold_left (fun s1 s2 -> s1 @@ s2)
empty_subst subst_list in
TyScheme (newids, subst_type subst ty)
let subst_tysc subst tysc =
let TyScheme (newids, ty') = rename_tysc tysc in
TyScheme (newids, subst_type subst ty')
let subst_tyenv subst tenv = ...
...
let rec ty_exp tyenv = function
Var x ->
(try
let TyScheme (_, renamed_ty) =
rename_tysc (Environment.lookup x tyenv) in
(empty_subst, renamed_ty)
with Environment.Not_bound -> err ("variable not bound: " ^ x))
| ...
let ty_decl tyenv = function
Exp e -> let (_, ty) = ty_exp tyenv e in (tyenv, ty)
| Decl (id, e) -> ...
|
Figure 16: 多相的letのための型推論の実装(2)