Date: Mon, 25 Jan 1999 16:06:25 +0100 (MET)
From: David Monniaux <monniaux@clipper.ens.fr>
To: Liste CAML <caml-list@inria.fr>
Subject: Musings on Obj.magic (Was: subtyping and inheritance)
In-Reply-To: <199901250008.BAA29432@miss.wu-wien.ac.at>
Here are some slightly off-thread remarks on Obj.magic and why it can be
good:
On Mon, 25 Jan 1999, Markus Mottl wrote:
> Nice example code! I don't know what "Obj.magic" does internally,
> but I believe it can do real black (= unintended) magic, too.
Obj.magic is defined as the identity from any type to any type. Its
semantics are highly dependent on the memory layout of OCaml, and you can
do nasty things like:
# (((Obj.magic A),(Obj.magic B)) : int*int);;
- : int * int = 0, 1
This depends on the fact that in an enumerated datatype, 0-ary
constructors are encoded exactly as integers are encoded. Thus the first
constructor is seen as 0, the second as 1...
Now there are some legitimate (ie non implementation-dependent) uses of
Obj.magic. First, its semantics are well-defined when there exists a proof
of well-typedness in a stronger type system than OCaml's. For instance,
programs exported from Coq may need to be manually patched by inserting
Obj.magic at some places. This has to do with the fact that Coq's typing
is impredicative while OCaml's is not.
Second, it's needed for the toplevel, for printing out values. The type
safety of the procedure that prints the value of the expression the user
has just input relies on the overall safety of the OCaml type checker and
the subject reduction property of OCaml. This means that if the
typechecker says "hey, it's an int*int" you can trust it and cast the
return value into a int*int using Obj.magic. Of course, you can see that
as well-typedness in a proof system that is powerful enough to certify
OCaml's typechecker.
Regards, D. Monniaux
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:18 MET