From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id UAA06333 for caml-redistribution; Mon, 25 Jan 1999 20:19:53 +0100 (MET)
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id QAA17212 for <caml-list@pauillac.inria.fr>; Mon, 25 Jan 1999 16:06:29 +0100 (MET)
Received: from nef.ens.fr (nef.ens.fr [129.199.96.12])
	by nez-perce.inria.fr (8.8.7/8.8.7) with ESMTP id QAA26723
	for <caml-list@inria.fr>; Mon, 25 Jan 1999 16:06:27 +0100 (MET)
Received: from clipper.ens.fr (clipper-gw.ens.fr [129.199.1.22])
          by nef.ens.fr (8.8.8/jtpda-5.1) with ESMTP id QAA17183
          for <caml-list@inria.fr>; Mon, 25 Jan 1999 16:06:26 +0100 (MET)
Received: from brick.ens.fr (monniaux@brick [129.199.129.13]) by clipper.ens.fr (8.8.7/jb-1.1)
	id QAA25673 for <caml-list@inria.fr>; Mon, 25 Jan 1999 16:06:26 +0100 (MET)
Received: from localhost (monniaux@localhost) by brick.ens.fr (8.8.7/jb-1.1)
	id QAA21511 for <caml-list@inria.fr>; Mon, 25 Jan 1999 16:06:25 +0100 (MET)
X-Authentication-Warning: brick.ens.fr: monniaux owned process doing -bs
Date: Mon, 25 Jan 1999 16:06:25 +0100 (MET)
From: David Monniaux <monniaux@clipper.ens.fr>
X-Sender: monniaux@brick.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>
Message-ID: <Pine.GSO.4.04.9901251554500.20816-100000@brick.ens.fr>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: weis

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