Jacques Garrigue wrote:
> From: John Max Skaller <skaller@maxtal.com.au>
> 
> >       This gives the olabl people their old labels back,
> > while merely requiring classic uses to decorate definitions
> > with labels. In this case a temporary compiler mode switch
> > to allow classic users to upgrade piecemeal would be ideal.
> >
> >       To me, this proposal appeals. (Will it work? Do I understand it?)
> 
> OK, I think that the problem is that the people do not understand all
> the constraints which must be fulfilled by the label system.
> 
> One is that we must keep compatibility with non-labelled mode,
> virtually forever.  We just cannot force anybody to switch to labelled
> mode.  We are talking about ML, not a new language starting from
> scratch.

	My programs in ocaml are NOT ML programs.
They're ocaml programs. I use objects (classes), for example,
which are not available in ML.

> Now the answer is very short: you cannot provide simultaneously (in
> the same mode)
> 1) backward compatibility
> 2) commutation of (non-optional) labels
> 3) labels as documentation (that is, anywhere you feel like putting them)

	Of course. So we throw out both (1) and (3). The proposal is that
USE of functions be compatible, but not definition.

	I will show the effect on your example:
 
> Here is a proof of that.
> Suppose you have two functions with same types but different labels
> in the standard library (3 above). A good example of that is
> 
> Pervasives.output: out_channel -> buf:string -> pos:int -> len:int -> unit
> Buffer.add_substring: Buffer.t -> string -> pos:int -> len:int -> unit
> 
> If you apply them both on their first argument, you obtain functions
> whose difference is limited to labels.
> Now, you could want to put these functions in a list.

	You can't. They have a different type. The labels are not
decoration. For two function types to agree, they must have the same
number of parameters, all labelled in the same order, with the same type
and label.
So when it comes to typing functions, the interpretation is strict:
labels are mandatory: Pervasives.output as given is not a valid
function type. 

	Lets retry with definitons:

output: chan:out_channel -> buf:string -> pos:int -> len:int -> unit
add_substring: buf:Buffer.t -> substr:string -> pos:int -> len:int ->
unit
 
>         let l = [output oc; Buffer.add_substring b];;

	with the labels given above, the SHOULD fail.
We WANT it to fail. it is an error well detected by the fact that
not only must the types agree, but also the labels must agree.
This requires a parameter be associated with a label which has
a coherent 'kinding' meaning IN ADDITION to the usual type information.

	It is this very kinding which prevents mixing up the
position and length arguments.

> This must work for backward compatibility (1).

	It will work IF and ONLY IF the labels of the two
functions agree.

	Suppose I have a function f (p1:a1 : int) (p2:a2 : int) : int,
and I want to fold it with

	fold_left 
	(fn:f : (x1:a1 : int) (x2:a2 : int) : int) 
	(acc:a : int)
	(ls:l : int list)
	: int

Here, saying 'fold_left fn:f' will not work, since the labels are
in disagreement. We can fix this by redefining the function
to have the right labels:

	let f2 (x1:a1) (x2:a2) = f p1:a1 p2:a2
	fold_left fn:f2 (* OK now *)

This is a 'kinding' coercion. It is messy to have to redefine the
function like this, we need a short hand syntax like:

	fold_left (f<x1:=p1,x2:=p2>)

this syntax is typechecked, and f is passed 'as if' it had labels x1:
and x2:
instead of p1: and p2: (that is, this really is a type conversion, since
labels are part of type information now).

There's no doubt this will BREAK every function I have written.
It isn't compatible with (either) classic or modern mode.

However, the mandatory 'relabelling' of function labels exhibited above
is good, since it exhibits what amounts to a paradigm shift 
(changing the labelling framework) physically in the code.

This WILL produce some extra 'clutter', but one can argue it only
appears when two incompatible labelling schemes must be 
made compatible.

As usual, a stricter typing regime has problems that one sometimes
finds the typing _overly_ strict, but this is always true for any
static type system I've seen (and at the same time, it is not strict
enough .. :-)

Is this a good compromise? I don't know. 
If the ocaml team wants to keep (1) compatibility, then the answer is
no.
I'm just following Einstein's principle: if you have a difficult
to prove property you want, make it an axiom, and try adjusting
the existing ones, instead of handing on to them.

-- 
John (Max) Skaller, mailto:skaller@maxtal.com.au
10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850
checkout Vyper http://Vyper.sourceforge.net
download Interscript http://Interscript.sourceforge.net