Hindley Milner型推論に機能を追加していく９ Refの追加（前編）

Ref型とそれに関係した式の処理を追加する。

この記事で（HM型推論なしで）追加したものと同じ：

zehnpaard.hatenablog.com

ref型を作るためのオペレータref（ここら辺OCamlだと型とオペレータの名前が被ったりしてややこしい）、ref型からデータを取り出すderef、そしてref型に破壊的代入をするassignの三つの式を用意する。

実はRef型はLet多相との相性が悪く、型安全性を保つためにValue Restrictionという特殊な制約と処理を追加する必要がある。その話は次回に持ち越し。

今回の（Value Restrictionなしなので型安全ではない）コードはここ

型

TRef型を追加：

type ty =
...
| TRef of ty

refは何らかの値を保持するので、TRefはその値の型を保持する。

型に対してパターンマッチしている既存関数

いつものようにgeneralize, instantiate, unify, occursin, adjustlevelにTRefを追加していく：

let rec generalize level ty = match ty with
...
| TRef ty -> TRef (generalize level ty)

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

let rec unify t1 t2 = match t1, t2 with
...
| TRef t1, TRef t2 -> unify t1 t2
...

let rec occursin id = function
...
| TRef t -> occursin id t

let rec adjustlevel level = function
...
| TRef t -> adjustlevel level t

TRefは一つのty型を保持しているだけなので、追加する処理も非常に簡単にその保持しているtyに対して再帰的に関数適用するだけ。

match_fun_tyなどはTRefが与えられるとワイルドカードのマッチで実行時エラーになるので修正の必要なし。

式

前述の通り三種の式を追加：

type exp =
...
| ERef of exp
| EDeref of exp
| EAssign of exp * exp

• ERefはなんらかの式をとり、その評価結果を保持するref型の値を作る
• EDerefはref型の式をとり、そのrefが保持する値を返す
• EAssignはref型の式とそのrefに代入する式をとり、後者の評価結果を前者に代入する（元々入っていた値は破棄される）

typeof

上記三種の式に対するケースを追加していく。

まずERef：

let rec typeof env level = function
...
| ERef e -> TRef (typeof env level e)

保持する値（の式）eの型を調べて、その型を保持するTRef型を返す。

EDeref：

| EDeref e -> match_ref_ty (typeof env level e)

まずderefする対象の式eの型を調べ、新しく定義したヘルパ関数match_ref_tyに渡す（この関数の実装については後述）。

match_ref_tyはeの型がTRef型と単一化できるか調べ、できるならそのTRef型が保持する型を返す。

EAssign：

| EAssign(e1,e2) ->
  let t2 = typeof env level e2 in
  unify (match_ref_ty (typeof env level e1)) t2;
  TUnit

e1が代入する先のref、e2が代入する値の式だ。

まず代入する値の型をlet t2 = typeof env level e2で求める。

(match_ref_ty (typeof env level e1))でref式の型がTRefだと見做せることを確認し、TRefの保持する型とt2を単一化する。

その上でrefへの代入の結果は()なので、最終的にTUnitを返す。

match_ref_ty

前述の通りtypeofのEDerefとEAssignケースで使われるmatch_ref_tyは型をとり、それがTRef型と単一化できる場合はそのTRef型の保持する型を返す：

let rec match_ref_ty ty = match ty with
| TRef ty -> ty
| TVar {contents=Link ty} -> match_ref_ty ty
| TVar ({contents=Unbound(_,level)} as tvar) ->
  let ty = new_tvar level in
  tvar := Link(TRef ty);
  ty
| TVar {contents=Generic _} -> failwith "Generic type encountered, expecting ref or instantiated variable"
| _ -> failwith "Non-ref type found in ref position"

他のmatch_..._ty関数と同じ構造で、もし引数のtyがTRef型そのものなら新しい型変数などは作成せずに直接処理する。

Linkな型変数の場合はリンクを辿って再帰的適用。

Unboundな型変数の場合は新しく型変数とそれを保持するTRef型を作り、tyを破壊的更新でそのTRefにリンクさせた上で作った型変数を返す。

それ以外のケースは他のmatch_..._tyと同じくエラー。

次回

前述のとおり今回のコードはRefとLet多相の関係により型安全ではない。次回はその問題について詳しく見ていき、その解決のためOCamlなどでも導入されているValue Restrictionを実装する。