型システム実装幕間１ 各種matchヘルパ関数について

ここまで実装した型システムではコアな部分であるtypeofの中で使うヘルパ関数として５つmatch_..._tyという名前の関数を定義している：

• match_fun_ty
• match_tuple_ty
• match_rec_ty
• match_ref_ty
• match_list_ty

これらは元々効率的なHM型推論のお手本として使ったGrow Your Own Type SystemというGitHubレポジトリでmatch_fun_tyが使われていたのを参考にしている。

中身を見ると：

let rec match_fun_ty tfunc targ = match tfunc with
| TArrow(tparam,tret) -> unify tparam targ; tret
| TVar {contents=Link ty} -> match_fun_ty ty targ
| TVar ({contents=Unbound(_,level)} as tvar) ->
  let tparam = new_tvar level in
  let tret = new_tvar level in
  tvar := Link(TArrow(tparam,tret));
  unify tparam targ;
  tret
| TVar {contents=Generic _} -> failwith "Generic type encountered, expecting arrow or instantiated variable"
| _ -> failwith "Non-arrow type found in function position"

match_fun_tyの場合は、もし引数が関数型ならその仮引数の型tparamと（match_fun_tyの引数として渡される）実引数の型targを単一化した上で、返り値の型を返している。この場合新しい型変数は作られていないのが一つのポイント。

新しく型変数が作成されるのはTVar ({contents=Unbound(_,level)} as tvar)のケース、つまりまだ単一化でリンクにされていない型変数だった場合。そのケースでは型変数を二つ作ってそれらを保持した関数型を作成する。

いろいろ参考にさせていただいているLunarMLに関するこちらの記事LunarML進捗・2022年2月 | 雑記帳に「以前、関数適用の型推論の部分を ... 「関数の型が既知の場合は新規の型変数を作らない」... という風に書き換えたところ、型推論が結構高速化した覚えがあります。」と書いてあったのも記憶にあって、この方が効率的なんだろうと漠然と考えていた。

しかしよく読むと「型推論の際は型が未知の変数（fn x => ... の x）が現れたらfreshな型変数を導入して割り当てると思いますが、あまりバカスカ型変数を導入すると管理用のテーブルが膨張して遅くなるのです（使用するデータ構造にも依るとは思いますが）。」とも書いてあり、現在の実装のように型変数が破壊的変更で違う型にリンクするようになっていて「管理用のテーブル」なるものがない場合は実際のところどの程度の効率化になっているのか怪しいように思う。

型変数を無闇に作ると実際の型に到達するまでに辿らなければいけないリンクが長くなりすぎるおそれはあるが、それは（以前も書いたが）Union Findでよくやられている経路圧縮（複数のリンクを辿ったら元のリンクの参照先を書き換える）などすればいいはず。

もし新しく型変数を振って単一化していくのでいいのであればmatch_fun_tyなどはいらなくなる。

そしてtypeofのEAppのケースは現在の：

let rec typeof env level = function
...
| EApp(func, arg) ->
  let tfunc = typeof env level func in
  let targ = typeof env level arg in
  match_fun_ty tfunc targ

の形から

let rec typeof env level = function
...
| EApp(func, arg) ->
  let tfunc = typeof env level func in
  let targ = typeof env level arg in
  let tparam = new_tvar level in
  let tret = new_tvar level in
  unify tfunc (TArrow(tparam, tret));
  unify tparam targ;
  tret

このように変わる。この部分でのコード量は増えるのだが、match_fun_tyの方にあるボイラープレートなパターンマッチが消せるので行数は減っているのと、match_fun_tyのようなヘルパ関数だと中で何が起きているかわかりにくいので明示的になっているのは好ましい気がする。

他の部分も同じように修正してmatch...ty関数を消したコードがこれ。

ベンチマークなど取れるようになったら実行時間がどのように変化するのか比較してみたい。