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 EAA02364; Tue, 22 Oct 2002 04:13:20 +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 EAA02455 for ; Tue, 22 Oct 2002 04:13:19 +0200 (MET DST) Received: from favie.faith.gr.jp (favie.faith.gr.jp [61.127.175.250]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g9M2DGD23953 for ; Tue, 22 Oct 2002 04:13:17 +0200 (MET DST) Received: from localhost (dhcp7.faith.gr.jp [192.168.1.17]) by favie.faith.gr.jp (8.9.3/8.9.3) with ESMTP id LAA31258; Tue, 22 Oct 2002 11:00:03 +0900 To: jcohen@lami.univ-evry.fr Cc: caml-list@inria.fr Subject: Re: [Caml-list] inference and phantom types In-Reply-To: <3DB41BFF.4010302@lami.univ-evry.fr> References: <3DB41BFF.4010302@lami.univ-evry.fr> X-Mailer: Mew version 1.94.2 on Emacs 21.2 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20021022105935Y.garrigue@kurims.kyoto-u.ac.jp> Date: Tue, 22 Oct 2002 10:59:35 +0900 From: Jacques Garrigue X-Dispatcher: imput version 20000228(IM140) Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk From: Julien Cohen > I read in the thread > http://caml.inria.fr/archives/200109/msg00097.html > that phantom types could be used in ocaml but I have some > troubles understanding the way they really work. > > In the following session I use a phantom type ('a,'b)t to > simulate a list with an additionnal type 'b. I create a special > cons preserving the type. I create an (int,bool)t value and when > I make a cons on it and the phantom type seems not to be well > infered: > > > > Objective Caml version 3.04 > > # type ('a,'b) t = 'a list;; > type ('a, 'b) t = 'a list > > # let f (x:'a) (y:('a,'b) t) = (x::y : ('a,'b) t);; > val f : 'a -> ('a, 'b) t -> ('a, 'b) t = > > # let (v: (int,bool) t) = [1];; > val v : (int, bool) t = [1] > > # f 1 v;; > - : (int, '_a) t = [1; 1] > > > Is there a fundamental reason for the bool type not to be inferred? > (no response in the ocaml-beginner list) Not surprising, this is not a beginner question :-) What happens is just that abbreviation types are expanded before unification, meaning that you are actually not unifying ('a,'b) t with ('c,'d) t, but only 'a list with 'c list, so that 'b and 'd will not be unified. Note that in recent versions of ocaml, defining a datatype (with constructors) will not help: the typecker infers variance, and will detect that 'b is unused in the definition, so that again it will just be discarded during unification (or subtyping). The real solution is to use an abstract type: put your type definition in a module with necessary operations, and provide an interface where the type is abstract. For instance module M : sig type (+'a,'b) t val inj : 'a list -> ('a,'b) t val proj : ('a,'b) t -> 'a list end = struct type ('a,'b) t = 'a list let inj x = x let proj x = x end If you really don't want your type to be abstract, you will need to make the type variable appear somewhere in it with the right variance, which can be complicated... 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