From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <weis@pauillac.inria.fr>
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39])
	by yquem.inria.fr (Postfix) with ESMTP id D8367BDCB
	for <caml-list@yquem.inria.fr>; Mon,  5 Sep 2005 14:26:17 +0200 (CEST)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j85CQHqS021395
	for <caml-list@yquem.inria.fr>; Mon, 5 Sep 2005 14:26:17 +0200
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 OAA23683 for <caml-list@pauillac.inria.fr>; Mon, 5 Sep 2005 14:26:16 +0200 (MET DST)
Received: from xproxy.gmail.com (xproxy.gmail.com [66.249.82.199])
	by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j85CQFJ3023624
	for <caml-list@inria.fr>; Mon, 5 Sep 2005 14:26:16 +0200
Received: by xproxy.gmail.com with SMTP id h26so1219801wxd
        for <caml-list@inria.fr>; Mon, 05 Sep 2005 05:26:15 -0700 (PDT)
DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws;
        s=beta; d=gmail.com;
        h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references;
        b=EqbY971Hzfq61xicN19zvnlgok5Ge0Ya4qXw6J6e0Zq+A/qkNDzGansDFdOGPQcHNgFFE9PS/BZrEEjcQKzbaBvt8xNfoxt+6td1dXl1p7K4cHjWrhd3SvYv6hQfv64lxeauB+u0HPZ/UQDdx8pnc8Nvl6oS+AcmYSdJXvytTmQ=
Received: by 10.70.9.15 with SMTP id 15mr44485wxi;
        Mon, 05 Sep 2005 05:26:15 -0700 (PDT)
Received: by 10.70.51.20 with HTTP; Mon, 5 Sep 2005 05:26:15 -0700 (PDT)
Message-ID: <4a708d205090505266800ae48@mail.gmail.com>
Date: Mon, 5 Sep 2005 14:26:15 +0200
From: Lukasz Stafiniak <lukstafi@gmail.com>
To: Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
Subject: Re: [Caml-list] Existential types
Cc: caml-list@inria.fr
In-Reply-To: <20050905.082839.104027887.garrigue@math.nagoya-u.ac.jp>
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Content-Disposition: inline
References: <4a708d205090412435bca9cb0@mail.gmail.com>
	 <20050905.082839.104027887.garrigue@math.nagoya-u.ac.jp>
X-Miltered: at concorde with ID 431C3969.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Miltered: at nez-perce with ID 431C3967.002 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)!
X-Spam: no; 0.00; lukasz:01 caml-list:01 existential:01 ocaml:01 pointers:01 one-way:01 subtyping:01 existential:01 subtyping:01 polymorphism:01 lukasz:01 ...:98 unsafe:01 jacques:01 exists:02 
X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.0 required=5.0 tests=RCVD_BY_IP autolearn=disabled 
	version=3.0.3

Nice to know, that this is a standard technique.

2005/9/5, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>:
> [...]
> And if this is not the case (i.e. implemented in ocaml but magic
> required), there is a serious risk that this is actually unsound.
> Remember that the function Obj.repr of type ['a -> Obj.t] is unsound,
> contrary to the intuition.
> Which leads to the rule of thumb: the only "safe" uses of  magic are
> when dealing with "unsafe" values (implemented in C.)

Yes, they are custom values wrapping pointers to C++ objects related
by inheritance.
>=20
> By the way, I'm not sure I would call this existantial quantification,
> as it is only one-way. This looks more like a simple form of
> subtyping.
>=20
I agree, it is by no means a constructive existential quantification,
and it is a simple form of subtyping based on polymorphism. The
similarity to <exists 'a. 'a t> may be misleading here.

Thank You,
Lukasz