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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 9BDFB7EE25 for ; Sat, 8 Jun 2013 07:37:36 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of nanaki@gmail.com) identity=pra; client-ip=209.85.220.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="nanaki@gmail.com"; x-sender="nanaki@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of nanaki@gmail.com designates 209.85.220.180 as permitted sender) identity=mailfrom; client-ip=209.85.220.180; receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-vc0-f180.google.com) identity=helo; client-ip=209.85.220.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="nanaki@gmail.com"; x-sender="postmaster@mail-vc0-f180.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Am4DAOvBslHRVdy0lWdsb2JhbABZFoMjSa9Zj1YIFg4BAQEBBw0JCRIqgihCARseAxIJB10BEQEFASIbh3IBAw8MnAOCfoxKgn+ELwoZJw1Yh3QBBQyTDwOJII4gj10WKYRVHA X-IPAS-Result: Am4DAOvBslHRVdy0lWdsb2JhbABZFoMjSa9Zj1YIFg4BAQEBBw0JCRIqgihCARseAxIJB10BEQEFASIbh3IBAw8MnAOCfoxKgn+ELwoZJw1Yh3QBBQyTDwOJII4gj10WKYRVHA X-IronPort-AV: E=Sophos;i="4.87,827,1363129200"; d="scan'208";a="17185169" Received: from mail-vc0-f180.google.com ([209.85.220.180]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Jun 2013 07:37:35 +0200 Received: by mail-vc0-f180.google.com with SMTP id gf11so1233362vcb.39 for ; Fri, 07 Jun 2013 22:37:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:date:message-id:subject:from:to:content-type; bh=FKaa96K+j0OWQN+SVF66x9qguv7YWthA4sCDeinxILg=; b=d0KZxCyRsT6MA4HiYzf0mS6DzNw7SbTV+E3oXNMVf85MxZudHixctdG6YjbA0guNl5 pd7yvHimn0qUFJrg3R6As2fTDMLKOcCO3JzxqO4OtsnDhv2cUMRkAEl0pTy4+/pmeEMb Pc8v7W4gNbKCF/UKNqNhYW6cCZgNS7LM7he+fa45BiGSkmBafruqI71ACdYLeeMxo8XC mcvQ9I7TN9YZvp5KShn7IPJ0UsoNPlBCuWNRbljlycFGGbmrY8GH/5Kuun1W0GFpfix0 u1RyEnN58EFSwskT0gLzvCK5H0YujvYbjsHa8atiaqk8QJI5Mu8GkEVkqtI3mj40p2mp o5kQ== MIME-Version: 1.0 X-Received: by 10.58.233.173 with SMTP id tx13mr812265vec.31.1370669854592; Fri, 07 Jun 2013 22:37:34 -0700 (PDT) Received: by 10.58.228.67 with HTTP; Fri, 7 Jun 2013 22:37:34 -0700 (PDT) Date: Fri, 7 Jun 2013 22:37:34 -0700 Message-ID: From: Jeff Meister To: Caml List Content-Type: multipart/alternative; boundary=089e0122ead4c9cc5d04de9df10a Subject: [Caml-list] Use-site variance in OCaml --089e0122ead4c9cc5d04de9df10a Content-Type: text/plain; charset=ISO-8859-1 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? --089e0122ead4c9cc5d04de9df10a Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
I don't often use subtyping in OCaml, but I = was recently reading a paper about a mixture of declaration-site and use-si= te variance annotations in a Java-like language (http://ww= w.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 concep= ts.

If I have a type parameter that appears in both covariant and con= travariant positions, then it is invariant, and OCaml will not allow me to = annotate the parameter with + or -. For example, this class of mutable refe= rences:

class ['a] rw (init : 'a) =3D object
=A0 val mutable v =3D i= nit
=A0 method get =3D v
=A0 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 contra= variant parts:

class [+'a] ro (init : 'a) =3D object val mutable v =3D init me= thod get =3D v end
class [-'a] wo (init : 'a) =3D object val mut= able 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

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-onl= y. Those types will then allow coercions that would not be permitted on = 9;a rw. For example, given this pair of classes:

class super =3D object end
class sub =3D object method foo =3D () en= d

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 definiti= ons of 'a ro and 'a wo; OCaml would have inferred them. And these c= oercions are all compile-time operations.

So, it seems that the OCaml type checker knows which methods of my firs= t definition of 'a rw use 'a in a covariant or contravariant positi= on. Would it be possible to implement use-site variance in OCaml based on t= his?

I'm imagining an expression like (new rw 0 :> +'a rw) that w= ould give an object of type 'a ro, without the programmer having to dec= lare any such type, or decompose his class manually. OCaml would automatica= lly select only those methods where 'a appears only in covariant positi= ons. Similarly, -'a rw would produce an object of type 'a wo.

Is this feasible, or is the situation more complicated than = I've described?
--089e0122ead4c9cc5d04de9df10a--