Hindley Milner型推論に機能を追加していく１１ Refの追加（後編）
前回書いたとおり、Let多相とRefとパラメトリックな型を組み合わせても型安全性が維持されるためには、Letで型が全称化される対象の式を制限する必要があり、これをvalue restrictionと呼ぶ。
残念ながらこの「全称化される式」であるsimple valuesのリストは公式リファレンスなどを探しても見つからなかった。
唯一見つかったのはReal World OCamlの不完全なリスト：
Constants (i.e., things like integer and floating-point literals)
Constructors that only contain other simple values
Function declarations, i.e., expressions that begin with fun or function, or the equivalent let binding, let f x = ...
let bindings of the form let var = expr1 in expr2, where both expr1 and expr2 are simple values
であるが、これは抜けがあることがわかっている。
@dico_lequeさんに教えていただいたのだがSMLではこれに相当するsyntactic valuesがスタンダードで定義されている：
SMLの場合はDefinitionの4.7節とかを参照https://t.co/6L8xQulp5h
— でこれき (@dico_leque) November 13, 2022
しかしこれは例えば「let bindings of the form let var = expr1 in expr2, where both expr1 and expr2 are simple values」が抜けており、OCamlに比べて制約が厳しくなっているようだ。（パッとこういう制約の詳細がわかるというのは標準化された言語の強みだと感じる・・・）
let f = let x = ... in fun () -> x, ref []
の...部分にいろんな式を入れてref []の部分が全称化されるかどうかを調べればOCamlで何がsimple valueかはわかる。
というわけでOCamlでは実際に何が全称化されるかを試しながら、現在作っている型システム上でsimple valueかどうかを判定する関数を作成する。（前回言った通り、ここまで実装してきた型システムではvalue restrictionが必要になるほど機能が豊富ではないのだが、今後のことを見越してOCaml準拠なvalue restrictionを入れておく）
今回のコードはここ。
is_simple
式がsimple valueかどうかを判定する関数is_simple：
let rec is_simple = function
当然式に対してパターンマッチしている。
let f = let x = ... in fun () -> x, ref []に色々入れて試したところ、
| EVar _ | EUnit | ETrue | EFalse | EInt _ | EAbs _ -> true
と変数、Unit、真偽値、整数値、関数などはどのような場合であれ（例えば関数内でRefが定義されていたり、変数が外部のRefを指していたりしても）simple valueとして認識される。意外だったのは変数で、ここまで基本的な式でReal World OCamlのリストに載ってなかったので「まあrefを指してたりすることもあるだろうしsimple valueじゃないんだろう」と思いつつ調べたらsimple valueだった。
逆に
| EApp _ | ERef _ | EDeref _ | EAssign _ -> false
のように、関数適用、refの作成、deref、そしてrefへの代入などはsimple valueにならない。!(ref 0)などはsimple valueでもいいのでは？とも思うがこれでも全称化されなかった。
これ以外の式に関しては、それらにネストで保持される式がsimple valueかどうかで判定する。
その最たるものはlet式：
| ELet(_,e,ebody) -> is_simple e && is_simple ebody
変数を束縛する式、そして本体の式のどちらもsimple valueである必要がある。
If式：
| EIf(_,e1,e2) -> is_simple e1 && is_simple e2
If式は条件式はsimple valueでなくてもいいようで
let f = let x = if (let x = ref true in !x) then 1 else 2 in fun () -> (x, ref [])
が全称化されていた。1や2の部分（つまり結果になるところ）は両方simple valueである必要がある。
タプル、レコード、バリアントのコンストラクタ：
| ETuple es -> List.for_all is_simple es | ERecord les -> List.for_all is_simple (List.map snd les) | ETag(_,e,_) -> is_simple e
ネストで含まれている式すべてがsimple valueならsimple value。
タプル、レコード、バリアントに対してアクセスする式：
| ETupleAccess(e,_,_) | EProjection(e,_,_) -> is_simple e | ECase(e,cases,_) -> is_simple e && List.for_all (fun (_,_,e) -> is_simple e) cases
タプルやレコードの場合、インデックスやフィールド名でアクセスするがそのアクセスする元の式がsimple valueならsimple value。
バリアントにアクセスするためのパターンマッチについては、matchする対象の式と、すべてのケースの返す結果全部がsimple valueであることが条件。
再帰：
| EFix e -> is_simple e
OCamlでlet rec式を入れても問題なく全称化されたので、Fixの中身がsimple valueなら大丈夫そう。
Add, IsZero：
| EAdd(e1,e2) -> is_simple e1 && is_simple e2 | EIsZero e -> is_simple e
ここらへんは実はOCamlではsimple valueにはならない。ただの関数適用と認識されるからだろう。現在実装している言語ではこれらは特殊な構文を持っている（主に型システム開発の例として話の都合上）。なのでこれらについても「引数」がsimple valueならsimple valueだとみなすことができる。
以上ですべての式に関してsimple valueか判定できるようになった。
type_of
これを受けてtype_of関数を修正する：
let rec typeof env level = function ... | ELet(svar, e, ebody) -> let tvar = typeof env (level+1) e in let tgen = if is_simple e then generalize level tvar else tvar in typeof ((svar,tgen)::env) level ebody ...
let tgen =generalize level tvar inだったのがlet tgen = if is_simple e then generalize level tvar else tvar inになってis_simpleならgeneralize、違うならしない、というロジックになっている。
Let多相だとLet式のケースでしかgeneralizeが使われないので、この修正だけでvalue restrictionが実装できる。ただし実際の言語だと、最終的なプログラムでは全称化されていない型変数が型に出てきてはまずい（というか何を意味するのかわからない）ので、OCamlなどだとモジュール単位でこのような型変数がないか調べている。あったらそのモジュールはコンパイルできないのでプログラマが明示的に型注釈を書く必要がある。OCamlで型注釈をどうしても書かないといけない数少ないケースの一つである。
次回
次は再帰型を扱えるように型システムを拡張する予定。
