Hindley Milner型推論に機能を追加していく４ Tuple型の追加

HM型推論にタプル型を追加していく。今回のコードはこちら。

型

タプルというのはちょっと不思議な型で、型コンストラクタとして表そうとすると「任意の数の型をとる型コンストラクタ」となる。理論上の考え方としては二つの型をとるPair型コンストラクタとUnit型を合わせて、式レベルではConsとNilでやるリストを型レベルでやっているものと同型だと見るのが良さそう。

ただし今回はPairを使った実装はしない：

type ty =
...
| TTuple of ty list

見てのとおり、直接「型のリスト」を持つTTupleを定義している。

式

式として追加するのはタプル値を作成するETuple式と、タプルから特定の要素を取り出すETupleAccess：

type exp =
...
| ETuple of exp list
| ETupleAccess of exp * int * int

ETupleは式のリストを持つ。こっちは直感的だと思うが、問題はETupleAccess。

ETupleAccessはタプル部分のexp、取り出したい要素の番地を表すint、そしてこのタプルの全要素数を表すintを保持している。この最後のものは必要かどうかが考えどころだ。

元々はなしでやることを考えていたのだが、型推論のうまいやり方が思いつかなかった。調べてみたところ、Design Concepts in Programming Languagesという本のType Reconstruction章が作者にオンラインでPreprintとして公開されていた。こちらの後半でETupleAccessに相応する部分でこの「タプルの要素数」を表す数が何故必要なのか説明せよという演習問題があり、「あ、やっぱりないと難しいのか」と急遽修正した次第。

この数がないと型推論でいくつ型変数を作成しないといけないのかがわからないのがポイント。「アクセス時にタプルの大きさが式に埋め込まれていなければいけない」というのは大きな制約のように思えるが、OCamlなどでも任意の大きさのタプルの要素を取る場合パターンマッチを使うが、その場合は要素数が明示されている。任意のタプルの第一、第二要素を取るfst、sndという関数はあるが第三要素以降を返す多相関数は存在しない。fst、sndは型検査については結構特殊な実装になっているのではないか？機会があったら調べてみたい。

（余談だがDesign Concepts in Programming Languagesの演習問題でLouis Reasonerが出てくる。SICPをやった人ならニヤッとする名前である）

typeof

型推論を行うtypeofには追加した２つの式のそれぞれのケースを足していく。

まずはETuple:

let rec typeof env level = function
...
| ETuple es -> TTuple (List.map (typeof env level) es)

ETupleの持つ式に対して再帰的にtypeofしていって、それらの型を組み合わせたTTuple型を返す。

ETupleAccess：

| ETupleAccess(e,i,n) -> match_tuple_ty (typeof env level e) i n

新たに定義したヘルパ関数match_tuple_tyに丸投げ。

match_tuple_ty

match_fun_tyと似たような形のETupleAccess用のヘルパ関数。

タプルとしてアクセスされる式の型ttupに対してパターンマッチしている。

ttupがTTupleだったケース：

let rec match_tuple_ty ttup i n = match ttup with
| TTuple ts ->
    if List.length ts != n then failwith "Incorrect tuple arity";
    List.nth ts i

TTupleの要素数がETupleAccessで指定されていた数と合致しているかを確認してからi番目の要素（これも型）を返す。

Linkになっている型変数の場合：

| TVar {contents=Link ty} -> match_tuple_ty ty i n

match_fun_tyと同じく、リンクを辿った先に対して再帰的にmatch_tuple_tyを適用。

Unboundな型変数の場合：

| TVar ({contents=Unbound(_,level)} as tvar) ->
  let ts = List.init n (fun _ -> new_tvar level) in
  tvar := Link(TTuple ts);
  List.nth ts i

新しくn個の別々な型変数を作り、そのリストをもつ新しいTTupleを作り、元のUnboundな型変数をそのTTupleにリンクした上で、新しいTTupleのi番目の要素（新しく作成した型変数の一つ）を返す。

それ以外のケース：

| TVar {contents=Generic _} -> failwith "Generic type encountered, expecting tuple or instantiated variable"
| TUnit | TBool | TInt | TArrow _ -> failwith "Non-tuple type found in tuple position"

これらはすべてエラーになる。ETupleAccessの第一要素はTTuple型に同一化できるものでなくてはいけない。

generalizeとinstantiate

これら二つの関数は型をとって型を返す。

両方ty型に対するパターンマッチなので、新しくTTupleのケースを追加：

let rec generalize level ty = match ty with
...
| TTuple ts -> TTuple (List.map (generalize level) ts)

let instantiate level ty =
  let id_var_hash = Hashtbl.create 10 in
  let rec f ty = match ty with
  ...
  | TTuple ts -> TTuple (List.map f ts)
  in f ty

どちらもList.mapでTTupleの要素に対して再帰的な関数適用をしている。

occursinとadjustlevel

これら関数もty型に対するパターンマッチ。

occursinはboolを返すのでList.existsを使う：

let rec occursin id = function
...
| TTuple ts -> List.exists (occursin id) ts

adjustlevelは副作用で型変数を変更して()を返すのでList.iterを使っている：

let rec adjustlevel level = function
...
| TTuple ts -> List.iter (adjustlevel level) ts

それ以外

match_fun_tyはTTupleに遭遇したらエラー：

let rec match_fun_ty tfunc targ = match tfunc with
...
| TUnit | TBool | TInt | TTuple _ -> failwith "Non-arrow type found in function position"

unifyは変更なし（ワイルドカードパターンで捕捉され、正しくエラーを投げる）

次回

次はレコード型を追加していく。