From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 31BCC7EE25 for ; Tue, 11 Jun 2013 22:58:14 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of nanaki@gmail.com) identity=pra; client-ip=209.85.212.46; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nanaki@gmail.com"; x-sender="nanaki@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of nanaki@gmail.com designates 209.85.212.46 as permitted sender) identity=mailfrom; client-ip=209.85.212.46; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nanaki@gmail.com"; x-sender="nanaki@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-vb0-f46.google.com) identity=helo; client-ip=209.85.212.46; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nanaki@gmail.com"; x-sender="postmaster@mail-vb0-f46.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvoAAIKOt1HRVdQujWdsb2JhbABZDgiDI0m+TnkIFg4BAQEBBwsLCRIGJIIjAQEDAQEnGQEbHQEDAQsGBQsNLiEBAREBBQEcBhOHegEDCQYMnGiMS4J/hEoKGScNWId0AQUMjEiCXgeDYAOJIIw5gWeMHoM/FimCWoEdXhw X-IPAS-Result: AvoAAIKOt1HRVdQujWdsb2JhbABZDgiDI0m+TnkIFg4BAQEBBwsLCRIGJIIjAQEDAQEnGQEbHQEDAQsGBQsNLiEBAREBBQEcBhOHegEDCQYMnGiMS4J/hEoKGScNWId0AQUMjEiCXgeDYAOJIIw5gWeMHoM/FimCWoEdXhw X-IronPort-AV: E=Sophos;i="4.87,847,1363129200"; d="scan'208";a="21390732" Received: from mail-vb0-f46.google.com ([209.85.212.46]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 11 Jun 2013 22:58:13 +0200 Received: by mail-vb0-f46.google.com with SMTP id 10so5597761vbe.33 for ; Tue, 11 Jun 2013 13:58:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=flbHo+HPx7BQfvN+J2JC/VZq+RjiDWt+Y4qZvOD5edY=; b=UHTy35pmZ9G3/7wcjXwMCX4Ufl1Ju5LaLPpveuhLCLkVs4K/URBEix/zyvfcNBuTxx +HVGSjExGA3SjZfL5oFEP1jo/6TU+zSp/aKnwYs9P9rQnlcmYEW42bkKjA/KghRFXzw+ OG6Fce4UxMHJHii3xqhx5OftzF0LX54Wx1ZhozaWN4j0L8fwdwxNWHiiAzZ8XDiPXxPy qVeiYQRWLsDxvtyQeq35dA62wN6fBwSz76gz4P3Q+h56lkQ07UAsM7xlKz+tcSyR0ico e1jDd7lyRvbgH+J7CPJbWy6mhAWUGP0TKsdwY1nNMs1YoYG3dZTiNY0SeuYi64DyJcES skug== MIME-Version: 1.0 X-Received: by 10.52.164.19 with SMTP id ym19mr7441444vdb.38.1370984292170; Tue, 11 Jun 2013 13:58:12 -0700 (PDT) Received: by 10.58.31.195 with HTTP; Tue, 11 Jun 2013 13:58:11 -0700 (PDT) In-Reply-To: <69F3B820-75C0-4EA1-B1AF-B70D276E4AEE@math.nagoya-u.ac.jp> References: <69F3B820-75C0-4EA1-B1AF-B70D276E4AEE@math.nagoya-u.ac.jp> Date: Tue, 11 Jun 2013 13:58:11 -0700 Message-ID: From: Jeff Meister To: Jacques Garrigue Cc: Caml List Content-Type: multipart/alternative; boundary=001a11c22b32ba459904dee727e0 Subject: Re: [Caml-list] Use-site variance in OCaml --001a11c22b32ba459904dee727e0 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable 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 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-20= 13.pdf), > and it occurred to me that OCaml might be able to express the same concep= ts. > > > > 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) =3D object > > val mutable v =3D init > > method get =3D v > > method set x =3D 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) =3D object val mutable v =3D init method get= =3D v > end > > class [-'a] wo (init : 'a) =3D object val mutable v =3D init method set= x =3D > v <- x end > > class ['a] rw init =3D object inherit ['a] ro init inherit! ['a] wo init > end > > [=85] > > > 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. Similarl= y, > -'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 =3D object ('self) inherit ['a] rw method eq : 's= elf > -> 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 =3D [+'a] rw > > or > > class type ['a] c =3D object > inherit [+'a] rw > method set x =3D {< v =3D 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 =3D struct type 'a t =3D 'a ref let get x =3D !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 =3D 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 --001a11c22b32ba459904dee727e0 Content-Type: text/html; charset=windows-1252 Content-Transfer-Encoding: quoted-printable
On S= at, Jun 8, 2013 at 12:05 AM, Jacques Garrigue <garrigue@math.na= goya-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 annotation= s in a Java-like language (http://www.cs= .cornell.edu/~ross/publications/mixedsite/mixed-site-tate-2013.pdf), an= d it occurred to me that OCaml might be able to express the same concepts.<= br> >
> If I have a type parameter that appears in both covariant and contrava= riant positions, then it is invariant, and OCaml will not allow me to annot= ate the parameter with + or -. For example, this class of mutable reference= s:
>
> class ['a] rw (init : 'a) =3D object
> =A0 val mutable v =3D init
> =A0 method get =3D v
> =A0 method set x =3D v <- x
> end
>
> This code will not compile with [+'a] or [-'a]. However, the c= lass can be (manually) decomposed into separate covariant and contravariant= parts:
>
> class [+'a] ro (init : 'a) =3D object val mutable v =3D init m= ethod get =3D v end
> class [-'a] wo (init : 'a) =3D object val mutable v =3D init m= ethod set x =3D v <- x end
> class ['a] rw init =3D object inherit ['a] ro init inherit! [&= #39;a] wo init end

[=85]

> So, it seems that the OCaml type checker knows which methods of my fir= st definition of 'a rw use 'a in a covariant or contravariant posit= ion. 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 de= clare any such type, or decompose his class manually. OCaml would automatic= ally select only those methods where 'a appears only in covariant posit= ions. Similarly, -'a rw would produce an object of type 'a wo.
>
> Is this feasible, or is the situation more complicated than I've d= escribed?

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 bein= g contravariant in the type of self
introduce some ambiguity in the meaning of "+":
=A0 =A0class type ['a] cell =3D object ('self) inherit ['a] rw = method eq : 'self -> bool end
In that case, =A0+'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, the= n I suppose my imagined expression might introduce more problems than it so= lves.
=A0
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 ver= y 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 wor= k on.
=A0
Also, an intermediate form seems possible too: rather than doing this on th= e fly inside coercions,
one could use it in declarations:

=A0 class type ['a] ro =3D [+'a] rw

or

=A0 class type ['a] c =3D object
=A0 =A0 =A0inherit [+'a] rw
=A0 =A0 =A0method set x =3D {< v =3D x >}
=A0 end

The change in syntax is much more modest: we just allow variance annotation= s 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 varia= nce annotations are not accepted then. Specifically, I cannot write:

module RO : sig
=A0 type +'a t
=A0 val get : 'a t -> &= #39;a
end =3D struct
=A0 type 'a t =3D 'a ref
=A0 let get = x =3D !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 operat= ion on t given in the signature is covariant in 'a. Could the same beha= vior of class ro be allowed for module RO?

If so, then it seems like we could have a module-level defin= ition like: module [type] RO =3D struct include module [type of] RW with ty= pe +'a t end

But even without adding that syntax, cou= ld the language allow me to manually decompose the module definition of RW = into RO and WO?
=A0
Jacques Garrigue
--001a11c22b32ba459904dee727e0--