前回の続きです。
Value restrictionによって
let x = fst ([], ()) val x : '_a list = []
となってしまっていた。うん、非常に残念。これは別に多相的にあつかってもいいはず。
Relaxed value restriction
ここで、Relaxed value restriction。
これはValue restrictionなんだけど、そのときに単相が多相の部分型になっているときには多相にする。（covariantな位置にのみ出現する単相型を多相型にする。）
covariantについて（補足）
covariantな型とは、ざっくりいうと関数の->の右側に現れる型。（'a -> 'b なら、'bがcovariant。さらに'aはcontravariantと呼ばれる。）で、OCamlのプリミティブ型の中でも、'a list や 'a lazy_t はパラメタ 'a がcovariantだけど、'a ref はパラメタである 'a がcovariantでない。また、type 'a t もcovariantではない。ただし、OCamlでtype +'a t はcovariant。ちなみに type -'a t ではcontravariantにできる。
コレを使って、先ほどの例をOCaml上で試してみます。
# type (-'a, +'b) t = 'a -> 'b;; type ('a, 'b) t = 'a -> 'b # type (-'a, 'b) t = 'b -> 'a;; Error: In this definition, expected parameter variances are not satisfied. The 1st type parameter was expected to be contravariant, but it is covariant # type (+'a, 'b) t = 'a -> 'b;; Error: In this definition, expected parameter variances are not satisfied. The 1st type parameter was expected to be contravariant, but it is covariant # type (-'a, +'b) t = 'a * 'b;; Error: In this definition, expected parameter variances are not satisfied. The 1st type parameter was expected to be contravariant, but it is covariant # type (+'a, +'b) t = 'a * 'b;; type ('a, 'b) t = 'a * 'b # type +'a t = 'a list;; type 'a t = 'a list # type +'a t = 'a lazy_t;; type 'a t = 'a lazy_t # type +'a t = 'a ref;; Error: In this definition, expected parameter variances are not satisfied. The 1st type parameter was expected to be covariant, but it is invariant # type -'a t = 'a ref;; Error: In this definition, expected parameter variances are not satisfied. The 1st type parameter was expected to be contravariant, but it is invariant # type +'a t = A of 'a | B of 'a;; type 'a t = A of 'a | B of 'a # type -'a t = A of 'a | B of 'a;; Error: In this definition, expected parameter variances are not satisfied. The 1st type parameter was expected to be contravariant, but it is covariant
関数の->の右にcontravariantは現れることができず、また左にcovariantが現れることもできない。
さらにプリミティブ型でのcovariant、not covariantも見える。
さらに、covariantでなければcontravariantであるわけでもない。 'a ref の部分を見れば分かるけれど、invariant（不変）というのがある。
relaxed value restriction
Relaxed value restrictionについて、ここでは軽く例を挙げて見ていくことにします。
Constructor
例えばValue restrictionの最後で出した例。
let x = fst ([], ())
これは結果として
val x : '_a list = []
でした。
ですが、'a list においてはcovariantなパラメタを持つので、Relaxed value restrictionでは上記の例は 'a list となります。
let x = fst ([], ()) val x : 'a list = []
だからもちろん
let x = fst (ref [], ())
は 'a ref になんかならない。無理。
抽象データ型
次のモジュールを考える。（処理には何ら意味はないので、type 'a t に注目してほしい。）
module Foo : sig type 'a t val foo : int -> int * 'a t end = struct type 'a t = 'a list let foo x = (x, []) end
ここで、次のようにFoo.foo を呼び出すことにしましょう。
Foo.foo 1
さて、この式の型はいったいどうなるのか。
- : int * '_a Foo.t = (1, <abstr>)
内部的には 'a list で 'a はどう見てもcovariantだけど、シグネチャ的にはcovariantには見えないので単相になる。
だから、ここでcovariantにしよう。
module Foo : sig type +'a t val foo : int -> int * 'a t end = struct type 'a t = 'a list let foo x = (x, []) end
そうすれば、
Foo.foo 1 - : int * 'a Foo.t = (1, <abstr>)
となる。
もちろん、'a Foo.t はcovariantなパラメタしか受け付けないので、struct ... end 内で type 'a t = 'a ref なんてことは書けない。
