まず，ML2 の式に対しての型推論を考える．ML2では， トップレベル入力として，式だけでなくlet宣言を導入したが，ここではひとまず 式についての型推論のみを考え，let宣言については最後に扱うことにする． ML2の文法は(記法は多少異なるが)以下のようであった．
|
ここでは <式> の代わりに e という記号(メタ変数)，<識別子> の代わりに x という記号(メタ変数)を用いている． また，型(メタ変数 τ)として，整数を表す int, 真偽値を表す boolを考える．
| ��τ�::=�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(Γ)はΓの定義域を表す．)規則 の前提として括弧内に書かれているのは付帯条件(side condition)と 呼ばれるもので，規則を使う際に成立していなければならない条件を示してい る．
以上を踏まえると，型推論アルゴリズムの仕様は，以下のように考えることができる．
入力: 型環境 Γ と式 e
出力: Γ⊢ e : τ という型判断が導出できるような型 τ
さて，このような仕様を満たすアルゴリズムを，どのように設計したらよいの かについては，型付け規則が指針を与えてくれる．どういうことかというと， 型付け規則を下から上に読むことによってアルゴリズムが得られるのである． 例えば，T-Int は入力式が整数リテラルならば，型環境に関わらず， intを出力する，と読むことができるし，T-Plusは，部分式の型を求め て，それが両方とも intであった場合には int型を出力すると読むことが できる．
Makefile:
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)
ここでの実装のために，集合演算を実装した モジュールである MySet (mySet.ml, mySet.mli)を使用する．これも， http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/class/isle4/src/ からダウンロードしておくこと．
次に，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 であることがわからない，というところにある．
この問題を解決するために，「今のところ正体がわからない未知の型」 を表す型変数(type variable)を導入する5．
| �τ��::=��α�|�int��|�bool��|�τ1�→�τ2 |
そして，型推論アルゴリズムの出力として，入力(正確には型環境中)に現れる 型変数の「正体が何か」を返すことにする．上の例だと，とりあえず x の型は α などと置いて，型推論を続ける．推論の結果，x+1 の型は int である，という情報に加え α = int という「型推論の結果αはint であることが判明しました」とい う情報が返ってくることになる．最終的にT-Absより，全体の型は α → int ，つまり，int → int で あることがわかる．また，fun x → fun y→ x� yのような式を考えると， 以下のような手順で型推論がすすむ．
さらに詳しい，型推論の処理については後述するが， ここで大事なことは，とりあえず未知の型として用意した型変数の正体 が，推論の過程で徐々に明らかになっていくことである．
ここまで述べたことを実装したのが図13である．ここでは型 変数は整数を使って表現している．関数 fresh_tyvar は fresh_tyvar () とすることで，新しい未使用の型変数を生成する．これは，T-Absのよう に未知の型を「とりあえず α とおく」際に使われる．
上述の型変数とその正体の対応関係を，型代入(type substitution)と 呼ぶ．型代入(メタ変数として Sを使用する．)は，型変数から 型への(有限)写像として表される．以下では， Sτ で τ 中 の型変数を S を使って置き換えたような型， SΓ で， 型環境中の全ての型に S を適用したような型環境を表す． Sτ， SΓ はより厳密には以下のように定義される．
|
型代入を使って，新しい型推論アルゴリズムの仕様は以下のように与えられる．
入力: 型環境 Γ と式 e
出力: SΓ⊢ e : τ を結論とする判断が存在するような型 τ と代入 S
val freevar_ty : ty -> tyvar MySet.tとする．型 'a MySet.t は(実験WWWページにある) mySet.mli で定義され ている'aを要素とする集合を表す型である．
type subst = (tyvar * ty) list val subst_type : subst -> ty -> ty型代入を表す型 subst は型変数と型ののペアのリスト [(id1,ty1); ...; (idn,tyn)] で表現する．このリストは [idn ↦ tyn] ∘ ⋯ ∘[id1 ↦ ty1] という型代入を 表す．順番が反転していること，また，代入の合成を表すので，ty1 に現れ る型変数は後続のリストの表す型代入の影響を受けることに注意すること．
例えば，
let alpha = fresh_tyvar () in subst_type [(alpha, TyInt)] (TyFun (alpha, TyBool))
の値は TyFun (TyInt, TyBool) になり，
let alpha = fresh_tyvar () in let beta = fresh_tyvar () in subst_type [(beta, (TyFun (TyVar alpha, TyInt))); (alpha, TyBool)] (TyVar beta)
の値は TyFun (TyBool, TyInt) になる．
Makefile:
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 MySet.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節の式の型が一致することを 検査するためには，より一般的な，
与えられた型のペアの集合 {(τ11, τ12), …, (τn1, τn2)} に対して， S τ11 = Sτ12, …, S τn1 = Sτn2 な る S を求める
という問題を解かなければいけない．このような問題は単一化(unification)問題と呼ばれ，型推論だけではなく， 計算機による自動証明などにおける基本的な問題として知られている．
例えば，α, int は S(α) = int なる 型代入 Sにより単一化できる．また，α → bool と (int → β) → β は S(α) = int → bool かつ S(β) = bool なる S により単一化できる．
単一化問題は，対象(ここでは型)の構造や変数の動く範囲によっては， 非常に難しくなるが，ここでは，型が単純な木構造を持ち，型代入も単に 型変数に型を割当てるだけのもの(一階の単一化(first-order unification)と呼ばれる)なので，解である型代入を求めるアルゴリズムが 存在する．(しかも，求まる型代入がある意味で「最も良い」解であることが わかっている．)型のペアの集合を入力とし型代入を返す，単一化のアルゴリズム は，以下のように与えられる． (X⊎ Y は，X∩ Y = ∅ のときの X と Y の和集合を示す．)
|
∅ は空の型代入を表 し，[α↦τ]は αを τ に写すだけの型代入 である．またFTV(τ)は τ中に現れる型変数の集合である．2番 目，3番目の式は α について解けたので，その結果を残りの方程式に 適用してさらにそれらを解き続ける(単一化を試みる)ことを示している．
val unify : (ty * ty) list -> substとして実装せよ．
以上を総合すると，ML3のための型推論アルゴリズムが得られる． 例えば，e1+e2 式に対する型推論は，T-Plus規則を 下から上に読んで，
となる．部分式の型推論で得られた型代入を方程式とみなして，再び単一化を 行うのは，ひとつの部分式から [α ↦ τ1]，もうひとつか らは [α ↦ τ2] という代入が得られた時 にτ1 と τ2 の整合性が取れているか(単一化できるか)を検査 するためである．
typing.ml:
let rec unify = ... (* eqs_of_subst : subst -> (ty * ty) list 型代入を型の等式集合に変換 *) let eqs_of_subst s = ... let ty_prim op ty1 ty2 = match op with Plus -> ([(ty1, TyInt), (ty2, TyInt)], TyInt) | ... 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 (s1, ty1) = ty_exp tyenv exp1 in let (s2, ty2) = ty_exp tyenv exp2 in let (eqs3, ty) = ty_prim op ty1 ty2 in let eqs = (eqs_of_subst s1) @ (eqs_of_subst s2) @ eqs3 in let s3 = unify eqs in (s3, subst_type s3 ty) | IfExp (exp1, exp2, exp3) -> ... | LetExp (id, exp1, exp2) -> ... | FunExp (id, exp) -> let domty = TyVar (fresh_tyvar ()) in let s, ranty = ty_exp (Environment.extend id domty tyenv) exp in (subst, TyFun (subst_type s 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)と呼ぶ．例えば ∀ α. α → α は型スキームである．型は ∀ α. がひとつもついていない型スキームと考えられるが，型スキームは一般に型ではない． 例えば，(∀ α.α) → (∀ α.α)のような 表現は型とは見做されない．(型スキームを型として扱えるようなプログラミ ング言語も存在するが，素朴に同一視すると型推論ができなくなってしまう．) 型スキームは σ で表す．型と型スキームの定義は以下の通りである．
|
型スキーム中，∀のついている型変数を束縛されているといい， 束縛されていない型変数(これらは未知の型を表す型変数である) を自由である，という． 例えば ∀ α. α → α → β において， α は束縛されており，β は自由である． 図15上半分に型スキームの実装上の定義を示す． 関数 freevar_tysc は型スキームからその中の自由な型変数 (の集合)を求める関数である．
次に，型スキームをもとに型付け規則がどのようになるか考えてみる． まず，一般に 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 のコードでは，名前替えの関数を利用してそれを実現している．)
syntax.ml
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 = MySet.diff (freevar_ty ty) (freevar_tyenv tyenv) in TyScheme (MySet.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)