JavaScript による型推論器の実装：型変数と単一化

JavaScript Ibis

目次　次：多相型

未知の型

型推論の肝は、未知の型の扱いです。
例えば、

fun x -> x * 2

という式の型推論をする際、仮引数 x の型は指定されていませんから未知です。関数の本体を見て「x は * の左辺に現れる」という情報を見つけることで初めて x の型が int だとわかります。

Var オブジェクトと型変数

Ibis においては、未知の型を表すための Var オブジェクトが存在します。Ibis.Type.createVar 関数を呼び出して作成します。

49:  var currentId = 0;
50:  function Var(id, value) {
51:    this.tag = "Var";
52:    this.id = id;
53:    this.value = value;
54:  }
..
58:  function createVar(value) {
59:    return new Var(currentId++, value);
60:  }
src/type.js

id というのは変数のユニークさを確保するための仕組みで、今はあまり気にしなくても構いません。

重要なのは、value というプロパティです。未知の型が現れたとき、value を null にして Var オブジェクトを作成しておき、型がわかり次第 value に代入します。このように、Var オブジェクトは型を代入する変数のように使われるため、型変数と呼びます。

var unknownType = Ibis.Type.createVar(null);
..
// 型が exactType だとわかったら代入
unknownType.value = exactType

現に、無名関数の型推論ではこの createVar が呼ばれています。

35:    case "Abs":
36:      var paramType = Type.createVar(null);
..
39:      return Type.createFun(paramType, retType);
src/inferer.js

paramType というのは仮引数の型であり、fun x -> x * 2 という式では x の型にあたります。

単一化

では、実際の型がわかるのはどのようなときでしょうか。例として、関数適用があげられます。

f : int -> int とわかっていて、x の型が Var オブジェクトのとき、f x という式が見つかるとどうでしょうか。f の引数は int 型のはずですから、Var の value には int が代入できます。このようにして、x の型がわかります。

しかし、ここで Var の value にすでに 型が代入されていた場合はどうでしょうか。この場合、int と Var の value が等価であることを確かめる必要があります。すでに代入した型が bool だった場合、bool 型の値に int -> int 型の関数を適用していることになってしまうからです。これを考慮にいれたアルゴリズムが、単一化（unification）です。

164:  function unify(type1, type2) {
165:    if (type1 == type2) {
166:      return;
167:    }
168:    if (type1.tag == "Var") {
169:      if (!type1.value) {
..
173:        type1.value = type2;
174:      } else {
175:        unify(type1.value, type2);
176:      }
177:    } else if (type2.tag == "Var") {
178:      if (!type2.value) {
..
182:        type2.value = type1;
183:      } else {
184:        unify(type2.value, type1);
185:      }
..
198:    } else {
199:      throw new IbisError("unification error: " + type1 + " and " + type2);
200:    }
201:  }
src/inferer.js

unify という関数は、type1 と type2 を単一化します。ここでの単一化とは、２つの型が等しいならば何もせず、一方が未知の型ならばその value にもう一方を代入する、という作業です。value にすでに型が入っているようなら、その型ともう一方を単一化します。単一化不可能（例えば、int と bool）なら、例外を投げます。

では、先ほど例に挙げた関数適用の型推論を見てみましょう。

41:    case "App":
42:      var funType = infer(ctxt, env, variants, expr.funExpr);
43:      var argType = infer(ctxt, env, variants, expr.argExpr);
44:      var retType = Type.createVar(null);
45:      unify(funType, Type.createFun(argType, retType));
46:      return retType;
src/inferer.js

f x という式があったとき、f の型を funType, x の型を argType に代入します。ここで、f x の型はわからないので retType に Var オブジェクトを代入し、funType と (argType -> retType) という型を単一化します。最後に retType を f x の型として返します。

実例

ここまで理解できれば、単相的な型の推論はほぼわかったようなものです。例として、double : int -> int という関数があったときに、fun x -> double x という式の型を推論する過程をソースコードを見ながらたどっていきましょう。

  1. x の型を未知の型 paramType とします。(infer:36)
  2. その仮定の下で double x の型 retType を推論します。(infer:37-39)
    1. double の型（funType）は int -> int、x の型（argType = paramType）は未知、f x の型（retType）も未知です。(infer:42-44)
    2. funType と (argType -> retType) を単一化します。(infer:45)
      1. argType.value には int, retType.value にも int が代入されます。(unify:164-201)
    3. retType を double x の型として返します。(infer:46)
  3. (paramType -> retType) を fun x -> double x の型として返します。(infer:40)

argType = paramType ですから、paramType.value は int, retType.value も int です。よって、fun x -> double x : int -> int です。

正確には、paramType も retType も Var ですから、生の int ではありません。よって、最終的には Var を剥いでやる必要があります。それがunwrapVar 関数です。unwrapVar 関数の説明には多相型が絡んでくるので、ここでいったん説明を区切ります。
目次　次：多相型