Re: [Caml-list] Polymorphic recursion

["Francois Maurel" <Francois.Maurel@normalesup.org>]

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
  in
  y

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.

François

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
>
>