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

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

On 2013/06/08, at 14:37, Jeff Meister <nanaki@gmail.com> wrote:

> I don't often use subtyping in OCaml, but I was recently reading a paper about a mixture of declaration-site and use-site variance annotations in a Java-like language (http://www.cs.cornell.edu/~ross/publications/mixedsite/mixed-site-tate-2013.pdf), and it occurred to me that OCaml might be able to express the same concepts.
> 
> If I have a type parameter that appears in both covariant and contravariant positions, then it is invariant, and OCaml will not allow me to annotate the parameter with + or -. For example, this class of mutable references:
> 
> class ['a] rw (init : 'a) = object
>   val mutable v = init
>   method get = v
>   method set x = v <- x
> end
> 
> This code will not compile with [+'a] or [-'a]. However, the class can be (manually) decomposed into separate covariant and contravariant parts:
> 
> class [+'a] ro (init : 'a) = object val mutable v = init method get = v end
> class [-'a] wo (init : 'a) = object val mutable v = init method set x = v <- x end
> class ['a] rw init = object inherit ['a] ro init inherit! ['a] wo init end

[…]

> So, it seems that the OCaml type checker knows which methods of my first definition of 'a rw use 'a in a covariant or contravariant position. Would it be possible to implement use-site variance in OCaml based on this?
> 
> I'm imagining an expression like (new rw 0 :> +'a rw) that would give an object of type 'a ro, without the programmer having to declare any such type, or decompose his class manually. OCaml would automatically select only those methods where 'a appears only in covariant positions. Similarly, -'a rw would produce an object of type 'a wo.
> 
> Is this feasible, or is the situation more complicated than I've described?

This is technically doable.
Maybe the most painful part would be to extend the syntax to allow variance annotations inside type expressions.
Also, OCaml and Java differ in that OCaml allows binary methods, which being contravariant in the type of self
introduce some ambiguity in the meaning of "+":
   class type ['a] cell = object ('self) inherit ['a] rw method eq : 'self -> bool end
In that case,  +'a cell could either keep only method get, or only eq, but keeping both would be invariant.

And as always the question is rather how useful it would be in practice.

Also, an intermediate form seems possible too: rather than doing this on the fly inside coercions,
one could use it in declarations:

  class type ['a] ro = [+'a] rw

or

  class type ['a] c = object
     inherit [+'a] rw
     method set x = {< v = x >}
  end

The change in syntax is much more modest: we just allow variance annotations in the bracket, and we are sure that rw must be a class type.

Jacques Garrigue