皆さん、いかがお過ごしでしょうか。楽しいOCamlライフ送ってますか？
私は紆余曲折あって「なぜだ・・・なぜ自分が使っている型システムすら知らないんだ！？」ということで、OCamlの型システムを勉強しようと思ってます。そのあたりで論理学の知識がどうしても必要そうなのでやります。とはいえ、そんなに踏み込んで勉強しているわけじゃないのであしからず。
そんな中でも気になっていたのが、Relaxed value restriction。
Value restrictionで失われた多相性を型代数を変えずにサブタイピングに基づいてその一部を復活させるものなのだそう。
気になった理由は、covariant、contravariantとabstract datatypeの関係から多相・単相になる理由が全然理解できてなかった点。いくらなんでも流石に知らなさすぎるな、と思ってしまいました。
今回は勉強がてら記事としてその内容をまとめつつ書いていこうと思ってます。ちなみに私の駄文ではなくもっと正確で詳細な内容は http://www.math.nagoya-u.ac.jp/~garrigue/papers/index.html の「Relaxing the value restriction.」を参照してください。この記事の内容はリンク先に書いてあること以下であっても、以上にはなり得ません。また勉強中の内容をまとめたものであるため、正確性を欠いた文章となることもあるかもしれません。その点を理解して以下を読みましょう。
let polymorphism（let多相性） と Value restriction
Relaxed Value restrictionについてですが、その前に前提知識として必要なlet polymorphismとValue restrictionについて書きます。
Value restrictionはML系言語で用いられているlet polymorphismの問題を回避するための方法です。
let polymorphism
let polymorphismはlet-binding（let-束縛）によってbindされた変数・関数が多相的に扱えるようにするためのものです。例えば、つぎのようにletによるbindingを行います。（ここでのlet-bindingは、value restrictionがないものとしています。）
let x = []
これは次のように多相的に解釈されます。
val x : 'a list = []
いいですね。多相的に扱えるんですから、問題ないですよね。
先の多相型では 'a という型変数が生成されています。let polymorphismでは型を解決した結果、最終的に型が決定されない変数の型として型変数を生成します。
∀a.(a list)
ってことです。分からない人は、「最終的に決定できない型を型変数として生成する」とだけ考えましょう。
ここまではいいでしょう。
では次のような場合にはどうなるでしょうか。
let x = ref [] val x : 'a list ref x := 1 :: !x; x - : ?
一つ目のlet束縛についての型は（OCamlではこうはなりませんが）いいでしょう。
では二つ目の式の型はどうなるでしょうか。
- : 'a list ref
となるはずです。
ではこのまま処理を続けましょう。
let y = hd !x val y : 'a let z = (function true -> false | false -> true) y val z : ?
さて、これはどうなるでしょうか？
一見、型チェック時のエラーになりそうですがそうはなりません。
理由としては変数x の型が 未だに型変数を含む多相型であるからです。
そのため、これはランタイムエラーとなるでしょう。
value restriction
ここでこの問題をいかに回避するか、ということになります。
多相型を全部消し去ってしまうのも一つの方法ですが、できれば多相型を残しつつ解決したいですよね。
そこでML系の言語で使われているのがvalue restrictionです。
これは「型変数を生成するのは、(syntacticな)値である(non-expansiveな)ときのみであり、値でない(expansiveである)ような場合は生成しない」ということです。分かりにくい場合は「右辺が値であるときは型変数を生成する」と思っておきましょう。
では先ほどの ref を用いた例のどこがどう変わるのかを見ていきましょう。
実はすぐに変化する場所があります。
let x = ref [] val x : '_a list ref
OCamlのコードを書いたことがある人ならすぐに分かりますが、一番最初の ref [] の時点で異なります。参照型で保持される型で決定できない型が存在する場合には未決定の単相型が与えられます。（正確には現在のOCamlの場合、Relaxed value restrictionが働いても'a refの'aはcovariantでないために単相型になる。これについての詳細は次回記述する。）これにより、
x := 1 :: !x; x val - : int list ref
となり、以降も x の型は int list ref として扱われるようになります。
しかし、先ほどのvalue restrictionを行うと、次のようなコードでもnon-expansive（右辺が値）でないので多相的に振る舞うことができなくなって、型エラーを起こすことになってしまいます。
let f = List.find (fun x -> true) let n = f [1] let m = f ["1"] (* type error *)
これを解決するには、次のようにnon-expansiveとなるようにすればよい。
let f y = List.find (fun x -> true) y
これはη-展開と呼ばれるものです。（詳しくはラムダ計算を調べよう！）
で、ここからがrelaxed に続く話。
たとえば次のようなものは右辺が値じゃない。つまり単相になる。
let x = fst ([], ()) val x : '_a list = []
おおぅ。。。
ではコレ、実際のOCaml（3.07以降で。実際に3.07は触ってないので文献の記述による）ではどうなっているかというと
let x = fst ([], []);; val x : 'a list = []
きちんと多相型となっている。これはRelaxed value restrictionのおかげ。
一応ここまでは（おそらく）理解できているので、ここまで書いておきます。次回でちゃんとRelaxed value restrictionを説明できるようにしておきたい。
>go to 次回
