[Caml-list] Use-site variance in OCaml

[Caml-list] Use-site variance in OCaml

[Jeff Meister]

[-- 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 --]

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

[Jacques Garrigue]

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

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

[Jeff Meister]

[-- 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 --]

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

[Jacques Garrigue]

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