Re: [Caml-list] Future of labels, and ideas for library labelling

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

[ 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