From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 23961BB91 for ; Thu, 27 Jan 2005 01:59:56 +0100 (CET) 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 j0R0xt6L027976 for ; Thu, 27 Jan 2005 01:59:55 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id BAA32216 for ; Thu, 27 Jan 2005 01:59:55 +0100 (MET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j0R0xrkn027968 for ; Thu, 27 Jan 2005 01:59:54 +0100 Received: from localhost (suiren [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.13.1/8.13.1) with ESMTP id j0R0xm3p014358; Thu, 27 Jan 2005 09:59:48 +0900 (JST) Date: Thu, 27 Jan 2005 09:59:24 +0900 (JST) Message-Id: <20050127.095924.76754666.garrigue@math.nagoya-u.ac.jp> To: daniel.buenzli@epfl.ch Cc: caml-list@inria.fr Subject: Re: [Caml-list] Phantom types and polymorphic variants From: Jacques Garrigue In-Reply-To: <6AFC6161-6FF6-11D9-ABDA-000393DBC266@epfl.ch> References: <6AFC6161-6FF6-11D9-ABDA-000393DBC266@epfl.ch> X-Mailer: Mew version 4.1.53 on Emacs 21.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable X-Miltered: at concorde with ID 41F83D0B.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 41F83D09.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 variants:01 epfl:01 well-typed:01 ocaml:01 checker:01 unification:01 annotation:01 unification:01 variance:01 coercions:01 polymorphic:01 abstract:01 define:01 jacques:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: From: Daniel B=FCnzli > Suppose I have the following (well-typed) definitions > = > > type tool =3D [`Spoon | `Fork] > > > > type 'a t =3D unit constraint 'a =3D [< tool] > > > > type 'a toolspec =3D unit constraint 'a =3D [< tool] > > > > let spoon : [< tool > `Spoon ] toolspec =3D () > > let fork : [< tool > `Fork ] toolspec =3D () > > > > let create : ([< tool ] as 'a) -> 'a t =3D fun t -> () > > let create' : ([< tool ] as 'a) toolspec -> 'a t =3D fun t -> () > = > I don't really understand why the type of the value returned by creat= e = > and create' differ : > = > > # create `Spoon;; > > - : [< Test.tool > `Spoon ] Test.t =3D () > > # create' spoon;; > > - : [< Test.tool ] Test.t =3D () > = > I expected the second value to have the same type as the first. The problem is that what you define here is not a phantom type. To behave properly, phantom types must be abstract types (or, in ocaml 3.09, private types). In particular, if they are simple type abbreviations, the type checker will expand them before unification, and the parameters will never be unified. This is why you get the type you gave as annotation, and nothing more. Even with normal sum types, unification would work, but variance information would allow to change the parameter through coercions, making it useless as phantom type. Jacques Garrigue