From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id BBCA97EE25 for ; Sat, 8 Jun 2013 09:05:47 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqYAAJrWslGFBoIFnGdsb2JhbABZFoMjvwOBEQ4BAQEBAQgUCTyCIwEBAwEBJxwBNQIDCwsOJhIhNgYTh3sDCQUNqgqERgKEew1LiAAHjFuCKjMHgnthiSGMO4FnjB6IQg X-IPAS-Result: AqYAAJrWslGFBoIFnGdsb2JhbABZFoMjvwOBEQ4BAQEBAQgUCTyCIwEBAwEBJxwBNQIDCwsOJhIhNgYTh3sDCQUNqgqERgKEew1LiAAHjFuCKjMHgnthiSGMO4FnjB6IQg X-IronPort-AV: E=Sophos;i="4.87,827,1363129200"; d="scan'208";a="17190432" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 08 Jun 2013 09:05:44 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id DEC876391; Sat, 8 Jun 2013 16:05:41 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 9F11C396F; Sat, 8 Jun 2013 16:05:41 +0900 (JST) DomainKey-Signature: h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 513BC2564; Sat, 8 Jun 2013 16:05:41 +0900 (JST) Content-Type: text/plain; charset=windows-1252 Mime-Version: 1.0 (Mac OS X Mail 6.3 \(1503\)) From: Jacques Garrigue In-Reply-To: Date: Sat, 8 Jun 2013 16:05:40 +0900 Cc: Caml List Content-Transfer-Encoding: quoted-printable Message-Id: <69F3B820-75C0-4EA1-B1AF-B70D276E4AEE@math.nagoya-u.ac.jp> References: To: Jeff Meister X-Mailer: Apple Mail (2.1503) Subject: Re: [Caml-list] Use-site variance in OCaml 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-2013.pdf), and it occurred to me that OCaml might be able t= o express the same concepts. >=20 > If I have a type parameter that appears in both covariant and contravaria= nt positions, then it is invariant, and OCaml will not allow me to annotate= the parameter with + or -. For example, this class of mutable references: >=20 > class ['a] rw (init : 'a) =3D object > val mutable v =3D init > method get =3D v > method set x =3D v <- x > end >=20 > This code will not compile with [+'a] or [-'a]. However, the class can be= (manually) decomposed into separate covariant and contravariant parts: >=20 > 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? >=20 > 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 typ= e, or decompose his class manually. OCaml would automatically select only t= hose methods where 'a appears only in covariant positions. Similarly, -'a r= w would produce an object of type 'a wo. >=20 > Is this feasible, or is the situation more complicated than I've describe= d? 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 "+": class type ['a] cell =3D object ('self) inherit ['a] rw method eq : 'sel= f -> 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 th= e 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 annotation= s in the bracket, and we are sure that rw must be a class type. Jacques Garrigue=