Browse thread
Polymorphic recursion
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| 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
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
>
>