I was browsing ocaml's standard library, and came across this code in the map.ml file.
module type S =
sig
type key
type +'a t
val empty: 'a t'
I'm wondering why there is type +'a t
, and why the author use it instead of simply 'a t
.
Its behaviour is strange and I can't deduce the usage of it.
# type +'a t = 'a list;;
type 'a t = 'a list
# type +'a t = +'a list;;
Characters 13-14:
type +'a t = +'a list;;
^
Error: Syntax error
Thanks
To build up on Jeffrey's answer, the reason the developers did the work of marking the abstract type as covariant here is likely not to help you use subtyping (essentially nobody uses subtyping in OCaml, as parametric polymorphis is generally preferred), but to use an even-less-well-known aspect of the type system called the "relaxed value restriction", thanks to which covariant abstract types allow more polymorphism.
You may safely ignore those subtleties until, someday, you hit a problem with an abstract type of yours that is not as polymorphic as you would like, and then you should remember than a covariance annotation in the signature may help.
We discussed this on reddit/ocaml a few months ago:
Consider the following code example:
module type S = sig type 'a collection val empty : unit -> 'a collection end module C : S = struct type 'a collection = | Nil | Cons of 'a * 'a collection let empty () = Nil end let test = C.empty ()
The type you get for
test
is'_a C.collection
, instead of the'a C.collection
that you would expect. It is not a polymorphic type ('_a
is a monomorphic inference variable that is not yet fully determined), and you won't be happy with it in most cases.This is because
C.empty ()
is not a value, so its type is not generalized (~ made polymorphic). To benefit from the relaxed value restriction, you have to mark the abstract type'a collection
covariant:module type S = sig type +'a collection val empty : unit -> 'a collection end
Of course this only happens because the module
C
is sealed with the signatureS
:module C : S = ...
. If the moduleC
was not given an explicit signature, the type-system would infer the most general variance (here covariance) and one wouldn't notice that.Programming against an abstract interface is often useful (when defining a functor, or enforcing a phantom type discipline, or writing modular programs) so this sort of situation definitely happens and it is then useful to know about the relaxed value restriction.
If you want to understand the theory, the value restriction and its relaxation are discussed in the 2004 research article Relaxing the value restriction from Jacques Garrigue, whose first few page are a rather interesting and accessible introduction to the topic and main idea.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With