やっとMLのrefが(たぶん)わかった人
よくわからないので、OCamlのソースを覗く。typing/printtyp.mlを見ると、
let non_gen_mark sch ty = if sch && ty.desc = Tvar && ty.level <> generic_level then "_" else ""
という関数があるので、ty.levelに多相か単相かが保存されていることがわかった。
しかし、これだけではしかたがないので、適当に論文を探すことにする。typing/typecore.mlとか読むのはさすがにしんどいので。
まず、大堀先生のRank1 Polymorphism論文を見る。すると、A. WrightのSimple imperative polymorphismというのが参照されているので、それを探す。ACMのWebページからどうたどれば良いかわからずてこずったが、最終的には(というかGoogleの4番目の検索結果にあった)手に入れることができた。
で、読む。*1
まず、既存の命令型プログラムの型付けの問題点について述べられている。例えばSMLだと、refは∀_α._α→_α refと型付けられている、とか*2 *3 *4。
そして、3章で「多相型をもてるのをsyntactic valueに限定すればいいじゃん」という話が出てくる。おおーーーvalue restrictionはここで導入されていたのか。知らなかった。95年か…意外と最近なんだな。ではvalueとは何か。いきなり
The precise definition of syntactic value is flexible.
と書かれていて、ちょっとぐんにゃりするがすぐ後にMLの話が出てきたので復活。MLではvalueは「定数」「変数」「ラムダ抽象」「型コンストラクタのvalueへの適用」らしい。さらにここで黒魔術を使って「refコンストラクタのいかなる適用もvalueではない」とする。そうするとあら不思議、いつの間にかよく知っている(？)MLの型システムが出来上がるというわけだ。
うーん、うまいなあ。なんで多相性をvalueに制限しようとか思いつくんだろう。すげー。
そこから先は、value restrictionでうまくいくことの主張とかがつらつら並んでいるような気がするので、省略。いまさらどうでもいいだろう(どうでも良くはないかもしれないけど、まあ私の興味はこれでOK)。
問題はここから先なんだが。とりあえず、OCamlでは「mutableなフィールドを含むレコードはvalueではない」で解釈できるような気がする。objectだと「mutableなフィールドはvalueではない」とでもなっているんだろうか。そこまで単純な話ではないような気がするけど。
というわけでやっとvalue restrictionが理解できた気がします。referenceが単相になるのと関数適用が単相になるのの関係がいまいち理解できなかったのですが、話が逆だったのですね。referenceを単相にしたいから関数適用を単相に制限する、と。少し納得。
