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

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

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