型推論機構の実装

4	型推論機構の実装

4.1

ML²のための型推論

まず，ML² の式に対しての型推論を考える．ML²では，トップレベル入力として，式だけでなくlet宣言を導入したが，ここではひとまず式についての型推論のみを考え，let宣言については最後に扱うことにする． ML²の文法は(記法は多少異なるが)以下のようであった．

e	::=	x \| n \| true \| false \| e₁ op e₂ \| if e₁ then e₂ else e₃
	\|	let x = e₁ in e₂
op	::=	+ \| * \| <

ここでは <式> の代わりに e という記号(メタ変数)，<識別子> の代わりに x という記号(メタ変数)を用いている．また，型(メタ変数 τ)として，整数を表す int, 真偽値を表す boolを考える．

τ ::= int | bool

4.1.1

型判断と型付け規則

さて，型推論のアルゴリズムを考える前に，そもそも「式 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)を使って導出される．型付け規則は一般に [<規則名>] <型判断₁> ⋯<型判断_n> <型判断> という形で書かれ，横線の上の<型判断₁>,..., <型判断_n>を規則の前提(premise)，下にある<型判断>を規則の結論(conclusion)と呼ぶ．例えば，以下は加算式の型付け規則である． [T-Plus] Γ⊢e_1 : intΓ⊢e_2 : int Γ⊢e_1 + e_2 : int この，型付け規則の直感的な意味(読み方)は，

前提の型判断が全て導出できたならば，結論の型判断を導出してよい

ということである．型判断は，具体的な型環境，式，型に関して，導出するものなので，より厳密には，規則を使うという場合には，まず，規則に現れる， Γ, e₁ などのメタ変数を実際の型環境，式などで具体化して使わなければいけない．例えば，� ⊢ 1 : int という型判断が既に導出されていたとしたら(� は空の型環境を表す)，この規則の Γ を � に，e₁, e₂ をともに， 1に具体化することによって，規則のインスタンス，具体例(instance) [T-Plus] �⊢1 : int�⊢1 : int �⊢1+1 : int が得られる．そこで，この具体化された規則を使うと，型判断� ⊢ 1+1 : int が導出できる．ちなみに，一般に何もないところから，ある型判断を導出するには，前提が無い型付け規則から始めることになる．

以下に，ML²の型付け規則を示す． [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)

と書くことができる．(dom(Γ)はΓの定義域を表す．)規則の前提として括弧内に書かれているのは付帯条件(side condition)と呼ばれるもので，規則を使う際に成立していなければならない条件を示している．

4.1.2

型推論アルゴリズム

以上を踏まえると，型推論アルゴリズムの仕様は，以下のように考えることができる．

入力: 型環境 Γ と式 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: ML² 型推論の実装 (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: ML² 型推論の実装 (2)

4.2

ML³の型推論

ここでの実装のために，集合演算を実装したモジュールである Set (set.ml, set.mli)を使用する．これも， http://www.sato.kuis.kyoto-u.ac.jp/~igarashi/class/isle4/src/ からダウンロードしておくこと． (Objective Caml の標準ライブラリと名前が同じなので，ダウンロードしておかないとコンパイル時に意味不明のエラーが発生する恐れがある．)

4.2.1

関数に関する型付け規則

次に，fun式，関数適用式

e ::= ⋯ | fun x → e | e₁ e₂

について考える．関数の型は τ₁ → τ₂ とすると，型の定義は以下のように変更される．

τ ::= int | bool | τ₁ → τ₂

そして，これらの式に関して型付け規則は以下のように与えられる． [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 が τ₁ を持つという仮定の下で τ₂ 型を持つならば，fun x → e は τ₁ → τ₂ 型である，と読める．また，規則T-Appは， e₁の型が，そもそも関数型であり，かつ，その引数型とe₂の型が一致している場合に，適用式全体にe₁の返り値型がつくことを示している．

この規則について，前節と同様に，規則を下から上に読むことでアルゴリズムを与えようとすると T-Absで問題が生じる．というのも，e の型を調べようとする時に x の型として何を与えてよいかわからないためである．簡単な例として，fun x → x+1という式を考えてみよう．これは，int → int 型の関数であることは「一目で」わかるので，一見，xの型を int として推論を続ければよさそうだが，問題は，本体式であるx+1を見るまえには，x の型が int であることがわからない，というところにある．

4.2.2

型変数，型代入と型推論アルゴリズムの仕様

この問題を解決するために，「今のところ正体がわからない未知の型」を表す型変数(type variable)を導入する⁵．

τ ::= α | int | bool | τ₁ → τ₂

そして，型推論アルゴリズムの出力として，入力(正確には型環境中)に現れる型変数の「正体が何か」を返すことにする．上の例だと，とりあえず 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 (τ₁ → τ₂)

Sτ₁ → Sτ₂

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: ML³ 型推論の実装(1)

4.2.3

単一化

型付け規則を眺めてみると，T-IfやT-Plusなどの規則は「条件式の型は boolでなくてはならない」「then節と else節の式の型は一致していなければならない」「引数の型は intでなくてはならない」という制約を課していることがわかる．ML²に対する型推論では，... = TyInt といった型(定義される言語の型を表現した値) の比較を行うことで，こういった制約が満たされていることを検査していた．

しかし，部分式の型として，型変数が含まれる可能性がでてくるため，そういった制約の検査には，このような単純比較は不十分である．例えば，fun x → 1+x という式の型推論過程を考えてみる．上で述べたように，まず，x の型を型変数 α とおいて，1+xの型推論をすることになる．まず，部分式の型推論をするわけだが，この場合，それぞれの部分式 1, xの型は， intと α となる．しかし，後者の型が intではない(単純比較に失敗する)からといって，この式に型がつかないわけではない．ここでわかることは「未知だったαは実はint である」ということである．つまり，型に関する制約を課している部分で未知の型の正体が求まるのである．この例の場合の処理は単純だが， T-Ifでthen節とelse節の式の型が一致することを検査するためには，より一般的な，

与えられたふたつの型 τ₁, τ₂ に対して， S τ₁ = Sτ₂ なる 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(τ₁₁ → τ₁₂,τ₂₁ → τ₂₂)

U( Sτ₁₂, Sτ₂₂) ( S = U(τ₁₁,τ₂₁))

U(τ₁,τ₂)

error (その他の場合)

� は空の型代入を表し，[α↦τ]は α を τ に写すだけの型代入である．またFTV(τ)は τ 中に現れる型変数の集合である．関数型同士の単一化は，定義域の型・値域の型をそれぞれ単一化するのだが，一方の単一化の結果得られた型代入をもう一方に適用してから単一化を行うことに注意すること．

Exercise 4 [必修課題] 単一化アルゴリズムにおいて，α ∉FTV(τ) という条件はなぜ必要か考察せよ．

4.2.4

ML³型推論アルゴリズム

以上を総合すると，ML³のための型推論アルゴリズムが得られる．例えば，e₁+e₂ 式に対する型推論は，T-Plus規則を下から上に読んで，

Γ, e₁ を入力として型推論を行い， S₁, τ₁ を得る．
S₁Γ, e₂ を入力として型推論を行い， S₂, τ₂ を得る．
S₂τ₁ と int を単一化し，型代入 S₃を得る．
S₃τ₂ と int を単一化し，型代入 S₄を得る．
S₄ ∘ S₃ ∘ S₂ ∘ S₁ と 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: ML³ 型推論の実装(2)

4.3

多相的 let の型推論

前節までの実装で実現される型(システム)は単相的であり，ひとつの変数をあたかも複数の型を持つように扱えない．例えば，


let f = fun x → x  in
if f true then f 2 else 3;;

のようなプログラムは，f が，ifの条件部ではbool → bool として，また，then節では int → int として使われているため，型推論に失敗してしまう．本節では，上記のプログラムなどを受理するよう let 多相を実装する．

4.3.1

多相性と型スキーム

Objective Caml で let f = fun x -> x;; とすると，その型は 'a -> 'a であると表示される．しかし，ここで現れる型変数 'a は，後でその正体が判明する(今のところは)未知の型を表しているわけではなく，「どんな型にでも置き換えてよい」ことを示すための，いわば「穴ボコ」につけた名前である．そのために，'a を int で置き換えて int->int として扱って整数に適用としたり，'a を置き換えて bool->bool として真偽値に適用したりすることができる．このような型変数の役割の違いを表すために，任意の型に置き換えてよい変数は，型の前に ∀ α. をつけて未知の型を表す変数と区別する．このような表現を 型スキーム(type scheme)と呼ぶ．例えば ∀ α. α → α は型スキームである．型は ∀ α. がひとつもついていない型スキームと考えられるが，型スキームは一般に型ではない．例えば，(∀ α.α) → (∀ α.α)のような表現は型とは見做されない．(型スキームを型として扱えるようなプログラミング言語も存在するが，素朴に同一視すると型推論ができなくなってしまう．) 型スキームは σ で表す．型と型スキームの定義は以下の通りである．

τ	::=	α \| int \| bool \| τ₁ → τ₂
σ	::=	τ \| ∀ α.σ

型スキーム中，∀のついている型変数を束縛されているといい，束縛されていない型変数(これらは未知の型を表す型変数である) を自由である，という．例えば ∀ α. α → α → β において， α は束縛されており，β は自由である．図15上半分に型スキームの実装上の定義を示す．関数 freevar_tysc は型スキームからその中の自由な型変数 (の集合)を求める関数である．

次に，型スキームをもとに型付け規則がどのようになるか考えてみる．まず，一般に let で定義された変数は型スキームを持つので，型環境は型から型スキームへの写像となる．そして，まず変数の型付け規則は以下のように書ける． [T-PolyVar] (Γ(x) = ∀α_1,...,α_n. τ) Γ⊢x : [α_1↦τ_1,...,α_n↦τ_n]τ この規則は，変数の型スキーム中の ∀ のついた型変数は任意の型に置き換えてよいことを，型代入 [α₁↦τ₁,…,α_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 これは，e₁の型から型スキームを作って，それを使って e₂ の型付けをすればいいことを示している．さて，残る問題はα₁,…,α_n としてどんな型変数を選べばよいかである．もちろん，τ₁に現れる型変数に関して ∀ をつけて，「未知の型」から「任意の型」に役割変更をするのだが，どんな型変数でも変更してよいわけではない．役割変更してよいものはΓ に自由に出現しないものである．Γ 中に(自由に)現れる型変数は，その後の型推論の過程で正体がわかって特定の型に置き換えられる可能性があるので，任意におきかえられるものとみなしてはまずいのである．というわけで，正しい型付け規則は，付帯条件をつけて， [T-PolyLet] Γ⊢e_1 : τ_1 Γ, x:∀α_1.⋯∀α_n. τ_1 ⊢e_2 : τ_2
(α₁,…,α_n は τ₁ に自由に出現する型変数で Γ には自由に出現しない) Γ⊢let x = e_1 in e_2 : τ_2 となる．図16の関数 closure が， τ₁ と Γ から条件を満たす型スキームを計算する関数である．(ids が上での α₁,…,α_nに対応する．)

4.3.2

型スキームに対する型代入

型推論の過程において(型環境中の)型スキームに対して型代入を作用させることがある．この際，自由な型変数と束縛された型変数をともにtyvar型の値 (実際は整数)で表現しているために，型スキームへの代入の定義は多少気をつける必要がある．というのは，置き換えた型中の自由な型変数と，束縛されている型変数が同じ名前で表現されている可能性があるためである．

例えば，型スキーム ∀ α. α → β に S(β) = α → int であるような型代入を作用させることを考える．この代入は，β を未知の型を表す α を使った型で置き換えることを示している．しかし，素朴に型スキーム中の β を置き換えると，∀ α.α → α → int という型スキームが得られてしまう．この型スキームでは，代入の前は，未知の型を表す型変数であった，二番目のαまでが任意に置き換えられる型変数になってしまっている．このように，代入によって型変数の役割が変化してしまうのはまずいので避けなければいけない．

このような変数の衝突問題を避けるための，ここで取る解決(回避)策は束縛変数の名前替え，という手法である⁶．

これは，例えば ∀ α.α → α と ∀β.β → β が(文字列としての見かけは違っても)意味的には同じ型スキームを表している⁷ことを利用する．つまり，代入が起こる前に，新しい型変数を使って一斉に束縛変数の名前を替えてしまって衝突が起こらないようにするのである．上の例ならば，まず，∀ α.α → β を ∀ γ.γ → β として，その後に β を α → int で置き換え， ∀ γ.γ → α → int を得ることになる．

このような変数の名前替えを伴う代入操作の実装を図16に示す． rename_tysc，subst_tysc がそれぞれ型スキームの名前替え，代入のための関数である．

4.3.3

型推論アルゴリズム概要

ここまでのところが理解できれば，実は型推論アルゴリズム自体に関して影響を受けるところは少ない．実際に大きな影響をうけるのは，変数の処理と let の処理である．変数の処理に関しては，型変数に代入する型(型付け規則中の τ₁,…,τ_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 : τ
(α₁,…,α_n は τ₁ もしくは τ₂ に自由に出現する型変数で Γ には自由に出現しない) Γ⊢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)