JavaScript による型推論器の実装:多相型

前:型変数と単一化 目次 次:let と let rec

中身のない型変数

前回の例では、すべての型変数(Var オブジェクト)に型が代入されました。しかし、以下の場合はどうでしょう。

fun x -> x

関数の本体に手がかり(関数適用など)がありませんから、x の具体的な型はわかりません。よって、中身のない型変数が残ってしまいます。
これを処理し多相型を生成するのが、createPolyType 関数です。

スキーマ

上記の式は、'a -> 'a という型を持ちます('a は型変数)。しかし、型の中にどんな型変数が含まれているのかの情報は後で必要となるので、あわせて保持しておかなくてはなりません。含まれる型変数を列挙したものを型に付加したデータを、型スキーマと呼びます。

Ibis における型スキーマは、TypeSchema オブジェクトで表されます。

124:  function TypeSchema(typeVars, bodyType) {
125:    this.tag = "TypeSchema";
126:    this.typeVars = typeVars;
127:    this.bodyType = bodyType;
128:  }
..
142:  function createTypeSchema(typeVars, bodyType) {
143:    return new TypeSchema(typeVars, bodyType);
144:  }
src/type.js

typeVars が型変数の配列、bodyType が本体の型です。bodyType が 'a -> 'a なら typeVars には 'a が、bodyType が 'a -> 'b -> 'a ならtypeVars には 'a と 'b がそれぞれ含まれます。

多相型の生成

では、多相型を生成する関数 createPolyType を見てみましょう。

266:  function createPolyType(type) {
267:    var freeVars = [];
268:    var unwrappedType = unwrapVar(type, freeVars);
269:    return Type.createTypeSchema(freeVars, unwrappedType);
270:  }
src/inferer.js

unwrapVar 関数は、Var オブジェクトの value が null でないなら中身を取り出して型変数を剥いでやります。null なら、それを freeVars に登録し、中身のない型変数をそのまま返します。結果として、unwrappedType には中身のない型変数だけが残り、freeVars にはそれらがすべて登録されています。この freeVars を createTypeSchema 関数で型スキーマの typeVars とします。

これだけで多相型が生成できたのかと疑う方もいらっしゃるでしょう。実際、生成する側はこれですべてですが、利用する側にはちょっとしたからくりがあります。

多相型の利用

多相型を利用する前に呼び出さなくてはならない関数があります。createAlphaEquivalent 関数です。これは型スキーマの typeVars に含まれる型変数すべてを、新しい型変数で置き換えます。

253:  function createAlphaEquivalent(typeSchema) {
254:    var map = {};
255:    var oldTypeVars = typeSchema.typeVars;
256:    var newTypeVars = []
257:    for (var i in oldTypeVars) {
258:      var freshVar = Type.createVar(null);
259:      map[oldTypeVars[i]] = freshVar;
260:      newTypeVars.push(freshVar);
261:    }
262:    var newBodyType = Type.subst(typeSchema.bodyType, map);
263:    return Type.createTypeSchema(newTypeVars, newBodyType);
264:  }
src/inferer.js

この関数は、変数の型推論で呼ばれています。

29:    case "Var":
30:      var typeSchema = Env.find(ctxt, expr.varName);
31:      if (!typeSchema) {
32:        throw new IbisError("undefined variable: " + expr.varName);
33:      }
34:      return createAlphaEquivalent(typeSchema).bodyType;
src/inferer.js

変数の型スキーマが登録してある環境 ctxt から型スキーマを取り出し、失敗したら例外を投げます。最後に createAlphaEquivalent 関数を使って型変数をすべて新しく置き換えた本体の型を返します。

新しく導入された型変数の中身は null です。単一化の過程で型が確定するかもしれませんし、しないかもしれません。いずれにせよ、どんな型にでもなれるということですから、紛れもない多相型です。また、導入されたのは新しい型変数ですから、変数の型スキーマとしてもともと登録されていたものに対し単一化は何の影響も与えません。

変数の型スキーマを登録する側である let の型推論では、createPolyType と createAlphaEquivalent が使われています。

47:    case "Let":
48:      var inferredType = infer(ctxt, env, variants, expr.valueExpr);
49:      var typeSchema = createPolyType(inferredType);
50:      Env.add(ctxt, expr.varName, typeSchema);
51:      return createAlphaEquivalent(typeSchema).bodyType;
src/inferer.js

型と型スキーマ

型と型スキーマの区別がわかりにくいと思うので、整理しておきます。

  1. infer 関数によって推論されるのは、「型」である
  2. let の型推論で「型」から「型スキーマ」が作られ、変数と「型スキーマ」が対応づけられる
  3. 変数の型推論で、変数に対応づけられた「型スキーマ」から新しい型変数を含む「型」が作られる

重要なのは、

  • 一般に「変数の型」と呼ばれるものは、Ibis では型スキーマである

ということです。
これで多相型の説明は終わりです。
前:型変数と単一化 目次 次:let と let rec