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 D96EDD45F for ; Fri, 4 Nov 2005 14:19:47 +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 jA4DJlok014070 for ; Fri, 4 Nov 2005 14:19:47 +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 OAA01266 for ; Fri, 4 Nov 2005 14:19:47 +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 jA4DJkCe014067 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Fri, 4 Nov 2005 14:19:46 +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 jA4DJhHa027676 for ; Fri, 4 Nov 2005 14:19:43 +0100 (CET) Mime-Version: 1.0 (Apple Message framework v746.2) In-Reply-To: <20051101.092744.112578253.garrigue@math.nagoya-u.ac.jp> References: <20051029.092649.55723981.garrigue@math.nagoya-u.ac.jp> <20051101.092744.112578253.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed Message-Id: <4CB7BAE5-122C-4241-B744-F9D1F5F3D96D@free.fr> Content-Transfer-Encoding: quoted-printable From: Xavier Clerc Subject: Re: [Caml-list] Question about polymorphic variants Date: Fri, 4 Nov 2005 14:20:12 +0100 To: caml-list@inria.fr X-Mailer: Apple Mail (2.746.2) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-1.6 (imag.imag.fr [129.88.30.1]); Fri, 04 Nov 2005 14:19:43 +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 : 436B5FF2.000 on concorde : j-chkmail score : X : 0/20 1 X-Miltered: at concorde with ID 436B5FF3.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 436B5FF2.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 variants:01 inference:01 inference:01 arrays:01 val:01 abstr:01 ocaml:01 pointer:01 ocaml:01 initialized:01 compiler:01 patched:01 arrays:01 unboxed: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 1 nov. 05 =E0 01:27, Jacques Garrigue a =E9crit : > From: Xavier Clerc > >> I must admit that I don't grasp the link between the existence of a >> "top" type and the inference of a polymorphic type in the given >> examples. I would expect inference of 'a array in arrays example and >> 'a in "List.map (fun (x, y) -> x + 1)" and don't see in what >> circumstances such types would not be safe (modulo the array >> representation issue discussed above). >> Could you exhibit an example where such inference would be false/ >> unsafe ? > > Here is the concrete counter-example for top. It uses the (unsafe) Obj > module to produce a segmentation fault, but through an operation that > most people would suppose to be safe. > > # let l =3D [| Obj.repr 1.0 |];; > val l : Obj.t array =3D [||] > # l.(0) <- Obj.repr 1;; > Segmentation fault > > How does it relate to top? Essentially, every ocaml value is > represented by a fixed-size word, either an integer or a > pointer to a boxed representation. All Obj.repr does is return its > argument with type Obj.t, the type of all ocaml values, which we can > see as another name for top. So one could assume that Obj.repr is a > coercion to top. The trouble, as you can see here, is that Obj.t > itself appears to be unsafe. Here l is created as an array, =20 > initialized > with a float. This means that internally it will get a float array > representation. Now when we try to put an integer into it, it will try > to use the float array assignment operation, which attempts to > dereference the argument to get its float representation. This > naturally results in a segmentation fault. > As a result we can see here that one assumption in the above must be > false. Since the definition of Obj.repr is exactly that of a coercion > to top, this must mean that adding top to the type system is unsound. Thanks for your answer, I start to grasp how existence of "top" can =20 be related to related to my question. However, I must confess that I am still puzzled by the fact that your =20= example heavily rely on the actual representations of elements and =20 not only on their types. A question is still pending in my mind (in fact, always the same =20 question, reformulated to sound like I am making some progress) : if =20 the compiler(s) where patched to treat all arrays either as boxed or =20 as unboxed, would it be safe to get rid of the leading underscore in =20 the inferred type ? Equivalently, is the use of "top" (using Obj.repr and relatives) =20 unsafe only because of concrete representation or for theoretical =20 reason ? > >> Well, the only way to get rid of the leading underscore in inferred >> type is to "use" all the tags of the type (that is "converge" toward >> the upper bound of the variant), as in the following toplevel =20 >> 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 >> for mf as one can pass [`Off | `On] where [< `Off | `On] is waited >> (as [`tag1 | `tag2 ... | `tagn] is shorthand for [< tag1 | `tag2 ... >> | `tagn > tag1 | `tag2 ... | `tagn]). > > Certainly, as [`Off|`On] is an instance of [< `Off|`On]. > But [`Off] or [`On] are other possible instances of [< `Off|`On], so > the latter is more general. > By the way, you can get your intended type directly with a type > annotation. > # let mf =3D List.map (f : [`Off|`On] -> _);; > val mf : [ `Off | `On ] list -> int list =3D Of course. I am ashamed of my error. Xavier Clerc=