Re: [Caml-list] Labels and polymorphism

["Nathaniel Gray" <n8gray@gmail.com>]

On 3/18/07, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> 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 </: l for all j < i
     and l_i <: l

(Apologies if gmail destroyed the formatting on that.)

It's possible I'm not seeing some fatal flaw, but I believe this can
work just as well as the current system.  The only difference is when
labels are considered matching.

> 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 -->