Re: [Caml-list] Labels and polymorphism

["Nathaniel Gray" <n8gray@gmail.com>]

On 3/8/07, Roland Zumkeller <roland.zumkeller@gmail.com> wrote:
> On 08/03/07, Nathaniel Gray <n8gray@gmail.com> wrote:
> > # let f ~x = x;;
> > val f : x:'a -> 'a = <fun>
> > # f ~x:1;;
> > - : int = 1
> > # f 1;;
> > - : x:(int -> 'a) -> 'a = <fun>
>
> The "1" is assumed to be an argument to "f ~x:a" (where "a" is yet to
> be given). Therefore "f ~x:a" must be of type "int -> ...". Now "f
> ~x:a" is of the same type as (and here actually reduces to)  "a".
> Hence this type for the x-labeled argument.
>
> Perhaps looking at this might help, too:
> # f 1 1 1;;
> - : x:(int -> int -> int -> 'a) -> 'a = <fun>

Ok, I think maybe I've got it.  The problem is the equivalence between:
  let f ~x ~y = ...
and
  let f ~x = (fun ~y -> ... )

Or in other words, you have to understand that all functions in ocaml
have just one parameter (at least as far as the type system is
concerned), so "total application" is tricky to figure out.  The more
enlightening example, IMHO, is this one:

# let f ~x = x;;
val f : x:'a -> 'a = <fun>
# f 10 ~x:(fun x -> x+1);;
- : int = 11

In a multi-argument-function world the second line makes no sense.
Labeled arguments should allow you to rearrange the (multiple)
arguments of the current application, but not interleave them with
arguments from upcoming applications!  Enlightenment blossoms when you
realize that that's actually the thing that labeled arguments *do*
allow you to do.

Another helpful example:
# let f ~x = x;;
val f : x:'a -> 'a = <fun>
# let g ~y = f;;
val g : y:'a -> x:'b -> 'b = <fun>
# g ~x:3 ~y:5;;
- : int = 3

> Now you ask, why are things as they are? Why can't OCaml guess that
> the "1" was meant for the label "x"?
>
> Probably it could, but with such a typing rule we would have to write
> "(fun ~x:a -> f ~x:a 1)" for what is currently "f 1" (partial
> application would be essentially lost here). In contrast, becoming
> able to write "f x" instead of "f ~x:1" seems not enough of a gain to
> compensate this.

You could do it by using the rule that applying an unlabeled argument
in a labeled context always binds to that label, but applying a
labeled argument in an unlabeled context (or one where the labels
don't match) defers the application until the label is found.  (Maybe
this is what you're hinting at?)  So if you define f like this:
  let f a b ~c x ~y ~z = z
Then you could apply it in one of these ways:
  f 1 2 3 4 5 6
  f 1 2 3 4 ~z:6 ~y:5
  f ~c:3 ~z:6 1 2 4 5
But not this way:
  f 1 2 4 ~c:3 5 6  (* Too late -- c is already bound to 4 *)
  f 1 2 ~y:5 4 ~c:3 6  (* Ditto *)

As a practical matter you would probably want to label a suffix of
your arguments for maximum flexibility.  You would lose the ability to
do *some* (dare I say unimportant?) partial applications, but this
approach seems much more intuitive to me.  Mainly it has the advantage
that adding labels to a function would never break existing calls to
that function.  This property seems highly desirable to me -- so
desirable that I'm downright astonished it isn't already true.

Thanks for helping,
-n8

-- 
>>>-- Nathaniel Gray -- Caltech Computer Science ------>
>>>-- Mojave Project -- http://mojave.cs.caltech.edu -->