Arantium Maestum

プログラミング、囲碁、読書の話題

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

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

Record型を追加:

type ty =
...
| TRecord of (string * ty) list

基本的にはタプル型の要素に文字列のラベルがついているというイメージでいい。

TRecord of (string * ty) listTRecord of string list * ty listではどっちがいいのか・・・。前者の方がラベルと型の順番が密接になっていていい気もするが、多くの処理で「ラベルだけ取り出す」「型だけ取り出す」といった処理が入るので後者の方が綺麗に書けるかもしれない。

レコード式ERecordと、レコードのフィールドにアクセスするEProjection:

type exp =
...
| ERecord of (string * exp) list
| EProjection of exp * string * ty

ERecordはTRecordと似ているが、保持しているのが「ラベルと式」のリストである(TRecordは「ラベルと型」)。

後者はタプルのアクセスと同じでEProjection of exp * stringだと型推論できない。OCamlの昔の制約と同じで、あるラベルはモジュール内でユニークである必要があると定義すれば、フィールドアクセスでラベルがわかった時点で全体の型もわかる。というわけでEProjection式それ自体に前段階で「ラベルから推測してexp部分が何の型であるべきか」を持たせている。型推論の一部としてやってもいいのだが、その場合はラベルとレコード型を対応させる新しい「環境」を作ってtypeofに渡す必要が出てくるのでやめておいた。

typeof

型推論typeof関数にERecordとEProjectionのケースを追加していく。

ERecordの場合:

let rec typeof env level = function
...
| ERecord les -> TRecord (List.map (fun (l,e) -> (l, typeof env level e)) les)

ERecordの持つ「ラベルと式」のリストの式部分に対してtypeofを適用して作った「ラベルと型」のリストを持たせたTRecordを返す。

フィールドアクセスのEProjection:

| EProjection (e,l,t) -> (match t with
  | TRecord lts -> unify t (typeof env level e); List.assoc l lts
  | _ -> failwith "Record type expected in projection annotation")

EProjectionに持たせた型注釈がTRecord型であることを確認し、レコードであるはずのtypeof env level eと単一化した上で、型注釈の部分からフィールドのラベルに対応する型を取り出す。

generalizeinstantiate

generalizeinstantiateに追加する処理はタプルの時の処理と非常に似ている:

let rec generalize level ty = match ty with
...
| TTuple ts -> TTuple (List.map (generalize level) ts)
| TRecord lts -> TRecord (List.map (fun (l,t) -> (l, generalize level t)) lts)

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)
  | TRecord lts -> TRecord (List.map (fun (l,t) -> (l, f t)) lts)
  in f ty

ラベルがついているので、それをつけたまま型の部分には再帰的にgeneralize/instantiateを適用するだけ。

unify

単一化unify関数に関して、片方がレコードだったとしてももう片方が

  • 完全に同一のレコード
  • 何らかの型変数
  • レコード型とまったく単一化できない型(例えばTBool、TTuple)

のケースはすでにワイルドカードも使って表現されている。

なので追加する必要があるのは両方がレコードだが、型変数の存在などにより内部が同一ではないケース:

let rec unify t1 t2 = match t1, t2 with
...
| TRecord lts1, TRecord lts2 ->
  if List.map fst lts1 != List.map fst lts2 then failwith "Cannot unify records with mismatched labels";
  List.iter2 unify (List.map snd lts1) (List.map snd lts2)

まずラベルの同一性を確認する。今回は実装を簡単にするためにも、ラベルの出てくる順番も同一でなくてはいけないという制約をつけている。

ラベルが同一であれば、あとは型部分をそれぞれ単一化するだけ。

occursinadjustlevel

occursinadjustlevelgeneralize/instantiateよりもさらにタプルに似ている:

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

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

ラベルのことは無視していいのでList.map sndで型のリストを作って、あとはTupleとまったく同じ処理。

それ以外

match_fun_tymatch_tuple_tyはいちいち更新するのがめんどくさくなったので

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

ワイルドカード化してしまった。網羅性を捨てているが・・・。

TRecordの内部構造

今回の実装を見ているとやはりstring list * ty listに軍配をあげたくなる(式の部分もstring list * exp listにする前提で)。

唯一めんどくさくなるのは

let rec typeof env level = function
...
| EProjection (e,l,t) -> (match t with
  | TRecord lts -> unify t (typeof env level e); List.assoc l lts

の部分で、List.assoc l ltsをList.findとList.nthの組み合わせにする必要が生じるが、それ以外のすべての箇所では例えば

let rec typeof env level = function
...
| ERecord les -> TRecord (List.map (fun (l,e) -> (l, typeof env level e)) les)

| ERecord(ls,es) -> TRecord (ls, List.map (typeof env level) es)

のような形になる。こっちにしたほうがよかったかもしれない。

次回

次はバリアント型を追加していく。