From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 2D981D45F for ; Mon, 31 Oct 2005 18:08:09 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j9VH88QO011392 for ; Mon, 31 Oct 2005 18:08:08 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA15240 for ; Mon, 31 Oct 2005 18:08:07 +0100 (MET) Received: from imag.imag.fr (imag.imag.fr [129.88.30.1]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j9VH87gv011389 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Mon, 31 Oct 2005 18:08:07 +0100 Received: from [147.171.255.214] (mac-clerc.imag.fr [147.171.255.214]) by imag.imag.fr (8.13.0/8.13.0) with ESMTP id j9VH85N9011222 for ; Mon, 31 Oct 2005 18:08:05 +0100 (CET) Mime-Version: 1.0 (Apple Message framework v734) In-Reply-To: <20051029.092649.55723981.garrigue@math.nagoya-u.ac.jp> References: <589B1E9E-D4EC-4E03-9375-30670ED82BEB@free.fr> <20051028.205957.68033883.garrigue@math.nagoya-u.ac.jp> <20051029.092649.55723981.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed Message-Id: Content-Transfer-Encoding: quoted-printable From: Xavier Clerc Subject: Re: [Caml-list] Question about polymorphic variants Date: Mon, 31 Oct 2005 18:08:34 +0100 To: caml-list@inria.fr X-Mailer: Apple Mail (2.734) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-1.6 (imag.imag.fr [129.88.30.1]); Mon, 31 Oct 2005 18:08:05 +0100 (CET) X-IMAG-MailScanner: Found to be clean X-IMAG-MailScanner-Information: Please contact the ISP for more information X-j-chkmail-Score: MSGID : 43664F77.000 on concorde : j-chkmail score : X : 0/20 1 X-Miltered: at concorde with ID 43664F78.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43664F77.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 variants:01 type-related:01 arrays:01 unboxed:01 coerced:01 ocaml:01 polymorphism:01 inference:01 inference:01 arrays:01 variants:01 compiler:01 subtype:01 trivial:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 Le 29 oct. 05 =E0 02:26, Jacques Garrigue a =E9crit : [...] >> In this counter-example, it is not clear to me whether the possible >> problem is type-related or runtime-related. I mean, would this >> counter-example still hold if arrays were both boxed or both =20 >> unboxed ? >> > > No, the difference in representation is essential here. > > But at the type level, this problem can be expressed a bit > differently: whether it is safe to add a "top" to the type system, > allowing any type to be coerced to it. While some languages might > allow that, there is no fundamental reason it should be so (an this is > indeed not the case in ocaml.) > If we cannot assume the existence of such a type, then we cannot prove > that polymorphism in this case would be safe. I must admit that I don't grasp the link between the existence of a =20 "top" type and the inference of a polymorphic type in the given =20 examples. I would expect inference of 'a array in arrays example and =20 'a in "List.map (fun (x, y) -> x + 1)" and don't see in what =20 circumstances such types would not be safe (modulo the array =20 representation issue discussed above). Could you exhibit an example where such inference would be false/=20 unsafe ? >>> Actually, since this counter-example wouldn't apply to the above =20 >>> case >>> of polymorphic variants, this would probably be safe to leave the >>> polymorphic variant type as polymorphic... >>> >> >> Does this mean that inferring "[< `Off | `On] list -> int list" would >> be perfectly safe in the example above ? >> (by saying so, I am not pleading for any compiler change, I am just >> trying to organize my thoughts) >> > > I believe so, but I don't have a proof ready for that. > One way to do it would be to prove that any instance of [< `Off | `On] > is a subtype of [ `Off | `On ], which sounds trivial in this case. > So I would say this should apply to both [< ... ] types (closed > polymorphic variants, including the [< ... > ...] case) and <...; ..> > types (extensible object types.) But not to [> ...] types (open > polymorphic variants.) Well, the only way to get rid of the leading underscore in inferred =20 type is to "use" all the tags of the type (that is "converge" toward =20 the upper bound of the variant), as in the following toplevel session : # let f =3D function | `Off -> 0 | `On -> 1;; val f : [< `Off | `On ] -> int =3D # let mf =3D List.map f;; val mf : _[< `Off | `On ] list -> int list =3D # mf [`On];; - : int list =3D [1] # mf;; - : _[< `Off | `On > `On ] list -> int list =3D # mf [`Off];; - : int list =3D [0] # mf;; - : [ `Off | `On ] list -> int list =3D Does this mean that [`Off | `On] list -> int list could be inferred =20 for mf as one can pass [`Off | `On] where [< `Off | `On] is waited =20 (as [`tag1 | `tag2 ... | `tagn] is shorthand for [< tag1 | `tag2 ... =20 | `tagn > tag1 | `tag2 ... | `tagn]). I apologize for my questions if they are trivial but I must confess =20 that I am having a hard time understanding the subtleties of =20 polymorphic variants. Xavier Clerc=