From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.0 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id BCE40BC6B for ; Tue, 20 Mar 2007 00:53:20 +0100 (CET) Received: from wr-out-0506.google.com (wr-out-0506.google.com [64.233.184.228]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l2JNrJGi007236 for ; Tue, 20 Mar 2007 00:53:20 +0100 Received: by wr-out-0506.google.com with SMTP id 60so1739910wri for ; Mon, 19 Mar 2007 16:53:19 -0700 (PDT) DKIM-Signature: a=rsa-sha1; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=prpystArv6m0EoaZU/qM3xkBvNHEOggjoyMPHJoOd8xD3fenG3Y0aqVOb8mzYzsIkckOrohUkZPnX5zO9QwMcaVR7kt+EtLYXhgbSCE5ozRjwbjQ34paoJBdl6vnPSfXOi2fh8/I8QGo2bBiBhIVSv/z5HdHpjUvfIYa32DyJIY= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=Svuvn0z0xaRbQG4OZtMzOe8m0wVPuyxRnJy0LVQMwi1QicP3eOFDPTHBooqFIqvBMXfQA+bFAyryV5Qpfzi1DNknxRYmDN44vAFhNNQQnxoIpuQX822oJUfJb85Gc+CYT2lam4fVQbtVDotyDnDLapReo/DF+W7Wt05oFEbY2eo= Received: by 10.90.113.20 with SMTP id l20mr170345agc.1174348398956; Mon, 19 Mar 2007 16:53:18 -0700 (PDT) Received: by 10.115.54.13 with HTTP; Mon, 19 Mar 2007 16:53:18 -0700 (PDT) Message-ID: Date: Mon, 19 Mar 2007 16:53:18 -0700 From: "Nathaniel Gray" To: "Jacques Garrigue" Subject: Re: [Caml-list] Labels and polymorphism Cc: caml-list@inria.fr In-Reply-To: <20070319.101500.03115026.garrigue@math.nagoya-u.ac.jp> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <20070319.101500.03115026.garrigue@math.nagoya-u.ac.jp> X-j-chkmail-Score: MSGID : 45FF226F.000 on concorde : j-chkmail score : X : 0/20 1 0.000 -> 1 X-Miltered: at concorde with ID 45FF226F.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; polymorphism:01 listlabels:01 listlabels:01 ocaml:01 subtyping:01 subtype:01 semantics:01 semantics:01 compilation:01 compiler:01 semantically:01 inference:01 axioms:01 symmetric:01 ocaml:01 On 3/18/07, Jacques Garrigue wrote: > > Sorry for the very late answer... Glad to have the reply! > What about your idea. I could like it, but I see two problems. > The first one is that (as you point yourself) it requires that labeled > arguments come after unlabeled ones. Well, it's not required, just practical. Notice that in my example the labeled arguments were not strictly a suffix. The only restriction is that it won't work to apply to a labeled argument after an unlabeled argument has been applied in its position. > If you look at the labelings in > ListLabels, you will see that generally the opposite is true: labeled > arguments come first. For instance, with your proposal it would become > impossible to write "ListLabels.map l ~f:(fun .........)", which is > one of the nice uses of labels. Sure, but instead you could write "List.map ~l:l ~f:(fun ...)". In other words, if labels are truly optional at application-time, there's no reason not to label everything, and there would be no reason for a separate ListLabels module at all. > There is a good reason for labeled arguments to come first: they are > the ones who provide useful partial applications. And it is generally > more efficient to do partial applications in the right order. > (Actually, one could argue that in a new language, we could choose a > different approach. But OCaml existed before labels, so this cannot be > easily changed in an existing language.) Hmm. I don't see a connection between which arguments are labeled and which will be partially applied. These seem unrelated to me. > The second problem is more fundamental: adding labels to a function > cannot be done without breaking compatibility. This is because > labels must match exactly when you pass a function as argument to > another function. I'm not sure I accept this. What I would like is a subtyping relation between labeled and unlabeled functions. A function with labels is a subtype of the label-erased (or partially label-erased) version of that function. Is there some reason this is not possible? > We could of course thing of other approaches, which would allow > out-of-order applications while being close to your proposal. > But first, a small word on why it is more complicated than it seems at > first sight. The difficulty is that we want the semantics not to > depend on types. That is, we should define a semantics for application > which works without looking at the type of the function applied. This > may seems contradictory, as the type must be known for compilation, > but this is a highly desirable property in a language where most types > are inferred. This may be annoying to have the compiler tell you that > some application is not allowed while it is semantically OK, but this > would be terrible if it accepted it, but resulted in an undefined > behaviour, depending on an hidden behaviour of type inference. The behavior I'm arguing for doesn't depend on types (at least no more so than the current behavior). I've actually taken a look at some of your papers on the topic so I can be a little more precise in my description. Start by defining a slightly different "matches" relation on labels, with two axioms: axiom 1: l <: l Any label matches itself. axiom 2: * <: l Star matches any label (including itself). Note that it is *not* the case that l <: * (the relation is not symmetric). Unlabeled arguments and parameters are considered to be labeled with star. Now the beta-reduction rule is: (...((fun ~l:x -> e) ~l_1:e_1 ...) ... ~l_i:e_i ... ~l_n:e_n) --> (...(e[e_i/x] ~l_1:e_1 ...) ... ~l_{i-1}:e_{i-1} ~l_{i+1}:e_{i+1} ... ~l_n:e_n) when l_j Finally, the rationale behind the current strategy is: > * keep full compatibility with a semantics where all labels would have > to be always written. This semantics was used in early versions of > ocaml, and is well understood. > * make it less intrusive by allowing ommiting labels in most > applications (as long as this can be made compatible with the above > semantics.) > This explains why this is not _all_ applications. > There could be other choices. This one privileges continuity. I don't > believe there is an ideal solution, as desired properties vary from > one person to another. Sure, there are always historical, social, and practical reasons a language evolves the way it does. I'm just frustrated because I want to use labels but I can't "open StdLabels" at the top of my files (or more to the point, my lab's files) without breaking things. Thanks, -n8 -- >>>-- Nathaniel Gray -- Caltech Computer Science ------> >>>-- Mojave Project -- http://mojave.cs.caltech.edu -->