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 UAA12374 for caml-redistribution; Sun, 22 Aug 1999 20:12:03 +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 DAA24166 for ; Fri, 13 Aug 1999 03:41:53 +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 DAA00134; Fri, 13 Aug 1999 03:41:44 +0200 (MET DST) Received: from localhost (safran.kurims.kyoto-u.ac.jp [130.54.16.91]) by kurims.kurims.kyoto-u.ac.jp (8.9.1a/3.7W) with ESMTP id KAA16804; Fri, 13 Aug 1999 10:41:41 +0900 (JST) To: Francois.Pottier@inria.fr Cc: caml-list@inria.fr Subject: Re: Weird behavior with mutually recursive type definitions In-Reply-To: Your message of "Wed, 4 Aug 1999 15:52:39 +0200" <19990804155239.50895@pauillac.inria.fr> References: <19990804155239.50895@pauillac.inria.fr> X-Mailer: Mew version 1.93 on Emacs 20.4 / Mule 4.0 (HANANOEN) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <19990813104206X.garrigue@kurims.kyoto-u.ac.jp> Date: Fri, 13 Aug 1999 10:42:06 +0900 From: Jacques GARRIGUE X-Dispatcher: imput version 980905(IM100) Content-Transfer-Encoding: 7bit Sender: weis From: Francois Pottier > Now, here's the problem. Let's change just one word, and make the type > declarations mutually recursive, even though they needn't be: > > type 'a t = 'a dummy > and specialized = int t > > O'Caml still accepts the code, but this time, it constrains 'a to be equal to > int, as if the type constructor t could not be used polymorphically within its > own declaration: > > type 'a t = 'a dummy constraint 'a = int > ^^^^^^^^^^^^^^^^^^^ > type specialized = int t > > Why is this? Can someone explain, or is it a typechecker bug? As Hendrik Tews already answered, this is not a bug. Like value definitions, recursive type abbreviation definitions are not polymorphic (while they are defined). So if in your defintion you use the abbreviation at a different type, a constraint is added. Why is it so? Constraints are required for the object system, and if there are constraints you must expand abbreviations inside definitions to check them. If recursion occurs before the abbreviation is generalized, this means that all occurences of an abbreviation in the same type definition will be unified, and have the same constraints. I personnaly think that, like for polymorphic recursion, the semantics could be changed so that the user has to write explicitely the constraints. In type definitions, this makes sense. If a constraint appears to be needed somewhere and was not declared, there would be an error. Technically this would probably mean doing two passes on type definitions: one to introduce definitions (polymorphically) and one to check the constraints. In such a way, one could avoid this strange side-effect of the object system on the rest of the language. Comments, Jerome ? Jacques --------------------------------------------------------------------------- Jacques Garrigue Kyoto University garrigue at kurims.kyoto-u.ac.jp JG