7-5. 単純な式に対する型推論

まず、原理を理解するため、もう一度、式の構文を簡単にして、「関数」と「関数適用」を排除する。 型の定義においても、TArrow (関数型)を除く。

type exp =
  | Var of string
  | IntLit of int
  | BoolLit of bool
  | Plus of exp * exp 
  | If of exp * exp * exp 

type ty = TInt | TBool | TVar of string

型推論の考え方

変数が1回しか出現しないとき、 その変数の型は何でもよいので、式e 全体の型推論が成功するように、都合の良い型をつければよい。 たとえば、(if x then 10 else 20) では x を bool型にすればよく、 (if true then x else 20) では x を int型にすればよい。 しかし、x が2回以上出現するときは、その全ての出現箇所で、 x は同じ型を持たなければならない。 この事を実現するためには、

1. 最初は x の型は「未知の型」としておき、
2. その後、x の型が(int や bool という)具体的な型であることをが判明したとき、 「未知の型」をその具体的な型で置き換える。
3. その後は、x の型がその具体的な型であるとして使う。

ここで大事なことは、「x の型が未知の型から具体的な型に変更された」という情報を、受け渡すことである。 たとえば、(e1 + e2) の形の式の型検査では、単に e1 と e2 を独立に型検査するのではなく、 e1 を型推論した結果、変数x 等の型が具体的に判明したときは、 その情報を使って、e2 の型推論を行うのである。 上記のことを実現するため、型検査で使った「型環境」を使う。 結局、型推論器 tinf1 は、入力にも出力にも型環境をとり、以下の型をもつ。

  tinf1 : tyenv -> exp -> tyenv * ty 

ちなみに、上記のような型では、tinf1 は tyenv型の引数を取るので、 「型推論は、式のみを受けとって、その型と型環境を返す」と予告したことに矛盾する、と思う人もいるだろう。 しかし、tinf1 の引数として現れる型環境 (tyenv型の引数)は、 tinf1 の処理の途中(再帰呼び出しを行っている最中)に必要になるのであって、 一番最初にtinf1 を呼びだす時には、空の型環境を与えるので、問題ない。 言い換えると、最初は、空の型環境(どの変数の型もわからない状況)から始めて、 型推論が進むにつれて、式の型が判明するとともに、変数の型も具体的に判明するのである。

上記で述べた型環境を扱う手順を整理すると、以下の通りである。

1. 型推論において、変数 x が初めて出現した時、 x の型は「未知の型α」とする。 ただし、αは型変数であり、新しい変数があらわれるごとに新しい型変数を 取るものとする。
2. その後、変数 x の型が具体的に判明したとき (x の型が TInt や TBool と一致する事がわかったとき)、 型環境における変数 x の型をその具体的な型に置き換える。
3. その後の型推論で、x の型が必要になった時は、その具体的な型を使う。

問題(提出課題ではない)

• 式e1 を (if true then if false then x else 10 else x + y + 20) とする。 この式を型推論すると、 「e1 : int で、型環境が x:int,y:int」という結果が返ってくる はずである。上記の「考え方」に基づいた手順を頭の中で実行して、実際にこの結果が 返ってくることを確認せよ。 (なお、x が初めて出現するときは x の型は不明であり、 次に、x + y の形で出現するときに、x の型が intであることが判明する。)
• 式e2 を (if x then if false then x else 10 else y) とする。 この式を型推論すると、「型が整合しない」という結果が返ってくるはずであ る。前問と同様に、頭の中で型推論することによりこのことを確認せよ。
• 式e3 を (if x then y else y) とする。 この式を型推論すると、 「e3 : bool, 型環境が x:bool,y:bool」という結果か、 「e3 : int, 型環境が x:bool,y:int」という結果のいずれかが 返ってくることが期待される。 さて、どちらが返ってくるべきであろうか？

型推論の考え方(つづき)

上記の問題の例である (if x then y else y) に対する 型推論の結果は複数あるが、そのどちらも、 「e3 の型が α、型環境が x:bool, y:α」というパターンで 表現されている。ここでαは型変数であり、 1つ目の結果は「α=bool」とすることにより得られるし、 2つ目は、「α=int」とすることにより得られる。 この場合、 「e3 : α, 型環境が x:bool,y:α」は、「最も一般的な結果(型付け)」 と呼ばれる。最も一般的な型付けは、OCaml の型システムでは(型が付く式に 対しては)常に唯一存在するこ とが保証されている。

そこで、型推論システムの実装では、「最も一般的な型付け」を 求めるように設計すればよい。 実は、今回の対象言語では、 特に難しい事を考えずに普通にアルゴリズムを書くと、 最も一般的な型付けが得られるので、あまり難しく考えなくてもよい。

以上の考え方で，型推論器 tinf1 を実装する． まず、準備として、「新しい型変数を作る」関数を定義する。 本節の範囲では、(通常の値をあらわす)変数1つにつき、型変数1つが生成される だけなので、通常の変数をそのまま使ってもよいのだが、 ディバッグなどの際に区別しやすくするため、 通常の変数名の前に "'" (quotattion mark)という文字をいれたものを型変数の名前とする。

(* new_typevar : string -> ty *)
let new_typevar s = TVar("'" ^ s)

(* tinf1 : tyenv -> exp -> tyenv * ty *)
let rec tinf1 te e =
  match e with
  | IntLit(_)    -> (te, TInt)
  | BoolLit(_)  -> (te, TBool)

次に、式 e が変数の場合である。変数名を s とする。 この場合は、s が型環境 te に含まれているときは、その型を返せばよい だけであるが、s が型環境に te に含まれていない時( x が初めて出現した時)、 新しい型変数αを作り、(s : α) という情報を型環境に追加する必要がある。 この措置を以下に書く。

  | Var(s)    ->  
        (try 
          let t1 = lookup s te in
            (te, t1)
	 with Failure(_) ->   (* 変数s が型環境 te に含まれなかった時 *)
            let tvar = new_typevar s in
            let te1 = ext te s tvar in
               (te1, tvar))

最後に、(e1+e2) の形の式の処理である。 e1 や e2 の型推論をおこない、その結果を使って (e1+e2) の型推論を行う、 という方針は型検査のときと同じであるが、意外に面倒である。なぜなら、 e1 の型推論の結果が TInt や TBool という具体的な型とは限らず、 型変数であるかもしれないからである。 ともかく処理を書くと以下のようになる。

  | Plus(e1,e2)  -> 
       let (te1, t1) = tinf1 te e1 in
       let te2 = 
         begin
          match t1 with
          | TInt -> te1
          | TVar(s) -> substitute t1 TInt te1
          | _ -> failwith "type error in Plus"
         end
       in 
       let (te3, t2) = tinf1 te2 e2 in
       let te4 = 
         begin
          match t2 with
          | TInt -> te3
          | TVar(s) -> substitute t2 TInt te3
          | _ -> failwith "type error in Plus"
         end
       in 
         (te4, TInt)

このように、最初の 6行は、e1 の処理であり、その結果として te2 という型 環境を得た。その次の6行で、e2 の処理を同様に行ない、その結果として te4 という型環境を得る。最終的に返すのは、(te4, TInt) である。 e1 と e2 に対して同様の処理をやっているので、結構長くなってしまった。

なお、(substitute t1 TInt te1) というのは、「型環境 te1 における 型変数t1 を TInt に変更した型環境」を返すものであり、 以下のように実装される。

(* substitute : ty -> ty -> tyenv -> tyenv *)
let rec substitute tvar t te =
   match te with
   | [] -> []
   | (x,t2) :: te2 -> 
       let t3 = (if t2 = tvar then t else t2) in
       (x,t3) :: (substitute tvar t te2)

  | If(e1,e2,e3) -> 
       let (te1, t1) = tinf1 te e1 in
       let te2 = 
         begin
          match t1 with
          | TBool -> te1
          | TVar(s) -> substitute t1 TBool te1
          | _ -> failwith "type error in IF"
         end
       in 
       let (te3, t2) = tinf1 te2 e2 in
       let (te4, t3) = tinf1 te3 e3 in
         begin
          match (t2,t3) with
          | (TInt,TInt) -> (te4, TInt)
          | (TBool,TBool) -> (te4, TBool)
          | (TInt,TVar(_)) -> 
	      let te5 = substitute t3 TInt te4 in (te5, TInt)
          | (TVar(_),TInt) -> 
	      let te5 = substitute t2 TInt te4 in (te5, TInt)
          | (TBool,TVar(_)) ->
	      let te5 = substitute t3 TBool te4 in (te5, TBool)
          | (TVar(_),TBool) -> 
	      let te5 = substitute t2 TBool te4 in (te5, TBool)
          | (TVar(_),TVar(_)) -> 
	      let te5 = substitute t2 t3 te4 in (te5, t3)
          | _ -> failwith "type error in IF"
         end

一番最後のケースとして、t2も t3 も型変数、ということがある。たとえば、 (if true then x else y) という式の型推論をしているときに、 このケースになる。この場合「x の型」と「yの型」が一致しなくてはいけないが、 それらが具体的に TIntでもTBool でもよい(そのどちらであるかは、現段階では未定) であるので、「xの型」を「yの型」で置きかえている。 上記のプログラムでは、(subsitute t2 t3 te4) といった計算をしている。 ここでは、もちろん、(subsitute t3 t2 te4) としても良い。 ただし、その場合、残る型変数が t2 になるので、 返すものが (te5, t3) でなく (te5, t2) となる。

本実験の最初に、「OCaml ではアルゴリズムを簡潔に記述できる」と述べたにもかかわらず、 match文の処理がこんなに長くなってしまったのは、 おかしいと思う人もいるかもしれない。たしかにそうであるが、 実は、ここでは、次の節で述べる「単一化」の考え方を使わずに実装しようとしたため長くなった、 というのが真相である。

最後に、関数 tinf1 の使いかたであるが、 型環境の初期値は空の型環境であるので、以下のようにすればよい。

   tinf1 [ ] e 

発展課題 7-5. 前半

• 関数tinf1 に、いくつかの式を与え、正しく型推論できていることを確かめよ。

ちょっと横道: リストに対する Iterator

(* substitute : ty -> ty -> tyenv -> tyenv *)
let rec substitute tvar t te =
   List.map (fun (x,t2) ->
             if t2 = tvar then (x,t) else (x,t2))
            te

発展課題 7-5. 後半

• 上記のように substitute を書き換えても、元の subsitute と同じ型と同じ動作をすることを確認しなさい。また、2つのバージョンで、動作速度はどうなるか(非常に長いリストに対して動かしたり、同じ操作を 1000回繰返す等をして)調べなさい。
• OCaml の標準ライブラリに含まれるListモジュールには、他にも iterator が定義されている。これらについて学習しなさい。そこには「List.map は tail recursive ではないが、Lisp.rev_mapはtail recursive である」と書いてある。「関数が tail recursiveである」とはどういう意味であるか調べなさい。

亀山 幸義