型推論を実装・改善していく６.５ 組み込み関数の多相型推論

このようなツイートを拝見した：

instantiationだけ実装すれば組み込み関数の多相化が出来るのでは？

— taka2 (@Jj1Fxh) October 30, 2022

確かにそのとおりで、単相型推論からLet多相の間に「ユーザ定義の関数は単相だが特定の組み込み関数は多相」という型システムが想定できる。

さらにいうとこの型システムはLet多相の実装の一部を使ったものになり、「段階的に高度な型システムを実装していく」というこのシリーズの趣旨に沿ったものになる。

というわけで

「型推論を実装・改善していく６　ミュータブルな型変数を使った単相型推論（後編）」 「型推論を実装・改善していく７　Let多相型推論（前編）」

の間の記事として今回の「型推論を実装・改善していく６.５　組み込み関数の多相型推論」を追加する。

今回のコード：

gist.github.com

単相のコードとの違いはかなり小さい。

tvarにGenericが追加され、instantiate関数が加わりtypeofで使われるようになる、というのが主体。あとは各関数のパターンマッチにGenericのケースを追加するくらい。

型

型変数に新しい種類Genericを追加：

type ty =
| TVar of tvar ref
| TArrow of ty * ty
and tvar =
| Unbound of int
| Link of ty
| Generic of int

今回のコードではGenericな型変数が作成される場面はない。環境に組み込み関数の型として使われることを想定している。

つまり[("id", TArrow(TVar{contents=Generic 0}, TVar{contents=Generic 0}))]のような環境がtypeofにはじめから渡されるようなイメージだ。idはforall 'a. 'a -> 'aという型を持つ。

ユーザが自前でidのような多相関数を定義することはできない。

typeof関数

型推論の根本であるtypeofで変更されたのはEVarのケースのみ：

let rec typeof env = function
| EVar s -> instantiate (List.assoc s env)
...

今までは単にList.assoc s envしていたのがinstantiateに渡されている。変数が組み込み関数を指している場合、汎化された関数型を持っている可能性があるので、それを具体化する（Genericな型変数に対してUnbound型変数を振った新しい型にする）。

instantiate関数

前述のとおり、汎化された型を具体化するinstantiate関数：

let instantiate ty =
  let id_var_hash = Hashtbl.create 10 in
  let rec f ty = match ty with
  | TVar{contents=Generic id} ->
    (try Hashtbl.find id_var_hash id
     with Not_found ->
       let var = new_tvar () in
        Hashtbl.add id_var_hash id var;
        var)
  | TVar{contents=Unbound _} -> ty
  | TVar{contents=Link ty} -> f ty
  | TArrow(tparam, tret) -> TArrow(f tparam, f tret)
  in f ty

同じ解説をするのもなんなので、型推論を実装・改善していく８　Let多相型推論（後編）のinstantiateの項を参照してほしい。

match_fun_ty、unify、occursin

これらヘルパ関数にはパターンマッチにGenericに対応するケースを追加していく。

match_fun_ty：

let rec match_fun_ty tfunc targ = match tfunc with
...
| TVar {contents=Generic _} -> failwith "Generic type encountered, expecting arrow or instantiated variable"

関数部分の型として渡される型は、元々汎化されていないかinstantiateで具体化されているはずなので、もしmatch_fun_tyの中で遭遇したらエラー。本当はエラーじゃなくて型推論のコードがバグっていなかったらあり得ない状況ということでassert falseした方がいいかもしれない・・・。

unify；

let rec unify t1 t2 = match t1, t2 with
...
| _ -> failwith "cannot unify types"

unifyもmatch_fun_tyと同じで本来具体化した型を渡されるはず（組み込み関数を呼び出す時も必ずその関数名、つまり変数を使ってアクセスするのでinstantiateを通っている）。なのでここも本来assert falseでいい。

occursin：

let rec occursin id = function
...
| TVar{contents=Generic _} -> false
...

occursinもunifyからしか呼ばれないのだから受け取る型は具体化されているはず、だがまあ処理の意味的にはGenericな型変数の中にはUnboundな型変数は出てこないのでfalseを返すのが正しい。これは今回のコードだと関係ないが、今後のより高度な型推論の実装では役に立つ。

次回（？）

単相な型推論にGenericな型変数とinstantiateを追加することで、組み込み関数の多相を扱える型システムができた。

ここにLet式と、Let式で定義された関数を汎化するgeneralizeを追加していくことでLet多相に拡張できる。というのが「型推論を実装・改善していく７」のお話。