Re: [Caml-list] Use-site variance in OCaml

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2013/06/12, at 5:58, Jeff Meister <nanaki@gmail.com> wrote:

> This seems like a good compromise! However, it raises another question for me. I tried writing ro/wo as modules rather than classes, but my variance annotations are not accepted then. Specifically, I cannot write:
> 
> module RO : sig
>   type +'a t
>   val get : 'a t -> 'a
> end = struct
>   type 'a t = 'a ref
>   let get x = !x
> end
> 
> Aside from the extensibility of class ro, this module looks like an equivalent definition. Yet I cannot declare 'a to be covariant, even though the type t is abstract, and the only operation on t given in the signature is covariant in 'a. Could the same behavior of class ro be allowed for module RO?
> 
> If so, then it seems like we could have a module-level definition like: module [type] RO = struct include module [type of] RW with type +'a t end
> 
> But even without adding that syntax, could the language allow me to manually decompose the module definition of RW into RO and WO?

Unfortunately, the way variance is computed for abstract types is very different of the one for objects.
Currently, for an abstract type to be covariant, its implementation must be covariant.
This problem was discussed in my paper on relaxing the value restriction.

It would be interesting to find a good criterion for  allowing this kind of variance improvement, and prove it.
Note that it can be tricky, as abstraction interacts in subtle ways with the rest of the language.
	Jacques Garrigue