JavaScript による型推論器の実装：多相型
中身のない型変数
前回の例では、すべての型変数（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
JavaScript による型推論器の実装：型変数と単一化
未知の型
型推論の肝は、未知の型の扱いです。
例えば、
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 という式の型を推論する過程をソースコードを見ながらたどっていきましょう。
- x の型を未知の型 paramType とします。(infer:36)
- その仮定の下で double x の型 retType を推論します。(infer:37-39)
- (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 関数の説明には多相型が絡んでくるので、ここでいったん説明を区切ります。
目次 次：多相型
JavaScript による型推論器の実装
型推論に興味はあるけど、抽象的な説明が多く難しそうだと思っている方々。基礎的なことを押さえておけば、型推論器は簡単に実装できます。
ここでは、私が JavaScript で書いた型推論器を例に、型推論の基本的なアルゴリズムの一例を具体的に説明していきます。解説対象は、ibis-js-1.0.0です。
型推論の可視化ツールを使いながら読むとよりわかりやすいかもしれません。
Ibis クイックチュートリアル
四則演算
> 1 + 2 * 3 - : int = 7 > (1 + 2) * 3 - : int = 9
変数
> let x = 123 - : int = 123 > x - : int = 123
関数
> let double = fun x -> x * 2 - : (int -> int) = <closure> > double 2 - : int = 4
再帰関数
> let rec fac = fun n -> if n = 0 then 1 else n * fac (n - 1) - : (int -> int) = <closure> > fac 10 - : int = 3628800
多相関数
> let id = fun x -> x
- : ('a -> 'a) = <closure>
> id 1
- : int = 1
> id true
- : bool = true
タプル
> let (a, b) = (1, 2) - : (int * int) = (1, 2) > a - : int = 1 > b - : int = 2
バリアント
> type num = Zero of unit | Pos of int | Neg of int - : unit = () > let num_to_int = fun n -> case n of Zero -> fun _ -> 0 | Pos -> fun i -> i | Neg -> fun i -> 0 - i - : (num -> int) = <closure> > num_to_int (Zero ()) - : int = 0 > num_to_int (Pos 123) - : int = 123 > num_to_int (Neg 456) - : int = -456 > let is_zero = fun n -> case n of Zero -> fun _ -> true | else -> fun _ -> false - : num -> bool = <closure> > is_zero (Zero ()) - : bool = true
再帰的なバリアント
> type nat = Zero of unit | Succ of nat - : unit = () > let zero = Zero () - : nat = (Zero ()) > let one = Succ zero - : nat = (Succ (Zero ())) > let two = Succ one - : nat = (Succ (Succ (Zero ()))) > let rec add = fun m -> fun n -> case m of Zero -> fun _ -> n | Succ -> fun k -> Succ (add k n) - : (nat -> (nat -> nat)) = <closure> > add one two - : nat = (Succ (Succ (Succ (Zero ()))))
JavaScriptで型推論器を作りました
JavaScriptで型推論付き静的型付け言語のインタプリタを作成しました。これは、サイボウズ・ラボユースのメンバーとして開発をさせていただいたものです。ライセンスは MIT License です。
型推論の実装方法を解説するため、メジャーであり気軽に試せるJavaScriptを使って型推論器を書きました。
文法の簡単な説明は
Ibis クイックチュートリアル
実装の詳細については
JavaScript による型推論器の実装
をご覧ください。
