From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: weis Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id PAA10882 for caml-redist; Wed, 26 Apr 2000 15:37:43 +0200 (MET DST) 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 LAA18669 for ; Wed, 26 Apr 2000 11:34:16 +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.8.7/8.8.7) with ESMTP id LAA09069 for ; Wed, 26 Apr 2000 11:34:14 +0200 (MET DST) Received: from localhost (sansho.kurims.kyoto-u.ac.jp [130.54.16.90]) by kurims.kurims.kyoto-u.ac.jp (8.9.3/3.7W) with ESMTP id SAA04931; Wed, 26 Apr 2000 18:34:07 +0900 (JST) To: bpr@best.com Cc: caml-list@inria.fr Subject: Re: Polymorphic variants question In-Reply-To: Your message of "Tue, 25 Apr 2000 17:25:09 -0700 (PDT)" References: X-Mailer: Mew version 1.93 on Emacs 20.5 / Mule 4.0 (HANANOEN) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20000426183407I.garrigue@kurims.kyoto-u.ac.jp> Date: Wed, 26 Apr 2000 18:34:07 +0900 From: Jacques Garrigue X-Dispatcher: imput version 980905(IM100) Sender: weis From: Brian Rogoff > class type ['a] a = object method do_a : int method downcast : 'a end [...] > If we replace the variant with a polymorphic variant. > type objsum = [`A of objsum a | `B of objsum b];; > > and then we do the same thing as before the type checker complains. > > # class test_a = > object (s) > method downcast = `A (s :> objsum a) > method do_a = 1 > end;; > # Characters 6-103: > # Some type variables are unbound in this type: > # class test_a : object method do_a : int method downcast : #objsum[>`A] > end > # The method downcast has type #objsum[>`A] where 'a is unbound > > This is a good error message, and it tells me what to do to fix the > problem right away: I add an annotation to constrain that "#objsum[>`A]" > > Now, in order to avoid surprises in the future, can someone tell me why I > should have expected that type "#objsum[>`A]" to be computed, and hence known > that I would need to constrain the type? It makes sense, but I don't yet > have a good mental model for the typing of polymorphic variants > which would have allowed me to write the correct version immediately. How > do the experts go about mentally inferring the right types in cases like > this? Variant typing can be quite subtle, so I suggest that you read my ML workshop paper. This is the first one in the list at http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/ A simpler document is olabl's manual http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/ What OCaml 3 does is even more complicated, but the explanations in these papers should be more intuitive. The idea is that a variant type is the combination of 3 components: * a list of pairs tag/type giving the type of the argument for each constructor. * a lower bound, that is the list of tags any matching on this variant must handle. This appears after the ">" in types. * an upper bound, that is the list of tags one may add to this type. This appears after the "<" in types. When there is a ">" and no "<" in a variant type the upper bound is open: you may add anything. To print types in a reasonably compact way, the actual syntax of types mangles that a bit: if there is no upper bound, argument types are printed inside the lower bound, otherwise they are printed in the upper bound. Your example is a bit hard to follow, but here is what happens: * since you coerce (s) to (objsum a), it is given the type (#objsum #a) (a is covariant in its parameter). * since (s) is the object itself, this constrains downcast to return a result of type (#objsum), which actually represents an upper bound: [< `A of objsum a | `B of objsum b] * as downcast returns actually (`A ...), there is also a lower bound constraint: [< `A of objsum a | `B of objsum b > `A]. * since the lower bound {`A} is smaller than the upper bound {`A,`B}, this type is polymorphic: it can be instantiated either in (objsum), i.e. [`A of objsum a | `B of objsum b], or in [`A of objsum b] (dropping the `B). Hope it helps, Jacques --------------------------------------------------------------------------- Jacques Garrigue Kyoto University garrigue at kurims.kyoto-u.ac.jp JG