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 QAA10384; Thu, 22 Aug 2002 16:26:54 +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 QAA14803 for ; Thu, 22 Aug 2002 16:26:54 +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 g7MEQpX22625 for ; Thu, 22 Aug 2002 16:26:52 +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 XAA07743; Thu, 22 Aug 2002 23:26:45 +0900 To: nalexander@amavi.com Cc: caml-list@inria.fr Subject: Re: [Caml-list] Naming polymorphic variant types -- additional questions In-Reply-To: <1066.207.194.7.55.1029979596.squirrel@mail.gx.ca> References: <1413.207.194.7.18.1029903741.squirrel@mail.gx.ca> <20020821142724W.garrigue@kurims.kyoto-u.ac.jp> <1066.207.194.7.55.1029979596.squirrel@mail.gx.ca> 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: <20020822232630X.garrigue@kurims.kyoto-u.ac.jp> Date: Thu, 22 Aug 2002 23:26:30 +0900 From: Jacques Garrigue X-Dispatcher: imput version 20000228(IM140) Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk From: "Nick Alexander" > When I was trying this, I accidently tried: > type outer = [< 'A | 'B] > and was duly rewarded with > Unbound type parameter [..] OK, [< t] and [> t] types contain an hidden type variable. If you really want to define a polymorphic type, you must write type 'a outer = 'a constraint 'a = [< `A | `B] Looks a bit confusing? This just means that ('a outer) can unify with anything included in [< `A | `B] > I am also a neophyte polymorphic variants user. It seems very intuitive > to me that [`A] is a subtype of [`A | `B]. Jacques informs me that > unification rejects the subtyping in favour of equality. So, what is the > situation where [`A] is _not_ a subtype of [`A | `B]? Ie, what common > construct, design pattern, or idiom reflects this? [`A] _is_ a subtype of [`A | `B]. The point is just that in ocaml subtyping is not implicit, like it is in most OO languages. fun (x : [`A]) -> (x :> [`A|`B]) , where :> denotes an explicit coercion, is typable, showing the subtyping relation. In ocaml, the implicit subsumption relation is instanciation rather than subtyping. While subtyping makes function arguments contravariant, with instanciation everything is "covariant", which has some advantages, but clearly doesn't mix well with subtyping. Polymorphic variants are based on instanciation: a polymorphic variant type can be seen as a constraint on the values that may go through this type. Unification refines it. Another small point is that in ML quantification only occurs at toplevel. This means that [< `A | `B] itself is not a closed type, and that you cannot close it easily. As a result, you cannot compare it to [`A], other than say they are unifiable. On the other hand, if you have a function whose type is All('a). ([< `A | `B] as 'a) -> t (this is the meaning of "val f : [< `A | `B] -> t") and another function whose type is [`A] -> t (here there is nothing to quantify), then you can see that the first one will accept more inputs, and as a result is more general then the second one. Not very clear, but this is the rough idea. 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