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 F1903BB91 for ; Sat, 29 Jan 2005 01:34:19 +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 j0T0YI0q000722 for ; Sat, 29 Jan 2005 01:34:19 +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 BAA03795 for ; Sat, 29 Jan 2005 01:34:18 +0100 (MET) Received: from dswu26.btconnect.com (dswu26.btconnect.com [193.113.154.27]) by nez-perce.inria.fr (8.13.0/8.13.0) with SMTP id j0T0YHOA000719 for ; Sat, 29 Jan 2005 01:34:18 +0100 Received: from Dagmar.btconnect.com (actually host 97.95.134.81.in-addr.arpa) by dswu26.btconnect.com with SMTP-CUST (XT-PP) with ESMTP; Sat, 29 Jan 2005 00:33:54 +0000 Message-Id: <6.1.2.0.2.20050129000409.0359e0a8@pop3.btconnect.com> X-Sender: daveberry@pop3.btconnect.com X-Mailer: QUALCOMM Windows Eudora Version 6.1.2.0 Date: Sat, 29 Jan 2005 00:33:46 +0000 To: Jacques Garrigue From: Dave Berry Subject: Re: [Caml-list] '_a Cc: caml-list@inria.fr In-Reply-To: <20050127.095119.88330421.garrigue@math.nagoya-u.ac.jp> References: <1448756C-6FF9-11D9-8411-0003939A19AA@fas.harvard.edu> <20050127.095119.88330421.garrigue@math.nagoya-u.ac.jp> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii"; format=flowed X-Miltered: at nez-perce with ID 41FADA0A.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41FADA09.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 datatypes:01 sml:01 compiler:01 polymorphism:01 touted:01 polymorphism:01 semantics:01 compilation:01 inference:01 inference:01 beginners:01 semantics:01 o'caml:01 sml:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: Jacques, That's a very interesting paper. I note that you ask "Our examples with constructor functions and abstract datatypes were expressible in systems predating the value restriction, and are refused by the strict value restriction. This makes one wonder why this didn't cause more problems during the transition." At the time that SML'97 was being defined, I was working on Harlequin's SML compiler and programming environment (which has long since vanished into legal limbo). The Harlequin team initially opposed the adoption of the value polymorphism rule for precisely the reasons you give. Eventually we gave in because the other advantages outweighed the disadvantages. (All these discussions took place in private e-mail). 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 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 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. Best wishes, Dave. At 00:51 27/01/2005, Jacques Garrigue wrote: >From: Mike Hamburg >Subject: [Caml-list] '_a >Date: Wed, 26 Jan 2005 19:19:16 -0500 > > > The appearance of '_a in places where it shouldn't appear causes some > > annoyance, and a good deal of confusion among beginners to O'Caml. In > > particular, List.map (fun x -> x) "ought to" have type 'a list -> 'a > > list, whereas it instead has type '_a list -> '_a list. > > > > Some types are treated specially for creation of '_a, such as refs and > > arrays. For instance, if you have the following two declarations: > > > > # let a = let f x () = [x] in f [];; > > val a : unit -> 'a list list = > > # let b = let f x () = [|x|] in f [];; > > val b : unit -> '_a list array = > > > > Although I haven't read the code for O'Caml, I deduce from this that > > there is deep magic in place to determine when to turn 'a into '_a, and > > in many cases, the heuristic is wrong (in the conservative direction: > > in this case, 'a should not be turned into '_a until b is applied). > >There is no deep magic, no heuristics. There is just a type system >which guarantees type soundness (i.e. "well typed programs cannot >produce runtime type errors"). > >If you want the type system and all the historical details, read my >paper "Relaxing the value restriction" at > http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/ > >In a nutshell, ocaml uses an improvement of the value restriction. >With the value restriction, only definitions which are syntactical >values (i.e. that do not call functions, etc when defined) are allowed >to contain polymorphic type variables. >This is improved by allowing covariant type variables to be >generalized in all cases. Your first example is ok, because list is a >covariant type, but your second fails, because array is not (you may >assign to an array, and you would have to look at the code to see that >each call to b creates a different array) > >Of course, one could think of many clever tricks by looking >at what the code actually does. The above paper describes some of the >"crazy" things Xavier Leroy and others tried in the past, which >actually subsume your ideas, before they all decided this was too >complicated. The main reason is that, if something is going to break >at module boundaries, then it is not really useful. > >Good reading, > >Jacques Garrigue > >_______________________________________________ >Caml-list mailing list. Subscription management: >http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list >Archives: http://caml.inria.fr >Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >Bug reports: http://caml.inria.fr/bin/caml-bugs