From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id FAA12267; Tue, 10 Apr 2001 05:38:01 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 FAA12263 for ; Tue, 10 Apr 2001 05:38:00 +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.11.1/8.10.0) with ESMTP id f3A3bwn29837 for ; Tue, 10 Apr 2001 05:37:59 +0200 (MET DST) Received: from localhost (mikan.kurims.kyoto-u.ac.jp [130.54.16.202]) by kurims.kurims.kyoto-u.ac.jp (8.9.3/3.7W) with ESMTP id MAA11786 for ; Tue, 10 Apr 2001 12:37:56 +0900 (JST) To: caml-list@inria.fr Subject: Re: [Caml-list] Future of labels, and ideas for library labelling In-Reply-To: <4.3.2.7.2.20010409124220.00d4a810@shell16.ba.best.com> References: <4.3.2.7.2.20010402232928.00d3b180@shell16.ba.best.com> <3AD16EBE.831E8DD@ozemail.com.au> <4.3.2.7.2.20010409124220.00d4a810@shell16.ba.best.com> X-Mailer: Mew version 1.94.2 on Emacs 20.7 / Mule 4.0 (HANANOEN) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20010410123756H.garrigue@kurims.kyoto-u.ac.jp> Date: Tue, 10 Apr 2001 12:37:56 +0900 From: Jacques Garrigue X-Dispatcher: imput version 20000228(IM140) Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk [ Disclaimer: you can safely skip this message if you are not interested in labels. It is about modalities of use for people who want them. ] To summarize recent posts by various people, there are two approaches for a universal mode: * Take the label mode as a basis, and split libraries where needed to avoid troubling non-labellers. Labels, when present, are no longer optional. * Extend classic mode with commutation, and keep labels in libraries. Labels are kept optional. Now let me explain what is the trouble with the second option. To put it simply: you cannot have commutation, first class functions, type inference, and allow discarding of labels in unification. People presented other languages more flexible with labels, but all these languages had neither type inference nor first class functions. Why is it so: type inference is based on unification. If you allow discarding labels during unification, then the notion of what is a labelled argument becomes fundamentally ambiguous. In the most simplistic way (what is currently done in classic mode), the type of a function variable will be non-deterministically taken from the possible types inferred for this function. Imagine the context gives both "f : a:int -> b:int -> int" and "f : b:int -> a:int -> int". For labels to be really optional, you have to accept unifying these two types, taking for the type of f one of these two. This is not (too) ambiguous in current classic mode, since anyway positional order is fixed, but if you allow commutation, then this is not only the type which is non-deterministic, but also the result of your function! The situation might be improved a bit by using subtyping in place of unification (which is known as very hard to infer!), but even then it would still mean that the semantics use overloading, and we cannot have a clean untyped semantics as is currently the case. Consider (f : a:int -> a:int -> int). If we forget labels selectively, we can both obtain (f : a:int -> int -> int) and (f : int -> a:int -> int), meaning that the semantics of (f 1 ~a:2) depends on a notion of what is the current type of f. Also, subtyping changes direction on left sides of arrows, so this wouldn't be enough to make labels fully optional. So, is there no way out? Not completely, if we accept to start from strict unification: function types can be unified only if they bear identical labels. This is the first option: starting from label mode. But then, we can be more lenient: If only non-labelled arguments are given, and if their number matches the arity of the function, then the type checker automatically adds missing labels. This is more or less what Chris Hecker is asking for. What is nice about it: the semantics need not be changed, the only thing the type checker does is adding labels in completely unambiguous cases, where there is only one way to add them, and not adding them would make typing fail. This makes efficient use of the fact order of arguments in function types is fixed in ocaml (contrary to olabl). This departs slightly from the pure untyped semantics for the source program (semantics applies on a completed program), so that there should be a way to turn on a warning, to make sure one's program is complete, and pure semantics apply directly to the source. This corresponds to the idea of having strict labels has a submode of default mode. Are there people who would _not_ be satisfied by such an approach? A point of detail: this would _not_ solve the fold problem. For two reasons. One is that unification is kept strict, so the function you pass to fold should have the right labels. And more specifically, you wouldn't even be able to omit labels in the call of fold itself: since fold has its return argument of polymorphic type, its arity is not known, and we cannot tell whether an application is complete or not. (One could accept this case on the ground that the ambiguity is really minor, but the ambiguity exists.) Anyway, I really think this discussion around fold and higher-order functions is pointless: I'd rather let people use the labeled or the non-labeled form according to their taste, than deciding what is the right one for everybody. Frank Atanassow made a very interesting contribution on this subject, on how the same person may both appreciate programming by combinators (without labels), and also a more imperative style (with commuting labels). Cheers, Jacques Garrigue ------------------- To unsubscribe, mail caml-list-request@inria.fr. Archives: http://caml.inria.fr