From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id WAA06987 for caml-redist@pauillac.inria.fr; Mon, 15 May 2000 22:09:12 +0200 (MET DST) Resent-Message-Id: <200005152009.WAA06987@pauillac.inria.fr> Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id CAA00268 for ; Mon, 15 May 2000 02:33:56 +0200 (MET DST) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e4F0Xsv17906 for ; Mon, 15 May 2000 02:33:55 +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 JAA07716; Mon, 15 May 2000 09:33:39 +0900 (JST) To: Judicael.Courant@lri.fr Cc: caml-list@pauillac.inria.fr Subject: Re: Typechecking of recursive variants In-Reply-To: Your message of "Fri, 12 May 2000 16:34:08 +0200 (MEST)" <200005121434.QAA12123@pc87.lri.fr> References: <200005121434.QAA12123@pc87.lri.fr> 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: <20000515093335H.garrigue@kurims.kyoto-u.ac.jp> Date: Mon, 15 May 2000 09:33:35 +0900 From: Jacques Garrigue X-Dispatcher: imput version 980905(IM100) Resent-From: weis@pauillac.inria.fr Resent-Date: Mon, 15 May 2000 22:09:12 +0200 Resent-To: caml-redist@pauillac.inria.fr From: Judicael Courant > Objective Caml version 3.00 > > # let rec x n = if n = 0 then `Y else `X (x (n-1));; > val x : int -> ([> `Y | `X of 'a] as 'a) = > # x 3;; > - : _[> `Y | `X of '_a] as 'a = `X (`X (`X `Y)) > # match x 4 with `X z -> z | `Y -> assert false;; > - : [ `Y | `X of '_a] as 'a = `X (`X (`X `Y)) > > > What do these underscores mean ? Anything to do with monomorphic type > variables ? Exactly. Since "x 3" is an application, its result must be monomorphic. But in fact the _ in '_a is a bug :-) In recursive variants, the monomorphism is not indicated on the abbreviation, but on the variant type itself (like for objects). So the right types would be # x 3;; - : _[> `Y | `X of 'a] as 'a = `X (`X (`X `Y)) # match x 4 with `X z -> z | `Y -> assert false;; - : [ `Y | `X of 'a] as 'a = `X (`X (`X `Y)) Notice that there is no monomorphism annotation in the second type, since it cannot be refined anymore. > Why is not there any ">" at the beginning of the latest > type ? Your original type was [> `Y | `X of 'a], and you matched it with cases producing the type [< `Y | `X of 'a]. By unification, the result is [< `Y | `X of 'a > `Y | `X], or, in abbreviated form, [`Y | `X of 'a] since all constructors are required. Since you type was monomorphic, this unification affects the type of "x 4", which is also the type of the argument of `X. Jacques --------------------------------------------------------------------------- Jacques Garrigue Kyoto University garrigue at kurims.kyoto-u.ac.jp JG