From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 4DB19BC88 for ; Wed, 2 Feb 2005 10:18:17 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j129IGCs000392 for ; Wed, 2 Feb 2005 10:18:16 +0100 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 KAA08402 for ; Wed, 2 Feb 2005 10:18:16 +0100 (MET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j129IDYT000377 for ; Wed, 2 Feb 2005 10:18:15 +0100 Received: from localhost (suiren [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.13.1/8.13.1) with ESMTP id j129Hwvk009796; Wed, 2 Feb 2005 18:17:59 +0900 (JST) Date: Wed, 02 Feb 2005 18:17:33 +0900 (JST) Message-Id: <20050202.181733.56159573.garrigue@math.nagoya-u.ac.jp> To: daveberry@btconnect.com Cc: caml-list@inria.fr Subject: Re: [Caml-list] '_a From: Jacques Garrigue In-Reply-To: <6.1.2.0.2.20050129000409.0359e0a8@pop3.btconnect.com> References: <1448756C-6FF9-11D9-8411-0003939A19AA@fas.harvard.edu> <20050127.095119.88330421.garrigue@math.nagoya-u.ac.jp> <6.1.2.0.2.20050129000409.0359e0a8@pop3.btconnect.com> X-Mailer: Mew version 4.1.53 on Emacs 21.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 42009AD8.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 42009AD6.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 touted:01 polymorphism:01 semantics:01 compilation:01 polymorphism:01 inference:01 inference:01 beginners:01 semantics:01 o'caml:01 sml:01 beginners:01 abstraction:01 mutable:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: Dave, Thanks for your comments. > Basically, the touted advantages of adopting the value polymorphism > rule were: > > 1. The formal semantics became simpler. > 2. Eliminating the different types of type variable made the language > easier to explain, without affecting expressibility in practice. > 3. It enabled typeful compilation (as you note in your paper). I personally believe that the main advantage is 0. Keep the typing abstract from implementation details. This limits one very strongly when seeking alternatives. > I have never believed either half of point 2. The value polymorphism rule > means that you have to explain about references and their effect on type > inference even for some simple programs that don't use references at all, > such as the example that Mike gave. This "raises the bar" for explaining > type inference to beginners. Furthermore, expressiveness is affected for > the examples that you give in your paper. We had to change several parts > of our code when we adopted the value polymorphism rule. However, we felt > (and I still think) that points 1 and 3, particularly point 3, outweigh > these disadvantages. > > From a practical point of view, I like your approach. However, it does > negate point 1 above, because it makes the formal semantics more complex > again - although this is less of a problem in O'Caml, because its semantics > are already so complicated compared to SML97. (I do not intend that remark > as an insult). It will be interesting to see how your approach affects > point 2 - novices may still encounter the value restriction in a simple > program, and the new system will be more complicated to explain. I agree with your first remark on point 2: while it avoids introducing a new kind of variables, the value restriction is really confusing for beginners. The theoretical rule may be simple, but it is not intuitive, so one only understands it through a series of approximations. So my argument goes as: avoid introducing a new kind of variables (for the sake of abstraction), but get as much polymorphism as possible, as the non-generalizable case should be the exception. Even if the rule for what to generalize is more complex, in some ways it is closer to intuition. In "most" cases, it is just okay to generalize the result of function applications. Basically, non-generalizable cases with the relaxed restriction end up belonging to two categories: * partial applications * mutable data structures I believe this is easy to understand why they have to be restricted. For the semantics, this should not be too hard. You just need to introduce subtyping. And ocaml already has subtyping for evident reasons. Typed compilation shall also be ok. Note that we only allow generalization of covariant variables (meaning "bottom"), not contravariant ones (meaning "top"). By definition the covariant variables correspond to no value, so you shouldn't need them to determine the data representation. If we were also to generalize purely contravariant variables, then we need a top object, meaning that the representation would have to be uniform. > I sometimes wonder whether it would help to have a "pure" annotation for > function types that would require the implementation to not use references > nor to raise exceptions. I don't mean a detailed closure analysis, just a > simple flag. Most practical functions would not be pure, but many simple > ones could be, and these could be used to introduce people to the basics of > functional programming without raising the complication of the value > polymorphism rule. (You wouldn't get a theory paper out of it > though). Unfortunately I'm no longer working on programming languages and > so I don't have the capability to explore this. It may be a half-baked > idea that doesn't work in practice. This is also an idea that crosses my mind once in a while, but I never tried to formalize it further. Looks like the main problem would be to decide where to use this annotation. You can quickly get back into the above abstraction problem, if purity is not considered as an essential part of the semantics. So this looks like an idea hard to apply in practice. Jacques Garrigue