7-6.単一化

前節では、関数等のない単純な式に対する型推論器を作成した。 本節では、関数等を含む式に対する一般的な型推論を解くための鍵となるアルゴリズムである単一化を学ぶ。 (次節で、単一化を用いて、型推論器を実装する。)

前節の実装では、PLUSやIFの処理において、 「「型変数を含むかもしれない型」が TInt であるかどうか」といった テストを何度か行った。これは、特に IF の処理においては、何度もあらわれ、 プログラムを読みにくくする要因であった。これを改善するため、 上記のテストを(少し一般化して)実行する関数を作って、 型推論器はそれを利用することにしよう。 この「一般化された上記のテスト」は、単一化(unification, ユニフィケーション) と呼ばれる。

(あらかじめ補足: 「関数型言語だから、本節のような難しい型推論が必要である」というのは正しくない。 実は、「型」の世界に、 関数型 (a->b)、リスト型 (a list), 構造体の型(struct)、オブジェクトの型などの、 どれか1つでもはいっている時に、型推論を行おうとおもうと、 本節で述べるような一般的な型推論が必要になる。 つまり、複雑度があがるのは、関数型があることではなく、「型から型を構成する」もの が1つでもあること、である。「型から型を構成するもの」を「型構成子」という。 本節では、煩雑さを避けるため、関数型のみ追加した型システムに対する 型推論を述べるが、実は、関数型以外の型構成子があっても対応できる。)

問題 (課題ではない)

まず、関数型などの型構成子をもつと、 型推論が大変になることを実感してもらうため、 以下の問題を(OCaml処理系に頼らずに、自分の頭で)考えてみてほしい。 (解説) e1=e2 という部分式があることと、 f の第1引数は x で、それは g の第2引数でもある等を使うと、fとg の型が f: 'a -> 'b -> 'c -> 'd と g: 'c -> 'a -> 'b -> 'd であることがわかる。さらに、 (if ... then f else g) の形であるので、f と g の型は完全に一致しなくて はならないので、 結局、'a='b='c となる。つまり、x:'a, y:'a, c:'a, f:'a->'a->'a->'d, g:'a->'a->'a->'d というのが本問の答えである。 (なお、ここで、型を表す変数(型変数)は、普通の変数とは異なるので、'a の ように single quote を付けて表現した。これは OCaml の真似をしたもので ある。)

単一化問題

上記の問題でやったことは、 (型変数を含む)型が2つ与えられたとき、型変数を適当な型で置きかえて、 それら2つを一致させることができるか、という問題である。これが「単一化問題」 (unification problem) である。

もう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)を表している。

さて、単一化関数について記述しよう。

さて、「YES」という判定結果のとき、対応する代入は1つとは限らないが、 例によって、「最も一般的な代入」は(実質的に)一意的であるので、 問題は起きない。

なお、通常、単一化問題は、2つの型の間だけでなく、 (t1=t2, t3=t4, ...) という、たくさんの(型の間の)単一化問題として 定式化される。

単一化アルゴリズム

さて、早速単一化を解決する方法を見てみよう。 まず、型、型環境、型代入の3つを定義する。
type tyvar = string
type ty = TInt | TBool | TArrow of ty * ty | TVar of tyvar
type tyenv = (string * ty) list
type tysubst = (tyvar * ty) list
tyvar は 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 
           begin
            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"
            end
  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モジュールにおける関数がでてきて 驚いた人もいるだろう。これについては、上記のコメントのほか、 前節において若干の説明をしたので、各自学習してほしい。

発展課題 7-6.


トップ, 前へ. 次へ.

亀山 幸義