OCaml passing labeled function as parameter / labeled function type equivalence

Question

Suppose a function g is defined as follows.

utop # let g ~y ~x = x + y ;;
val g : y:int -> x:int -> int = <fun>
utop # g ~x:1 ;;
- : y:int -> int = <fun>
utop # g ~y:2 ;;
- : x:int -> int = <fun>
utop # g ~x:1 ~y:2 ;;
- : int = 3
utop # g ~y:2 ~x:1 ;;
- : int = 3

Now there is another function foo

utop # let foobar (f: x:int -> y:int -> int) = f ~x:1 ~y:2 ;;
val foobar : (x:int -> y:int -> int) -> int = <fun>

Sadly when I try to provide g as the parameter of foobar, it complains:

utop # foobar g ;;
Error: This expression has type y:int -> x:int -> int
       but an expression was expected of type x:int -> y:int -> int

This is quite surprising as I can successfully currify g but cannot pass it as the parameter. I googled and found this article which doesn't help much. I guess this is related to the underlying type system of OCaml (e.g. subtyping rules of labeled arrow types).

So is it possible to pass g as the parameter to foobar by any means in OCaml? If not, why is it not allowed? Any supporting articles/books/papers would be sufficient.

Answer 1

The key is that labels do not exist at runtime. A function of type X:int -> y:float -> int is really a function whose first argument is an int and whose second argument is a float.

Calling g ~y:123 means that we store the second argument 123 somewhere (in a closure) and we will use it automatically later when the original function g is finally called with all its arguments.

Now consider a higher-order function such as foobar:

let foobar (f : y:float -> x:int -> int) = f ~x:1 ~y:2.

(* which is the same as: *)
let foobar (f : y:float -> x:int -> int) = f 2. 1

The function f passed to foobar takes two arguments, and the float must be the first argument, at runtime.

Maybe it would be possible to support your wish, but it would add some overhead. In order for the following to work:

let g ~x ~y = x + truncate y;;
foobar g  (* rejected *)

the compiler would have to create an extra closure. Instead you are required to do it yourself, as follows:

let g ~x ~y = x + truncate y;;
foobar (fun ~y ~x -> g ~x ~y)

In general, the OCaml compiler is very straightforward and won't perform this kind of hard-to-guess code insertion for you.

(I'm not a type theorist either)

Answer 2

Think instead of the types x:int -> y:float -> int and y:float -> x:int -> int. I claim these are not the same type because you can call them without labels if you like. When you do this, the first requires an int as its first parameter and a float as the second. The second type requires them in the reverse order.

# let f ~x ~y = x + int_of_float y;;
val f : x:int -> y:float -> int = <fun>
# f 3 2.5;;
- : int = 5
# f 2.5 3;;
Error: This expression has type float but an expression was
expected of type int 

Another complication is that functions can have some labelled and some unlabelled parameters.

As a result, the labeled parameters of a function are treated as a sequence (in a particular order) rather than a set (without an inherent order).

Possibly if you required all parameters to be labelled and removed the capability of calling without labels, you could make things work the way you expect.

(Disclaimer: I'm not a type theorist, though I wish I was.)

Answer 3

This pitfall of labels in OCaml is described in detail in the Labels and type inference subsection of the OCaml manual, giving an example similar to yours.

If I remember correctly, some type systems for labels lift that restriction, but at the cost of additional overall complexity that was judged "not worth it" for the OCaml language itself. Labels can be rearranged automatically at first-order application sites, but not when abstracting over labelled functions (or using such abstractions).

You can have your example accepted by manually eta-expanding the labelled function to make a reorderable application appear (a type-theorist would say this is a retyping eta-conversion):

# let f ~x ~y = x+y;;
val f : x:int -> y:int -> int = <fun>
# let yx f = f ~y:0 ~x:1;;
val yx : (y:int -> x:int -> 'a) -> 'a = <fun>
# yx f;;
Error: This expression has type x:int -> y:int -> int
       but an expression was expected of type y:int -> x:int -> 'a
# yx (fun ~y ~x -> f ~y ~x);;
- : int = 1