前節の実装では、PLUSやIFの処理において、 「「型変数を含むかもしれない型」が TInt であるかどうか」といった テストを何度か行った。これは、特に IF の処理においては、何度もあらわれ、 プログラムを読みにくくする要因であった。これを改善するため、上記のテス トを(少し一般化して)実行する関数を作って、型推論器はそれを利用すること にしよう。この「一般化された上記のテスト」は、単一化 (unification, ユニフィケーション) と呼ばれる。
(あらかじめ補足: 「関数型言語だから、本節のような難しい型推論が必要である」というのは 正しくない。実は、「型」の世界に、 関数型 (a->b)、リスト型 (a list), 構造体の型(struct)、オブジェクトの型 などの、どれか1つでもはいっている時に、型推論を行おうとおもうと、 本節で述べるような一般的な型推論が必要になる。 つまり、複雑度があがるのは、関数型があることではなく、「型から型を構成する」もの が1つでもあること、である。「型から型を構成するもの」を「型構成子」という。 本節では、煩雑さを避けるため、関数型のみ追加した型システムに対する 型推論を述べるが、実は、関数型以外の型構成子があっても対応できる。)
もう1つ例題を書くと、 'y->(int->'w)->'x と ('x->'z)->('x->'z) を単一化する問題というのは、 「この中にあらわれる型変数に、うまい型を代入すると、この2つの型は、同じ型になるかどうか」 を判定することである。 この場合の答えとしては、['x:=int->'w, 'y:=(int->'w)->(int->'w), 'z:=int->'w] とすることにより、両辺とも同じ型になるので、YES である。 なお、'x:=int->'w というのは、型変数'x を int->'w 型にするという 代入(substitution)を表している。
さて、単一化関数について記述しよう。
なお、通常、単一化問題は、2つの型の間だけでなく、 (t1=t2, t3=t4, ...) という、たくさんの(型の間の)単一化問題として 定式化される。
type tyvar = string type ty = TInt | TBool | TArrow of ty * ty | TVar of tyvar type tyenv = (string * ty) list type tysubst = (tyvar * ty) listtyvar は string と同じだが、(普通の)変数と型変数を区別したいので、 ここでは、わざわざ tyvar という名前をつけている。 tyenv は、既に出てきた型環境であり、(普通の)変数に対する型をあらわして いる。 たとえば、 [("x", TInt); ("y",TArrow(TBool,TVar("'a"))] である。 一方、tysubst は、型環境と似た形をしているが、中身は異なり、 型変数と型の対応をあらわす。たとえば、 [("'a", TInt); ("'b",TArrow(TBool,TVar("'a"))] である。 これは、単一化問題の「答え」を表すために用いられる。
さて、次にいきなり unify という単一化関数を書いてしまおう。 この関数は、実は、型代入を操作するためのいくつかの関数を必要としている のだが、それらは後回しにしている。 関数unify は、 unify [(TVar("'a"), TArrow(TInt,TBool)); ...] のようにして呼びだし、単一化可能ならば型代入を返し、単一化不能ならば Failureを起こして終了する。
(* unify : (ty * ty) list -> tysubst *)
let unify eql =
let rec solve eql theta =
match eql with
| [] -> theta
| (t1,t2):: eql2 ->
(if t1 = t2 then solve eql2 theta
else (match (t1,t2) with
| (TArrow(t11,t12),TArrow(t21,t22))
-> solve ((t11,t21)::(t12,t22)::eql2) theta
| (TVar(s), _)
-> if (occurs t1 t2) then failwith "unification failed"
else solve (subst_eql [(s,t2)] eql2)
(compose_subst [(s,t2)] theta)
| (_,TVar(s))
-> if (occurs t2 t1) then failwith "unification failed"
else solve (subst_eql [(s,t1)] eql2)
(compose_subst [(s,t1)] theta)
| (_,_) -> failwith "unification failed"))
in solve eql []
え、すごく難しいアルゴリズムがでてくるかと思いきや、いきなり終わってし
まった!
unifyは、subst_eql や compose_subst, occursなどの補助関数を使ってはい
るが、概念的には簡単なアルゴリズムなのである。言葉で書けばもっと簡単な
のだが、ここでは、いきなりコードを書いてしまった。
少し解説しよう。unify は solve という内部関数をもっている。 solve の第1引数は、(型同士の)等式のリストであり、 第2引数の theta は、「作りかけの型代入」である。 つまり、solve は再帰呼び出しで何度も呼ばれている間に、だんだんと thetaを増やしていって、最終的に thetaを完成させて返す、という動作をする。
solve は、まず、eqlという等式リストが空リストのときは、 残っている単一化問題がない、ということなので、 これまでに作成した型代入 theta を返して終了する。
eql が空でないときは、その先頭の要素を (t1,t2) とする。これは t1=t2 という(型に関する)等式をあらわしている。 t1とt2がもともと一致するとき(上記のOCamlのコードは、t1 = t2 と書いてある 部分で、t1 と t2 が一致するかどうかを調べている)、 この等式はもう何もしなくても解を持つので、その等式は「残っている単一化 問題」から捨てて、残りの等式を解きにいく。つまり、(solve eql2 theta) という再帰呼び出しをする。
t1とt2が一致しない時は、t1とt2 の中に含まれている型変数を適当に選択す ることにより一致させられる可能性があるので、まだ、計算を続ける。 そこで、t1,t2 についてのパターンマッチを行う。
t1が (t11->t12)の形で、t2が (t21->t22) の形のときは、 t11=t21 かつ t12=t22 でなければいけないので、それら2つの等式を 等式リストに追加して、続行する。 すなわち、 (solve ((t11,t21)::(t12,t22)::eql2) theta) という再帰呼び出しをする。
次に、t1が型変数のときを考える。この場合、t2 が何であろうと、型変数t1 を 型t2に代入することにより、t1=t2 という等式は満たされる。 そこで、t1=t2 を、解となる代入に追加する。これが (compose_subst [(s,t2)] theta) というところである。(ここで、 (t1,t2) を追加するのではなく、(s,t2) を追加しているのは、ちょっとした 実装上の都合である。もう少し解説すると、 t1 が TVar(s) の形の型変数のとき、t1でなく、その型変数の名前をあらわす 文字列である s を代入に追加することにしている。)
ところで、この操作の前に (occurs t1 t2) というチェックをおこない、 もし、これが true であれば、いきなり単一化関数全体が fail して終了して いる。これは何だろうか？ 実は、 'a = (TInt -> ('a -> TBool)) のように、 「型変数'a」と「型変数'a を含む型」との等式は、どのような代入をおこなっ ても解を持たない。なぜなら、'a をどのような型で置き換えても、 右辺の方が常に大きな型になってしまうからである。 というわけで、「t1 が型変数のとき t2が何であろうと、。。。等式を満たす ことができる」と上で書いたのは、嘘であり、「t2 がt1の型変数を含まない」 場合のみ等式を満たすことができるのである。 そこで、このためのチェックを occurs という関数がおこなう。 occurs は以下のように実装できる。
let rec occurs tx t =
if tx = t then true
else (match t with
| TArrow(t1,t2) -> (occurs tx t1) or (occurs tx t2)
| _ -> false)
ここで現れる or という関数は、論理の or である。
さて、一気にunify を説明してしまった。 unify の本質的なところは上で述べたように簡単であるが、補助関数がごちゃ ごちゃいっぱい必要であり、これらは各自学習してほしい。ここでは コードのみを載せる。
(* subst_ty : tysubst -> ty -> ty *)
(* 代入thetaを型t に適用する *)
let rec subst_ty theta t =
let rec subst_ty1 theta1 s =
match theta1 with
[] -> TVar(s)
| (tx,t1):: theta2 ->
if tx = s then t1
else subst_ty1 theta2 s
in match t with
TInt -> TInt
| TBool -> TBool
| TArrow(t2,t3) -> TArrow(subst_ty theta t2, subst_ty theta t3)
| TVar(s) -> subst_ty1 theta s
(* subst_tyenv : tysubst -> tyenv -> tyenv *)
(* 代入thetaを型環境 te に適用する *)
let subst_tyenv theta te =
List.map (fun (x,t) -> (x, subst_ty theta t)) te
(* List.mapは OCaml における リストに対する iterator である *)
(* subst_eq : tysubst -> (ty * ty) list -> (ty * ty) list *)
(* 代入thetaを型の等式のリスト eql に適用する *)
let subst_eql theta eql =
List.map (fun (t1,t2) -> (subst_ty theta t1, subst_ty theta t2))
eql
(* compose_subst : tysubst -> tysubst -> tysubst *)
(* 2つの代入を合成した代入を返す。theta1 が「先」でtheta2が「後」である *)
let rec compose_subst theta2 theta1 =
let theta11 =
List.map (fun (tx,t) -> (tx, subst_ty theta2 t)) theta1
in
List.fold_left (fun tau -> fun (tx,t) ->
try
let _ = lookup tx theta1 in
tau
with Failure(_) ->
(tx,t) :: tau)
theta11
theta2
(* List.fold_left は、リストに対する iterator であり、
* List.fold_left f x [a1;a2;a3] は (f (f (f x a1) a2) a3) を返す
*)
List.map や List.fold_leftなど、Listモジュールにおける関数がでてきて
驚いた人もいるだろう。これについては、上記のコメントのほか、
前節において若干の説明をしたので、各自学習してほしい。
亀山 幸義