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 RAA18832; Wed, 11 Apr 2001 17:12:15 +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 RAA18833 for ; Wed, 11 Apr 2001 17:12:14 +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 f3BF8nD05118; Wed, 11 Apr 2001 17:08:50 +0200 (MET DST) Received: from localhost (isdnppp3.kurims.kyoto-u.ac.jp [130.54.16.104]) by kurims.kurims.kyoto-u.ac.jp (8.9.3/3.7W) with ESMTP id AAA01895; Thu, 12 Apr 2001 00:08:46 +0900 (JST) To: remy@morgon.inria.fr Cc: caml-list@inria.fr Subject: Re: [Caml-list] Future of labels, and ideas for library labelling In-Reply-To: References: <20010411172919K.garrigue@kurims.kyoto-u.ac.jp> 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: <20010412001114U.garrigue@kurims.kyoto-u.ac.jp> Date: Thu, 12 Apr 2001 00:11:14 +0900 From: Jacques Garrigue X-Dispatcher: imput version 20000228(IM140) Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Salut Didier, > I am not sure I understand all your conclusions: > > > * SLIGHTLY extend it to allow non-labelled complete applications of > > functions: this is non-ambiguous, but keep a warning for PURISTS, > > and also because of the SLIGHT MISMATCH between PROGRAM TEXT and > > UNTYPED SEMANTICS > > I do not understand much of this sentence. > Moreover, I am a bit worried by the use of the words I've emphasized. Yes, this is not the kind of language you usually understand. I think I gave a bit more details on it in the developper's list, but anyway here are full details for interested people. The intended "slight" extension: Suppose I have a function f, of type string -> pos:int -> len:int -> string. It appears in a program applied on 3 arguments, without any labels: f "Hello" 1 2 The idea is to have the type checker insert the labels rather than fail with a type error. To be sure nothing ambiguous is happening, and to avoid "misuses" of this feature, we have to be a bit strict: * no argument should be labelled * the arity of f must be known, and it must exactly match the number of arguments In particular functions whose return type is a type variable are not eligible for that, since their arity is unknown. With all these conditions, it is clear that no ambiguity will happen: type checking was going to fail otherwise, and there is only one way to add labels in this application. If you care about stronger properties than that, in the current version type checking with labels is not complete, but it produces a unique type: when type checking succeeds, the type it finds does not depend on the inference algorithm, but whether a type will be found or not depends on it. Basically this property is not changed: either we knew the complete type for f at the application point, and could add the right labels, or we didn't know the type and it will fail either immediately or later. By the way, we were doing something pretty similar in our paper on first class polymorphism. The problem I describe at the semantics level is related to this notion of adding labels. Without optional arguments, the reduction in label mode can be described by this single rule: (fun ~ln:x -> e) ~l1:v1 ... ~ln:vn ---> e[vn/x] ~l1:v1 ... ~ln-1:vn-1 No label is just the empty label, behaving exactly like other labels. If we try to apply a labelled function to unlabelled arguments (with empty labels), reduction will be stuck. So this idea of "adding labels" during type checking, which results in this "slight" gap between the program and its untyped semantics: there is no ambiguity, but the program you reduce is not exactly the one you wrote (which would have been stuck anyway). So the warning is both for semantics purists, who want to be sure they can apply semantic rules directly on their source code, and label purists, who do not want to omit labels anyway. I suppose there are other ways to handle this, by extending a bit the semantics, but you would still need some kind of non-syntactic information, like the arity of f. > > * put some labels in alternative versions of a few libraries > > (List, Array, Unix). Access to these libraries would use already > > existing ways: "open Stdlabels", "module Unix = Lunix" > > * also add alternative labelled versions for the few functions with > > more than 4 arguments in the standard library (e.g. String.blit') > > Since these two points are the same, that is, provide alternative labeled > versions of some functions, could they be solved in the same way (introduce > a prime version of module M v.s. introduction primed definitions of > identifier f), so as to avoid dupplicating conventions. > > Also, before you chose names for the primed modules, can you find a uniform > convention (c.f. Stdlabels and Lunix that you keep using in examples). Or, > could these modules have the same name but be defined in a subdirectory of > the stdlib? I do not expect many of them, and I'm not even sure users will want to use labels everywhere simultaneously: labellings in List and Unix are rather different in nature. So they could happily stay in the main directory. Also having primes in module names may be problematic, if they are to be compilation units: any idea on how various operation systems handle primes in file names? I must admit I didn't seriously consider the problem of naming. We could probably find a solution among developpers. And a prerequisite is of course that this proposal (or a variant of it) gets accepted, which is not clear yet. Best regards, Jacques ------------------- To unsubscribe, mail caml-list-request@inria.fr. Archives: http://caml.inria.fr