From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id DAA08867; Fri, 27 Aug 2004 03:28:40 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 DAA08388 for ; Fri, 27 Aug 2004 03:28:38 +0200 (MET DST) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id i7R1SYxR007220 for ; Fri, 27 Aug 2004 03:28:37 +0200 Received: from localhost (suiren.kurims.kyoto-u.ac.jp [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.9.3p2-20030924/3.7W) with ESMTP id KAA00687; Fri, 27 Aug 2004 10:28:27 +0900 (JST) Date: Fri, 27 Aug 2004 10:28:27 +0900 (JST) Message-Id: <20040827.102827.50023947.garrigue@kurims.kyoto-u.ac.jp> To: bpr@artisan.com Cc: caml-bugs@pauillac.inria.fr, caml-list@inria.fr Subject: [Caml-list] Re: OCaml typechecking bug? (PR#3104) [about phantom types] From: Jacques GARRIGUE In-Reply-To: <200408261703.TAA23962@pauillac.inria.fr> References: <200408261703.TAA23962@pauillac.inria.fr> X-Mailer: Mew version 4.0.64 on Emacs 21.2 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 412E8E42.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; bug:01 jacques:01 int':01 datatypes:01 val:01 val:01 int':01 subtyping:01 jacques:01 unify:01 ocaml:01 ocaml:01 caml:01 typechecking:01 equality:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk From: bpr@artisan.com > Version: 3.08.1 > > As mentioned on the mailing list, simple use of phantom types leads to a > situation where it appears that built in types and user defined types are > handled > differently. Here's a simple example from the command line. The same behavior is > > observed when I replace int in "type 'p t = int" with int64 and int array, or > when > I change from sum type to record in PHANTOM_INT' Not surprising: the distinction is not between built-in and user-defined, but between abbreviation types and datatypes (which share the same syntax in ocaml, but have different syntax in most other dialects) > bpr@boreal[bpr]$ ocaml > Objective Caml version 3.08.1 > > # module type PHANTOM_INT = sig > type 'p t = int [...] > val add_even_even : even t -> even t -> even t > end;; [...] > # PhantomInt.add_even_even two three;; > val three : PhantomInt.odd PhantomInt.t = 3 This behaviour is perfectly normal. In the above signature, the type t is not phantom at all. It will be expanded to int before checking equality, so the type argument will be completely ignored altogether. > # module type PHANTOM_INT' = sig > type 'p t = Int of int [...] > val add_even_even : even t -> even t -> even t > end;; > # PhantomInt'.add_even_even two' three';; > This expression has type PhantomInt'.odd PhantomInt'.t > but is here used with type PhantomInt'.even PhantomInt'.t Actually this one is not much better. You indeed get an error if you try to unify [even t] with [odd t], but you still can cheat by building a value by hand (eg (Int 1 : even t) is perfectly legal), or by using subtyping ((two' :> odd t) shall work). A real phantom type must be abstract, and nothing else will. That is, in your signature, you must have: module type PHANTOM_INT = sig type 'p t ... end Jacques Garrigue ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners