On Sat, Jun 8, 2013 at 12:05 AM, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
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.

Ahh good point, I hadn't considered that. If there's ambiguity, then I suppose my imagined expression might introduce more problems than it solves.
 
And as always the question is rather how useful it would be in practice.

Indeed, I'm not necessarily proposing to add new features to OCaml for something I probably wouldn't use very often. If it's an easy extension, then it might be a neat addition to OCaml's object system that many other languages don't support. But my interest came out of curiosity, not a practical need for the code I work on.
 
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.

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?
 
Jacques Garrigue