Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Re: Syntax for label
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2000-04-02 (21:34)
From: Jacques Garrigue <garrigue@k...>
Subject: Re: Semantic of label: The best (only ?) solution to merge both mode
From: John Max Skaller <>

> 	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

Another one is that there is a whole bunch of theoretical properties
that must be kept.  Maybe you don't even know about them, but this is
thanks to them that you can be confident when the compiler tells you
that your program is OK. (At least much more confident than in weakly
typed languages.)

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)

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.

        let l = [output oc; Buffer.add_substring b];;

This must work for backward compatibility (1).
What type shall we give to l? There's no unique answer, and this is
actually the case that the classic mode will give you either
(buf:string -> ...) list or (string -> ...) list depending on the
order in which you listed the functions.
This is not a problem since in classic mode you will anyway have to
consume arguments in a fixed order, and labels are just a decoration.
(For label check to work properly (in theory), you must use it only on
function whose type is known, as are all library functions.)

Now suppose you base yourself on this non-deterministic type
information to reorder arguments by commutation according to the
labels given in the application (2).
Well, this is as you would expect, anything can happen.
Including the compiler passing parameters in the wrong order and not
telling you anything about the commutation done!
More generally, I can also write:
        let l' : (string -> len:int -> pos:int -> unit) list = l;;
Since labels have to be ignored during unification, this must be
Now, what will be the outcome of this application?
        (List.hd l') "Hello" pos:1 len:2
"l", not "el" as it should.

So, please do not ask for something that is just plain impossible.
Classic mode is already providing the maximum one can expect:
* backward compatibility
* commutation for optional arguments
* fully transparent (and yet useful) labels for non-optional ones
This is the default mode, and would have been probably the only one
if olabl had not existed.

Now, the commuting label mode is just for those who are ready
to change a bit their habits.
And since it is my personal creation (with others), I will just
refrain from explaining why it is so wonderfully clean theoretically.

Best regards,

Jacques Garrigue      Kyoto University     garrigue at
		<A HREF=>JG</A>