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

From: Jacques Garrigue (garrigue@kurims.kyoto-u.ac.jp)
Date: Tue Apr 04 2000 - 07:50:25 MET DST

  • Next message: Jacques Garrigue: "Re: to have labels or not"

    From: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>

    > Let's only talk about the modern mode !
    >
    > I wanted to really use commuting labels, I was ready to change my habit,
    > but I found them to restrictive. I find my proposal, which is just to
    > change a bit the semantics of function application (and nothing else) on
    > non-labelled arguments quite nice and useful (no need to always remember
    > all the label names if you prefer to remember the order of the
    > arguments).

    * They are (a bit) restrictive. This is intentional.
      (Still, there will be less labels in the standard library in 3.00.)
      Experience with olabl shows that non-optional labels are more useful
      as documentation than for commutation. If you don't have to write
      them, you will probably not write them, and you loose the benefit.
      Sometimes you have to be forced to do things that are good for you :-)
      And please do not compare this with ADA: these are only a few more
      characters, in an already very compact language.

    * For you this is just a matter of remembering either position or
      labels. But if someone is to read your code, he will have to switch
      from one to the other at each application, according to the one you
      choosed. Not so nice.

    > As my proposal only cost to change about 20 lines why not have an option
    > to the modern mode to let people try it for real and see what they think
    > ?

    This is not a problem of number of lines.
    Before putting even one line of code in the type checker, we have to
    be sure it is not breaking anything in the language.
    I asked you to produce
    1) type inference rules (which must mix with the rest of the language)
    2) an untyped reduction semantics, including optional arguments
       (you cannot use the type of the function to decide how it should
        be evaluated, only its value)
    These are pre-conditions.
    If you do not produce these, this is just an idea, not a proposal.
    And I don't see why I should do the work for you, since I am satisfied
    with the current system.

    > About the "so wonderfully clean theoretically" .. it is not so clear:
    > look at this example:
    >
    > > lama-d134:~> ocaml -modern
    > > Objective Caml version 2.99 (99/12/08)
    > >
    > > # let h f = f x:1 y:2;;
    > > val h : (x:int -> y:int -> 'a) -> 'a = <fun>
    > > # let h f = f y:1 x:2;;
    > > val h : (y:int -> x:int -> 'a) -> 'a =
    > > <fun>
    > >
    > > The infered type depends on the way you write thing while one could think
    > > they are equivalent (the labels commute in modern mode, don't they ?)

    This is just an example of how keeping the theory clean may force you
    to weaken the implementation.
    In olabl those two types were to a great extent equivalent, but this
    resulted in breaking the call-by-value semantics in some special
    cases. We add to back on this.
    If you really want those two types to be equivalent, you will have to
    pay (probably a lot) in terms of efficiency. Considering that
    commutation is not very useful in this particular case, it is better
    to have the compiler refuse this code than turn it into an innefficient
    blurb. Call it a trade-off. Not between theory and practice, just
    between power and efficiency.

    Regards,

    Jacques Garrigue
    ---------------------------------------------------------------------------
    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 : Thu Apr 06 2000 - 15:23:53 MET DST