多相関数と部分型と value restriction

http://d.hatena.ne.jp/eagletmt/20100716 を見ての感想ですが特に意味のあることを書いているわけではありません．
本来はコメント欄に書くべきことなのかもしれないですが，せっかく開設したのでこちらに書きます．
あと別に疑問に答えるとかそんな大層なもんではないです．すいません．

reference と subtyping

整数の型 Int と数字の型 Number の間には

Int <: Number

という部分型関係が成り立っているとすると，このとき

Int ref <: Number ref

という関係は成り立たない．逆に

ref Number <: ref Int

という関係も成り立たない．
ref Int の値を ref Number の場所で使うことを考えればすぐわかることだけど，
実は ref Int は ref Int 自身とだけ部分型関係を持つ．つまり ref Int に関して成り立つ部分型関係は

ref Int <: ref Int

だけということになる．
もちろんこれは Int と Number に限った話ではなく，

A <: B

という部分型関係にある任意の型でも成り立つ話．

ここら辺の情報は TaPL の Subtyping の章が詳しかったはず．

reference と polymorphic function

もちろん関数にも部分型のための規則はある．
が，多相関数(例えば id)とそれをインスタンス化した後の関数(例えば succ)に対しては部分型関係(のようなもの)が成り立つんじゃないかなあというのが今回思ったこと．
まあそのこと自体はインスタンス関係を表す記号 ≦ にもよく表われているし，単相関数を多相関数を(単相関数へインスタンス化できれば)置き換えるできることからもすぐわかると思う．

多相関数にも(本来の部分型関係とは違う)部分型ちっくな関係が成り立つのなら，それは reference に適用できそう．
例えば

let f x = x;;       (* f : ∀a.a->a *)
let r = ref f;;     (* r : ∀a.a->a ref *)
r := (+);;          (* ∀a.a->a ref ≠ int->int ref なのでエラー *)
r := (fun x -> x);; (* reference は参照している値の型とだけ部分型関係が成り立つので OK *)
let g = !r;;        (* g : ∀a.a->a *)

この制限を使うと，value restriction は必要なくなる(と思う)．

しかし，この場合リストのような多相的な type constructor を使うときに問題が起こる．

let l1 = ref [];;   (* ∀a.[a] ref *)
l1 := [1];;         (* エラー．l1 は ∀a.[a] という型の値しか代入できない *)
let l2 = 1::!l1;;   (* これは OK *)

特に2行目みたいな使い方ができないというのは参照を使う上ではけっこう大きな制限じゃないだろうか．
なので，ref で残った型変数は一般化せずに単相の型としておくという value restriction はけっこう妥当な解決策なのかなと思う．

# value restriction 近辺の議論は一昔前にけっこうあったそうなので，論文を調べれば色々出てきて面白そうだなーとか思ったり．
# 確か TaPL の Type Reconstruction の章に参考文献が載っていたような...


追記:
例が不適切だったのを修正