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

[Jeff Meister <nanaki@gmail.com>]

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

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

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