前回の終わりに

前述のとおり今回のコードはRefとLet多相の関係により型安全ではない。

と書いた。

しかしよくよく考えてみると、現在実装した型システムだと機能がギリギリなところで弱く、Let多相とRef型があるにもかかわらず型安全性は保たれている、ような気がする。

OCamlにおけるこの問題についてはReal World OCamlに詳しく書いてある：

dev.realworldocaml.org

以下のような関数を考えると：

let remember =
  let cache = ref None in
  (fun x ->
     match !cache with
     | Some y -> y
     | None -> cache := Some x; x)

今までの型推論コードだとrememberはgeneralizeされて多相な'a -> 'a型の関数になる（基本的に入力・出力としてはidと同じ）。ポイントはref Noneがそれ自体では型が定まらず、'a option ref型になっていることだ。

なので以下のコードは型検査を通ってしまう：

(remember 3, remember true)

しかし実行時エラー（あるいはセグフォ？）である。型検査では(int * bool)型だと認識されていたのに実行時には(bool * bool)になっている（OCamlのタプルの評価順は右から左へとなっているので）。

この問題を回避するためにgeneralizeできる式に制約をつける、というのがvalue restrictionなのだが・・・。これまで実装してきた型システムはref Noneに相当するような「パラメトリックな型を持つ式」が表現できない。なのでギリギリこの問題は避けているように思う。ただし今後型コンストラクタを実装してしまえばその限りではない、のでこのままvalue restrictionを導入していく。

value restriction

前述のとおり、うっかり多相なRefを作って型安全性を破壊するのを回避するために、generalizeで多相化する型に制約をかけるのがvalue restrictionだ。Let多相ではlet v = e in e2のeの部分の型にgeneralizeがかかるわけだが、このeがsimple valueと呼ばれる形であるかどうかでgeneralizeするかを決める。

Real World OCamlから引用すると：

The core of the value restriction is the observation that some kinds of expressions, which we’ll refer to as simple values, by their nature can’t introduce persistent mutable cells, including:

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

とのこと。この説明で重要なのは"including"という単語で、そこからわかる通りこのリストは完全なものではない。

じゃあどうすれば何がsimple valueか確認できるのか。

いろいろ調べていたらこのOCaml コンパイラのGitHubレポに対するIssueを見つけた：

github.com

以下のコードは多相化されるのに

# let f =
  ref 0;
  fun () -> ref 0, ref []
  ;;
val f : unit -> int ref * 'a list ref = <fun>

以下のコードは多相化されない

# let f =
  let now = ref 0 in
  fun () -> now, ref []
  ;;
val f : unit -> int ref * '_a list ref = <fun>

という話だ。

これはつまりlet now = ref 0 in fun () -> now, ref []はlet v = e in e2のeの部分（ref 0）がsimple valueではないからだ。

ということはlet f = let x = ... in fun () -> x, ref []の...にいろんな式を当てはめていけばどの式がsimple valueなのかを確認できる。

次回

長くなってきたので今回はここまで。次回はどの式がOCamlではsimple valueだと認識されているのかを調べた上で型推論のコードを更新する。

Arantium Maestum

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

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

value restriction

次回