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)