[Caml-list] Use-site variance in OCaml

[Jeff Meister <nanaki@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2270 bytes --]

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

I can always coerce from 'a rw to 'a ro or 'a wo, when I want to restrict
access to the reference as read-only or write-only. Those types will then
allow coercions that would not be permitted on 'a rw. For example, given
this pair of classes:

class super = object end
class sub = object method foo = () end

The compiler will accept (new ro (new sub) :> super ro) as well as (new wo
(new super) :> sub wo).

However, I didn't actually need to annotate the type parameters in my
definitions of 'a ro and 'a wo; OCaml would have inferred them. And these
coercions are all compile-time operations.

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?

[-- Attachment #2: Type: text/html, Size: 2696 bytes --]