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 XAA20276 for caml-redistribution@pauillac.inria.fr; Sun, 2 Apr 2000 23:34:48 +0200 (MET DST) Resent-Message-Id: <200004022134.XAA20276@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 GAA19129 for ; Fri, 31 Mar 2000 06:31:46 +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 GAA21303 for ; Fri, 31 Mar 2000 06:31:45 +0200 (MET DST) Received: from tet.kurims.kyoto-u.ac.jp (isdnppp2.kurims.kyoto-u.ac.jp [130.54.16.103]) by kurims.kurims.kyoto-u.ac.jp (8.9.3/3.7W) with ESMTP id NAA12589; Fri, 31 Mar 2000 13:31:37 +0900 (JST) Received: from localhost (localhost [127.0.0.1]) by tet.kurims.kyoto-u.ac.jp (8.9.3/8.9.3) with ESMTP id NAA15179; Fri, 31 Mar 2000 13:34:29 +0900 (JST) (envelope-from garrigue@kurims.kyoto-u.ac.jp) To: skaller@maxtal.com.au, 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 "Thu, 30 Mar 2000 19:39:30 +1000" <38E320D2.6F67964C@maxtal.com.au> References: <38E320D2.6F67964C@maxtal.com.au> 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: <20000331133429V.garrigue@kurims.kyoto-u.ac.jp> Date: Fri, 31 Mar 2000 13:34:29 +0900 From: Jacques Garrigue X-Dispatcher: imput version 980905(IM100) Resent-From: weis@pauillac.inria.fr Resent-Date: Sun, 2 Apr 2000 23:34:48 +0200 Resent-To: caml-redistribution@pauillac.inria.fr From: John Max Skaller > This gives the olabl people their old labels back, > while merely requiring classic uses to decorate definitions > with labels. In this case a temporary compiler mode switch > to allow classic users to upgrade piecemeal would be ideal. > > To me, this proposal appeals. (Will it work? Do I understand it?) OK, I think that the problem is that the people do not understand all the constraints which must be fulfilled by the label system. One is that we must keep compatibility with non-labelled mode, virtually forever. We just cannot force anybody to switch to labelled mode. We are talking about ML, not a new language starting from scratch. Another one is that there is a whole bunch of theoretical properties that must be kept. Maybe you don't even know about them, but this is thanks to them that you can be confident when the compiler tells you that your program is OK. (At least much more confident than in weakly typed languages.) Now the answer is very short: you cannot provide simultaneously (in the same mode) 1) backward compatibility 2) commutation of (non-optional) labels 3) labels as documentation (that is, anywhere you feel like putting them) Here is a proof of that. Suppose you have two functions with same types but different labels in the standard library (3 above). A good example of that is Pervasives.output: out_channel -> buf:string -> pos:int -> len:int -> unit Buffer.add_substring: Buffer.t -> string -> pos:int -> len:int -> unit If you apply them both on their first argument, you obtain functions whose difference is limited to labels. Now, you could want to put these functions in a list. let l = [output oc; Buffer.add_substring b];; This must work for backward compatibility (1). What type shall we give to l? There's no unique answer, and this is actually the case that the classic mode will give you either (buf:string -> ...) list or (string -> ...) list depending on the order in which you listed the functions. This is not a problem since in classic mode you will anyway have to consume arguments in a fixed order, and labels are just a decoration. (For label check to work properly (in theory), you must use it only on function whose type is known, as are all library functions.) Now suppose you base yourself on this non-deterministic type information to reorder arguments by commutation according to the labels given in the application (2). Well, this is as you would expect, anything can happen. Including the compiler passing parameters in the wrong order and not telling you anything about the commutation done! More generally, I can also write: let l' : (string -> len:int -> pos:int -> unit) list = l;; Since labels have to be ignored during unification, this must be accepted. Now, what will be the outcome of this application? (List.hd l') "Hello" pos:1 len:2 "l", not "el" as it should. So, please do not ask for something that is just plain impossible. Classic mode is already providing the maximum one can expect: * backward compatibility * commutation for optional arguments * fully transparent (and yet useful) labels for non-optional ones This is the default mode, and would have been probably the only one if olabl had not existed. Now, the commuting label mode is just for those who are ready to change a bit their habits. And since it is my personal creation (with others), I will just refrain from explaining why it is so wonderfully clean theoretically. Best regards, Jacques --------------------------------------------------------------------------- Jacques Garrigue Kyoto University garrigue at kurims.kyoto-u.ac.jp JG