English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Polymorphic recursion
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-04-05 (09:46)
From: Francois Maurel <Francois.Maurel@n...>
Subject: Re: [Caml-list] Polymorphic recursion
About unintuitive - and, of course, strongly implementation dependent
- Obj.magic stuff, one can also patch your example into:

let magic x =
  let y =
    Obj.magic x

let () =
  let x = if ("a" = "b") then magic 0 else String.copy "abc" in
 for i = 0 to 100000 do ignore (ref [1]) done;
  Gc.major ();
 print_endline x

which is somehow "correct".

The version
let magic x =
  Obj.magic x

is not.


On 04/04/07, Alain Frisch <Alain.Frisch@inria.fr> wrote:
> 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
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs