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

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

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>