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 PAA27252 for caml-redistribution@pauillac.inria.fr; Thu, 6 Apr 2000 15:21:43 +0200 (MET DST) Resent-Message-Id: <200004061321.PAA27252@pauillac.inria.fr> 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 HAA30515 for ; Tue, 4 Apr 2000 07:50:39 +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 HAA07752 for ; Tue, 4 Apr 2000 07:50:37 +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 OAA24140; Tue, 4 Apr 2000 14:50:25 +0900 (JST) To: Christophe.Raffalli@univ-savoie.fr Cc: caml-list@inria.fr Subject: Re: Semantic of label: The best (only ?) solution to merge both mode In-Reply-To: Your message of "Sun, 02 Apr 2000 21:24:59 +0200" <38E79E8B.100C8F60@univ-savoie.fr> References: <38E79E8B.100C8F60@univ-savoie.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: <20000404145025N.garrigue@kurims.kyoto-u.ac.jp> Date: Tue, 04 Apr 2000 14:50:25 +0900 From: Jacques Garrigue X-Dispatcher: imput version 980905(IM100) Resent-From: weis@pauillac.inria.fr Resent-Date: Thu, 6 Apr 2000 15:21:43 +0200 Resent-To: caml-redistribution@pauillac.inria.fr From: Christophe Raffalli > Let's only talk about the modern mode ! > > I wanted to really use commuting labels, I was ready to change my habit, > but I found them to restrictive. I find my proposal, which is just to > change a bit the semantics of function application (and nothing else) on > non-labelled arguments quite nice and useful (no need to always remember > all the label names if you prefer to remember the order of the > arguments). * They are (a bit) restrictive. This is intentional. (Still, there will be less labels in the standard library in 3.00.) Experience with olabl shows that non-optional labels are more useful as documentation than for commutation. If you don't have to write them, you will probably not write them, and you loose the benefit. Sometimes you have to be forced to do things that are good for you :-) And please do not compare this with ADA: these are only a few more characters, in an already very compact language. * For you this is just a matter of remembering either position or labels. But if someone is to read your code, he will have to switch from one to the other at each application, according to the one you choosed. Not so nice. > As my proposal only cost to change about 20 lines why not have an option > to the modern mode to let people try it for real and see what they think > ? This is not a problem of number of lines. Before putting even one line of code in the type checker, we have to be sure it is not breaking anything in the language. I asked you to produce 1) type inference rules (which must mix with the rest of the language) 2) an untyped reduction semantics, including optional arguments (you cannot use the type of the function to decide how it should be evaluated, only its value) These are pre-conditions. If you do not produce these, this is just an idea, not a proposal. And I don't see why I should do the work for you, since I am satisfied with the current system. > About the "so wonderfully clean theoretically" .. it is not so clear: > look at this example: > > > lama-d134:~> ocaml -modern > > Objective Caml version 2.99 (99/12/08) > > > > # let h f = f x:1 y:2;; > > val h : (x:int -> y:int -> 'a) -> 'a = > > # let h f = f y:1 x:2;; > > val h : (y:int -> x:int -> 'a) -> 'a = > > > > > > The infered type depends on the way you write thing while one could think > > they are equivalent (the labels commute in modern mode, don't they ?) This is just an example of how keeping the theory clean may force you to weaken the implementation. In olabl those two types were to a great extent equivalent, but this resulted in breaking the call-by-value semantics in some special cases. We add to back on this. If you really want those two types to be equivalent, you will have to pay (probably a lot) in terms of efficiency. Considering that commutation is not very useful in this particular case, it is better to have the compiler refuse this code than turn it into an innefficient blurb. Call it a trade-off. Not between theory and practice, just between power and efficiency. Regards, Jacques Garrigue --------------------------------------------------------------------------- Jacques Garrigue Kyoto University garrigue at kurims.kyoto-u.ac.jp JG