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 VAA15083 for caml-redistribution; Sun, 22 Aug 1999 21:13:17 +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 JAA20411 for ; Mon, 16 Aug 1999 09:08:05 +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 JAA25470; Mon, 16 Aug 1999 09:07:48 +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 QAA10535; Mon, 16 Aug 1999 16:07: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 "Mon, 16 Aug 1999 08:31:58 +0200" <19990816083158.52649@pauillac.inria.fr> References: <19990816083158.52649@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: <19990816160801Q.garrigue@kurims.kyoto-u.ac.jp> Date: Mon, 16 Aug 1999 16:08:01 +0900 From: Jacques GARRIGUE X-Dispatcher: imput version 980905(IM100) Content-Transfer-Encoding: 7bit Sender: weis From: Francois Pottier > > 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 fail to see why type abbreviations should be monomorphic while > their declaration is being checked. Is this intended to make the > type system safe, or to guarantee the typechecker's termination? My explanation probably lacked clarity. Since abbreviations may contain constraints, one must expand them when defining types depending on them (to check that the constraints are satisfied). If the abbreviation has been defined earlier, no problem, you just extract its constraints. But if it is yet to be defined (which is the case with mutually recursive definitions), you must keep everything monomorphic so that constraints can be enforced later. What we want is just to enforce constraints from the abbreviation to other type definitions, but as a result this means also introducing constraints the other way round (classical problem with unification). My comment was that such a restrictive algorithm is needed if we want to collect all constraints in one pass, but if we require that all abbreviation definitions contain explicitely all their constraints, the above problem can be avoided with a two-pass algorithm. > By the way, I find O'Caml's error messages on this topic rather > strange. Error messages with unification are hard. You can see here another funny behaviour with recursive definitions: # type t = u and u = unit;; type t = unit type u = t Jacques --------------------------------------------------------------------------- Jacques Garrigue Kyoto University garrigue at kurims.kyoto-u.ac.jp JG