JavaScriptによる型推論器の実装：バリアント型

JavaScript Ibis

前：let と let rec　目次

パターンマッチ対象の型推論

昨日挙げた以下のコードではバリアントを使用していますが、パターンマッチ対象である m の型はどこにも明示されていません。

let rec add =
  fun m -> fun n ->
    case m of
      Zero -> fun _ -> n
    | Succ -> fun k -> Succ (add k n)
http://d.hatena.ne.jp/takuto_h/20110405/variant

Ibis の case 式はバリアントのみを対象とするという制限がありますから、m がバリアント型であることは確かです。しかしそれ以上のことはわかりません。では、どのようにして具体的な型を推論しているのでしょうか。

タグ環境

話は単純で、パターン内に現れるコンストラクタ名から推論します。コンストラクタ名からそれによって生成されるバリアント型を取り出せる環境を用意しておき、それを参照すればよいのです。これをタグ環境と呼びます。イメージとしては

{ Zero: nat, Succ: nat }

のような形式です。
Ibis では variants という変数にタグ環境が入っています。

 91:    case "VariantDef":
 92:      var typeName = expr.typeName;
 93:      var paramTypeExprs = expr.typeCtors;
 94:      var paramTypes = {};
 95:      var variantType = Type.createVariant(typeName, paramTypes);
 96:      Env.add(env, typeName, variantType);
 97:      for (var ctorName in paramTypeExprs) {
 98:        var typeExpr = paramTypeExprs[ctorName];
 99:        var paramType = eval(env, typeExpr);
100:        paramTypes[ctorName] = paramType;
101:        var ctorType = Type.createFun(paramType, variantType);
102:        Env.add(ctxt, ctorName, Type.createTypeSchema([], ctorType));
103:        Env.add(variants, ctorName, variantType);
104:      }
105:      return Type.Unit;
https://github.com/takuto-h/ibis-js/blob/ibis-js-1.0.0/src/inferer.js

バリアント型の定義（type という予約語を使った式）の型推論では、103行目でタグ環境 variants に コンストラクタ名 ctorName をキーとしてバリアント型 variantType を登録しています。

106:    case "Case":
107:      var inferredType = infer(ctxt, env, variants, expr.variantExpr);
108:      var clauseExprs = expr.clauseExprs;
109:      var elseClause = expr.elseClause;
110:      var variantType = null;
111:      for (var ctorName in clauseExprs) {
112:        variantType = Env.find(variants, ctorName);
113:        if (!variantType) {
114:          throw new IbisError("undefined constructor: " + ctorName);
115:        }
116:        break;
117:      }
118:      unify(inferredType, variantType);
..
https://github.com/takuto-h/ibis-js/blob/ibis-js-1.0.0/src/inferer.js

case 式の型推論では、112行目でいくつかのパターン節 clauseExprs から最初に取り出せたコンストラクタ名 ctorName を使ってタグ環境 variants からバリアント型 variantType を取り出しています。

このことによって、コンストラクタ名からバリアント型は一意に定まらなくてはならないために、同一のスコープ内で異なる型を返す同名のコンストラクタを同時に定義することはできないことがわかります。

前：let と let rec　目次