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