From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id E4678BC0A for ; Wed, 4 Apr 2007 21:58:55 +0200 (CEST) Received: from smtp3-g19.free.fr (smtp3-g19.free.fr [212.27.42.29]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l34JwtTG016327 for ; Wed, 4 Apr 2007 21:58:55 +0200 Received: from [192.168.0.1] (rke75-3-82-229-183-156.fbx.proxad.net [82.229.183.156]) by smtp3-g19.free.fr (Postfix) with ESMTP id 4375A5E086; Wed, 4 Apr 2007 21:58:55 +0200 (CEST) Message-ID: <4614037E.6060709@inria.fr> Date: Wed, 04 Apr 2007 21:58:54 +0200 From: Alain Frisch User-Agent: Icedove 1.5.0.8 (X11/20061116) MIME-Version: 1.0 To: Roland Zumkeller Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Polymorphic recursion References: <6f9f8f4a0704030959l8ebb155g8532e3ee6d31c66d@mail.gmail.com> <4613C0AA.8010405@inria.fr> <4613C22E.5060206@inria.fr> In-Reply-To: X-Enigmail-Version: 0.94.0.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 4614037F.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; frisch:01 frisch:01 recursion:01 annotations:01 well-typed:01 coq:01 ocaml:01 type-checker:01 ocaml:01 runtime:01 endline:01 coq:01 ocamlopt:01 segfault:01 bug:01 Roland Zumkeller wrote: > The function can be checked in richer type systems with annotations > (e.g. Coq's), so we know that Obj.magic is not dangerous here. The fact that something is well-typed in Coq does not mean that you can just translate it to OCaml by adding a few Obj.magic to make the type-checker happy. OCaml programmers tend to have a rough mental picture of what the semantic of the Obj module is and what are the important properties of the runtime representation of values, but they often only see part of the picture. Do you know what the following piece of code does? let () = let x = if ("a" = "b") then Obj.magic 0 else String.copy "abc" in for i = 0 to 100000 do ignore (ref [1]) done; Gc.major (); print_endline x Well, if I knew Coq, I could prove that "a" is not equal to "b" and thus that x is always bound to a valid string. So the Caml code should print "abc". Right? No. This code compiled with ocamlopt produces a segfault on my machine. I remember spending hours (and wasting my boss' precious time) on a bug I introduced in some code because I thought that Obj.magic 0 and Obj.magic () are equivalent. The code above show that this is not the case (if you replace 0 with (), it works fine). If you don't understand what's going on, you'd better not use the Obj module. If you know why, there is probably some other dark corner which you don't understand and that will bite you some day. In the present case, we have good solutions that don't require Obj. Unless a strong case is made that performance is not adequate, there is really no reason to use Obj. -- Alain