Labels and polymorphism

Labels and polymorphism

[Nathaniel Gray]

I was recently bemoaning the way that folds (especially nested folds)
using longish anonymous functions become very hard to read, since the
argument order is optimized for greatest opportunity for partial
application rather than readability.  This led me to think about using
ListLabels in my code, but then I hit this bit of documentation:

"""
As an exception to the above parameter matching rules, if an
application is total, labels may be omitted. In practice, most
applications are total, so that labels can be omitted in applications.
...
But beware that functions like ListLabels.fold_left whose result type
is a type variable will never be considered as totally applied.
"""

Wha??  I'm trying to wrap my head around this but I'm just totally
confused.  I thought that playing around in the interpreter would
help, but it just left me more confused:

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

Can somebody make sense of this for me?  Is there a paper somewhere on
labels in ocaml that I should read?

Thanks,
-n8

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

Re: [Caml-list] Labels and polymorphism

[Eric Cooper]

On Thu, Mar 08, 2007 at 10:31:46AM -0800, Nathaniel Gray wrote:
> # let f ~x = x;;
> val f : x:'a -> 'a = <fun>
> # f ~x:1;;
> - : int = 1
> # f 1;;
> - : x:(int -> 'a) -> 'a = <fun>
> 
> Can somebody make sense of this for me?  Is there a paper somewhere on
> labels in ocaml that I should read?

Section 6.7.1 of the manual, subsection "Function application", says:
    As a special case, if the function has a known arity, all the
    arguments are unlabeled, and their number matches the number of
    non-optional parameters, then labels are ignored and non-optional
    parameters are matched in their definition order.

The problem is that if the result type of a function f is 'a, then
it's not of known arity -- an application of f could produce a
function, which could then be applied to more arguments.  For example:

# let id x = x;;
val id : 'a -> 'a = <fun>
# id id id id 17;;
- : int = 17

In your example, if you constrain the type of f, it works as expected:

# (f : x:int->int) 1;;
- : int = 1

-- 
Eric Cooper             e c c @ c m u . e d u

Re: [Caml-list] Labels and polymorphism

[Roland Zumkeller]

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>

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.

Best,

Roland

-- 
http://www.lix.polytechnique.fr/~zumkeller/

Re: [Caml-list] Labels and polymorphism

[skaller]

On Thu, 2007-03-08 at 10:31 -0800, Nathaniel Gray wrote:
> I was recently bemoaning the way that folds (especially nested folds)
> using longish anonymous functions become very hard to read, since the
> argument order is optimized for greatest opportunity for partial
> application rather than readability.  This led me to think about using
> ListLabels in my code, but then I hit this bit of documentation:
> 
> """
> As an exception to the above parameter matching rules, if an
> application is total, labels may be omitted. In practice, most
> applications are total, so that labels can be omitted in applications.
> ...
> But beware that functions like ListLabels.fold_left whose result type
> is a type variable will never be considered as totally applied.
> """
> 
> Wha??  I'm trying to wrap my head around this but I'm just totally
> confused.  I thought that playing around in the interpreter would
> help, but it just left me more confused:

It's simple:

# let id x = x;;
val id : 'a -> 'a = <fun>
# id 1;;
- : int = 1


id has arity 1 and is fully applied when it has one argument
right? 

# let f x = x * x;;
val f : int -> int = <fun>

# id f 2;;
- : int = 4

WOOPS! Here id has TWO arguments ...

So the arity of a function returning a type variable is
indeterminate, so you cannot tell if it is fully applied or not.

Hence the caveat.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] Labels and polymorphism

[Nathaniel Gray]

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 -->

Re: [Caml-list] Labels and polymorphism

[Jacques Garrigue]

From: "Nathaniel Gray" <n8gray@gmail.com>
[...]
> 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.

Sorry for the very late answer...

What about your idea. I could like it, but I see two problems.
The first one is that (as you point yourself) it requires that labeled
arguments come after unlabeled ones. If you look at the labelings in
ListLabels, you will see that generally the opposite is true: labeled
arguments come first. For instance, with your proposal it would become
impossible to write "ListLabels.map l ~f:(fun .........)", which is
one of the nice uses of labels.
There is a good reason for labeled arguments to come first: they are
the ones who provide useful partial applications. And it is generally
more efficient to do partial applications in the right order.
(Actually, one could argue that in a new language, we could choose a
different approach. But OCaml existed before labels, so this cannot be
easily changed in an existing language.)
The second problem is more fundamental: adding labels to a function
cannot be done without breaking compatibility. This is because
labels must match exactly when you pass a function as argument to
another function. So, while we want to make the use of labels not too
intrusive, it is impossible to make them completely transparent. This
reduces the relative value of a small increment in non-intrusiveness,
as it cannot be perfect anyway.

We could of course thing of other approaches, which would allow
out-of-order applications while being close to your proposal.
But first, a small word on why it is more complicated than it seems at
first sight. The difficulty is that we want the semantics not to
depend on types. That is, we should define a semantics for application
which works without looking at the type of the function applied. This
may seems contradictory, as the type must be known for compilation,
but this is a highly desirable property in a language where most types
are inferred. This may be annoying to have the compiler tell you that
some application is not allowed while it is semantically OK, but this
would be terrible if it accepted it, but resulted in an undefined
behaviour, depending on an hidden behaviour of type inference.

Finally, the rationale behind the current strategy is:
* keep full compatibility with a semantics where all labels would have
  to be always written. This semantics was used in early versions of
  ocaml, and is well understood.
* make it less intrusive by allowing ommiting labels in most
  applications (as long as this can be made compatible with the above
  semantics.)
This explains why this is not _all_ applications.
There could be other choices. This one privileges continuity. I don't
believe there is an ideal solution, as desired properties vary from
one person to another.

Jacques Garrigue

Re: [Caml-list] Labels and polymorphism

[Nathaniel Gray]

On 3/18/07, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
>
> Sorry for the very late answer...

Glad to have the reply!

> What about your idea. I could like it, but I see two problems.
> The first one is that (as you point yourself) it requires that labeled
> arguments come after unlabeled ones.

Well, it's not required, just practical.  Notice that in my example
the labeled arguments were not strictly a suffix.  The only
restriction is that it won't work to apply to a labeled argument after
an unlabeled argument has been applied in its position.

> If you look at the labelings in
> ListLabels, you will see that generally the opposite is true: labeled
> arguments come first. For instance, with your proposal it would become
> impossible to write "ListLabels.map l ~f:(fun .........)", which is
> one of the nice uses of labels.

Sure, but instead you could write "List.map ~l:l ~f:(fun ...)".  In
other words, if labels are truly optional at application-time, there's
no reason not to label everything, and there would be no reason for a
separate ListLabels module at all.

> There is a good reason for labeled arguments to come first: they are
> the ones who provide useful partial applications. And it is generally
> more efficient to do partial applications in the right order.
> (Actually, one could argue that in a new language, we could choose a
> different approach. But OCaml existed before labels, so this cannot be
> easily changed in an existing language.)

Hmm.  I don't see a connection between which arguments are labeled and
which will be partially applied.  These seem unrelated to me.

> The second problem is more fundamental: adding labels to a function
> cannot be done without breaking compatibility. This is because
> labels must match exactly when you pass a function as argument to
> another function.

I'm not sure I accept this.  What I would like is a subtyping relation
between labeled and unlabeled functions.  A function with labels is a
subtype of the label-erased (or partially label-erased) version of
that function.  Is there some reason this is not possible?

> We could of course thing of other approaches, which would allow
> out-of-order applications while being close to your proposal.
> But first, a small word on why it is more complicated than it seems at
> first sight. The difficulty is that we want the semantics not to
> depend on types. That is, we should define a semantics for application
> which works without looking at the type of the function applied. This
> may seems contradictory, as the type must be known for compilation,
> but this is a highly desirable property in a language where most types
> are inferred. This may be annoying to have the compiler tell you that
> some application is not allowed while it is semantically OK, but this
> would be terrible if it accepted it, but resulted in an undefined
> behaviour, depending on an hidden behaviour of type inference.

The behavior I'm arguing for doesn't depend on types (at least no more
so than the current behavior).  I've actually taken a look at some of
your papers on the topic so I can be a little more precise in my
description.  Start by defining a slightly different "matches"
relation on labels, with two axioms:

axiom 1:  l <: l
Any label matches itself.

axiom 2:  * <: l
Star matches any label (including itself).

Note that it is *not* the case that l <: * (the relation is not
symmetric).  Unlabeled arguments and parameters are considered to be
labeled with star.  Now the beta-reduction rule is:

(...((fun ~l:x -> e) ~l_1:e_1 ...) ... ~l_i:e_i ... ~l_n:e_n)
-->
(...(e[e_i/x] ~l_1:e_1 ...) ... ~l_{i-1}:e_{i-1} ~l_{i+1}:e_{i+1} ... ~l_n:e_n)
     when l_j </: l for all j < i
     and l_i <: l

(Apologies if gmail destroyed the formatting on that.)

It's possible I'm not seeing some fatal flaw, but I believe this can
work just as well as the current system.  The only difference is when
labels are considered matching.

> Finally, the rationale behind the current strategy is:
> * keep full compatibility with a semantics where all labels would have
>   to be always written. This semantics was used in early versions of
>   ocaml, and is well understood.
> * make it less intrusive by allowing ommiting labels in most
>   applications (as long as this can be made compatible with the above
>   semantics.)
> This explains why this is not _all_ applications.
> There could be other choices. This one privileges continuity. I don't
> believe there is an ideal solution, as desired properties vary from
> one person to another.

Sure, there are always historical, social, and practical reasons a
language evolves the way it does.  I'm just frustrated because I want
to use labels but I can't "open StdLabels" at the top of my files (or
more to the point, my lab's files) without breaking things.

Thanks,
-n8

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

Re: [Caml-list] Labels and polymorphism

[Jacques Garrigue]

From: "Nathaniel Gray" <n8gray@gmail.com>

> > The second problem is more fundamental: adding labels to a function
> > cannot be done without breaking compatibility. This is because
> > labels must match exactly when you pass a function as argument to
> > another function.
> 
> I'm not sure I accept this.  What I would like is a subtyping relation
> between labeled and unlabeled functions.  A function with labels is a
> subtype of the label-erased (or partially label-erased) version of
> that function.  Is there some reason this is not possible?

Just that subtyping doesn't play well with type inference.
This is why subtyping for objects is completely explicit.
As a result, while your subtyping-based approach seems sound, it
would still not allow transparent addition of labels, as one would
have to add coercions to "remove" labels from function types.

Note also that your subtyping approach is weaker than your earlier
proposal: out-of-order application is only allowed when all formal
parameters are labeled. And this doesn't take optional arguments into
account.  This said, this could be a nice proposal for labeled
arguments in Java, for instance.

Jacques Garrigue