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 HAA15153; Fri, 27 Aug 2004 07:05:18 +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 HAA14281 for ; Fri, 27 Aug 2004 07:05:17 +0200 (MET DST) Received: from mail5.speakeasy.net (mail5.speakeasy.net [216.254.0.205]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id i7R55ESj029015 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Fri, 27 Aug 2004 07:05:16 +0200 Received: (qmail 21765 invoked from network); 27 Aug 2004 05:05:13 -0000 Received: from shell2.speakeasy.net ([69.17.110.71]) (envelope-sender ) by mail5.speakeasy.net (qmail-ldap-1.03) with AES256-SHA encrypted SMTP for ; 27 Aug 2004 05:05:13 -0000 Date: Thu, 26 Aug 2004 22:05:13 -0700 (PDT) From: brogoff To: Jacques GARRIGUE cc: caml-list@inria.fr Subject: Re: [Caml-list] Re: OCaml typechecking bug? (PR#3104) [about phantom types] In-Reply-To: <20040827.102827.50023947.garrigue@kurims.kyoto-u.ac.jp> Message-ID: References: <200408261703.TAA23962@pauillac.inria.fr> <20040827.102827.50023947.garrigue@kurims.kyoto-u.ac.jp> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Miltered: at nez-perce with ID 412EC10A.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; brogoff:01 brogoff:01 caml-list:01 bug:01 jacques:01 datatypes:01 abstraction:01 int':01 val:01 subtyping:01 datatype:01 unify:01 ocaml:01 ocaml:01 typechecking:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Fri, 27 Aug 2004, Jacques GARRIGUE wrote: > From: bpr@artisan.com > 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) OK, I almost understand. I thought that you absolutely needed type abstraction for phantom types to work, and I was surprised that the examples with data types "worked" in the sense that illegal use was detected. > > # 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). What I still don't understand is why we get the type "error" in this case, where I used a datatype. What am I missing? > 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 That's what I originally thought, but the behavior in the case above threw me. -- Brian ------------------- 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