読者です 読者をやめる 読者になる 読者になる

Relaxed value restriction (2. covariant と relaxed value restriction)

ocaml

前回の続きです。

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 なんてことは書けない。

軽く説明、書いてみて

論文を読んでみたけれど、最後の方は今の段階では読める気がしない。
論理学の知識が皆無すぎて、やってられない。

この前までvalue restrictionもマトモに知らなかったわけだけど、少しはRelaxed value restrictionについて理解できたかもしれない。ほかにもいろいろと学んでいかないと、OCamlではメリットであるはずの型システムに振り回されそうで怖い。

広告を非表示にする