let-polymorphism と value restriction

について，現時点での自分の理解をまとめておく．
ML 系言語での話．

let-polymorphism とは

let によって束縛されたものが多相的に振舞えるためのもの．

let twice = fun f x -> f (f x)
let a = twice (fun x -> x + 1) 0
let b = twice not true

このような式の型を普通にチェックしていくと，まず twice の定義から twice : (a -> a) -> a -> a となる．
次の a の右辺で twice : (int -> int) -> int -> int に決定し，b の右辺をチェックするときに型エラーとなってしまう．
そこで，twice : (a -> a) -> a -> a となった後，残った型変数を generalize して ∀a. (a -> a) -> a -> a というような型とし，a の右辺では twice : (int -> int) -> int -> int に instantiate し，b の右辺では twice : (bool -> bool) -> bool -> bool に instantiate することで，この式を型付けできる．

(fun id -> (id true, id 0)) (fun x -> x)

はできないのに，

let id = fun x -> x in (id true, id 0)

はできるのは，まさに let-polymorphism のおかげなのだ．

let-polymorphism の問題点

しかし，twice のように型変数が残った場合に無条件でそれを generalize すると問題が生じる．
具体的には ref 型だ．

let r = ref (fun x -> x)
let f = r := (fun x -> x + 1); !r
let g = r := not; !r

これについて考えてみると，まず r の右辺を見て r : (a -> a) ref とわかり，型変数が残っているのでこれを generalize して r : ∀a. (a -> a) ref となる．
次の f においては r : (int -> int) ref に instantiate され，g においては r : (bool -> bool) ref に instantiate されるので型付けされる．
しかし実際には，f の時点で r には (int -> int) な関数が格納されており，g の時点で (bool -> bool) な関数が格納されるので問題がある．
これを回避するにはどうすればいいか．
右辺が ref 型かどうかは実行前にわかるので，ref 型の場合は generalize しないようにするだけでいいのだろうか．

次に

let f = fun x -> let r = ref x in fun y -> let t = !r in r := y; t
let g = f (fun x -> x)
let h = g (fun x -> x + 1)
let i = g not

について考えてみる．
f の右辺から f : a -> a -> a がわかり，ref 型ではないので generalize され f : ∀a. a -> a -> a となる．
ここまででは問題無い (f はたしかに多相的に振舞える) が，次の g において f : (a -> a) -> (a -> a) -> a -> a に instantiate されて g : (a -> a) -> a -> a となり，ref 型ではないので generalize されて g : ∀a. (a -> a) -> a -> a となってしまう．
こうなると，h の束縛も i の束縛も型付けされてしまうが，1つ上の例と実質的に同じ状況であり，問題がある．

value restriction

実際の OCaml 等の ML 系言語の処理系においては value restriction が採用されている．
value restriction とは，let-polymorphism において型変数を generalize するのは右辺が「値」であるときに限る，というものである．
ref (fun x -> x) も f (fun x -> x) も値ではないので，これらを束縛したときは型変数を generalize しないようになっている．
以下は ocaml 3.11.2 での例．

# let f = fun x -> let r = ref x in fun y -> let t = !r in r := y; t;;
val f : 'a -> 'a -> 'a = <fun>  (* 右辺は値なので generalize されている *)
# let g = f (fun x -> x);;
val g : ('_a -> '_a) -> '_a -> '_a = <fun>  (* 右辺は値ではないので generalize されていない *)
# let h = g (fun x -> x + 1);;
val h : int -> int = <fun>
# g;;
- : (int -> int) -> int -> int = <fun>
# let i = g not;;
Error: This expression has type bool -> bool
       but an expression was expected of type int -> int

しかしこの制限はかなり大雑把な制限である．
value restriction の下では

let f = List.map (fun x -> x)
let a = f [0]
let b = f [true]

が型エラーとなってしまう．
実際にはこの f は多相的に振る舞っても問題はない．
ちなみに，

let f = fun l -> List.map (fun x -> x) l

のように定義してやれば，f は多相的な型を持つ．

疑問点

ref 型がなければ，value restriction は必要無いのだろうか．

Haskell では

実際，ref 型の無い Haskell においては value restriction は存在しないように思う．

let f = map id
let a = f [0]
let b = f [True]

は問題無く型付けされる．

STRef や IORef は

Haskell で参照を扱うときこれらを使うことになるが，まず STRef で上の例を入力してみると

> let f = \x -> runST $ do { r <- newSTRef x; return (\y -> runST $ do { t <- readSTRef r; writeSTRef r y; return t })}

<interactive>:1:71:
    Couldn't match expected type `s' against inferred type `s1'
      `s' is a rigid type variable bound by
          the polymorphic type `forall s. ST s a' at <interactive>:1:14
      `s1' is a rigid type variable bound by
           the polymorphic type `forall s1. ST s1 a1' at <interactive>:1:58
      Expected type: ST s a2
      Inferred type: ST s1 a2
    In a stmt of a 'do' expression: t <- readSTRef r
    In the second argument of `($)', namely
        `do { t <- readSTRef r;
              writeSTRef r y;
              return t }'

というエラーがでる．
r は1つ目の ST s モナドにおける STRef s a 型であり，2つ目の ST s1 モナドでの STRef ではないからだ (たぶん)．

一方 STRef の代わりに IORef を使い，runST の代わりに unsafePerformIO を使うようにしてみると

> let f = \x -> unsafePerformIO $ do { r <- newIORef x; return (\y -> unsafePerformIO $ do { t <- readIORef r; writeIORef r y; return t })}
f :: forall a. a -> a -> a

と型付けされる．
この状態で

> let g = f id
g :: forall a. (a -> a) -> a -> a
> let h = g (+1)
h :: Integer -> Integer
> let i = g not
i :: Bool -> Bool

なんて定義して，h 0 の後に i True とかやると bus error となる．

unsafePerformIO を使うと unsafeCoerce を書ける，ということを思い出したりした．
http://www.tom.sfc.keio.ac.jp/~sakai/w3ml/w3ml.cgi/haskell-jp-2/msg/283