Re: Semantic of label: The best (only ?) solution to merge both mode

From: Jacques Garrigue (garrigue@kurims.kyoto-u.ac.jp)
Date: Fri Mar 31 2000 - 06:34:29 MET DST

  • Next message: Dmitri Lomov: "Emacs indentation fo OCaml"

    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.

    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
    accepted.
    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
    ---------------------------------------------------------------------------
    Jacques Garrigue Kyoto University garrigue at kurims.kyoto-u.ac.jp
                    <A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>



    This archive was generated by hypermail 2b29 : Sun Apr 02 2000 - 23:38:17 MET DST