Re: [Caml-list] Polymorphic recursion

[Alain Frisch <Alain.Frisch@inria.fr>]

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