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 CAA28187; Thu, 29 Mar 2001 02:43:00 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id CAA28099 for ; Thu, 29 Mar 2001 02:42:59 +0200 (MET DST) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id f2T0gRT00753 for ; Thu, 29 Mar 2001 02:42:28 +0200 (MET DST) Received: from localhost (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 JAA05369 for ; Thu, 29 Mar 2001 09:42:24 +0900 (JST) To: caml-list@inria.fr Subject: [Caml-list] Future of labels 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: <20010329094438J.garrigue@kurims.kyoto-u.ac.jp> Date: Thu, 29 Mar 2001 09:44:38 +0900 From: Jacques Garrigue X-Dispatcher: imput version 20000228(IM140) Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Hello everybody, A bit more than a year ago, we had a big "discussion" about presence of labels in the standard library, and the existence of two modes (classic and commuting labels). The two modes were kept, but the number of labels were reduced. Now that a more stable version was released, it may be time to assess whether these choices were good, and what should be done in the long-term. As a minimum step, if the classic mode is to be kept, then its semantics must be cleaned-up, because of the soundness problem I exposed a few weeks ago, and also because its typing discipline is not very well defined anyway. Personally I see two possible directions. (1) suppress the classic mode (and also labels in the standard library) advantages: now everybody can use commuting labels problems to solve: * need to provide alternative versions of some modules, were label mode users want to keep labels Not too difficult for the standard library itself, but what about other libraries. I particularly think of the Unix module, or user contributions that use labels. * what about people using "decorative labels", that is putting labels in the .mli files mainly, and only exceptionally in the implementation. i.e. real users of the classic mode. * transition for label mode users (2) clean-up the classic mode This essentialy means giving a reduction semantics that matches more closely the typed behaviour. I give more details below. Rather than getting immediately into a discussion about what is the good solution (and this might be a 3rd one), it would be nice to now really what people expect from labels. In particular arguments for keeping a classic mode are: * having labels in the standard library * using decorative labels in one's own programs/interfaces (something people asked for before ocaml 3.00) * allowing different styles depending on whether you care about commutation or not * ... Arguments for dumping it are: * avoiding multiple styles * desire for commutation, but do not want labels in the standard library * ... This would be nice if people could tell how they position themselves on these, particularly if this is backed by experience. Last year this discussion literally overflowed this mailing list, so please speak in turn, and no need to repeat what the previous poster said: this is not a vote, but a call for suggestions. Personally, if there is no support for classic mode as it is, removing it would simplify things. There are so few labels left in the standard library that removing them would not be a big pain. The problem of other libraries, and particularly Unix, needs more work, but I would think it could be solved, if in particular people are really ready to write labels when they use 3rd party libraries. Cheers, Jacques Garrigue P.S. Here are some possible rules for a better classic mode (still 100% compatible with ocaml 2, and 99% compatible with the current mode) To keep the soundness, type annotations would have to intervene in reductions. Before bashing about overloading, note that not inferred types, but only syntactic type annotations are used, meaning that we are still more or less working with an untyped semantics. (fun ~l:x -> e) ~l:v --> e[v/x] (fun ~l:x -> e) v --> e[v/x] (fun ?l:x -> e) ~l:v --> e[Some v/x] (fun ?l:x -> e) e --> (e[None/x]) e (f : l:t -> t') ~l:e --> (f e : t') (f : ?l1:t1 -> ... ?ln:tn -> l:t -> t') e --> (f e : t') (f : ?l1:t1 -> ... ?ln:tn -> ?l:t -> t') ~l:e --> (f ~ln:e : ?l1:t1 -> ... ?ln:tn -> t') (f : ?l1:t1 -> ... ?ln:tn -> 'a) --> f Advantage: we can now see at the semantic level that while (fun ~l:x -> e) ~l':e' is not legal (stuck when l <> l'), let f ~l:x = e in (f : l':t -> t') ~l':e' is legal (as it should be in classic mode, where different labels are unifiable). And of course this allows to discard optional arguments on the basis of type information, solving the current soundness problem. Problems: * this is a bit complex to understand in detail * type checking this relies on type information discrimination (but it should be added to the compiler anyway) ------------------- To unsubscribe, mail caml-list-request@inria.fr. Archives: http://caml.inria.fr