Ocaml's named parameters

Trying to understand Ocaml's mechanism for named parameters. I understand the basics, but the doc shows an example like this:

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

# let x = 3 and y = 2 in f ~x ~y;;
- : int = 1

What exactly is going on when only the tilde is used in application? Is it just shorthand for ~x:x, similar to definitions? If so, can someone explain why this:

# ListLabels.fold_left;;
- : f:('a -> 'b -> 'a) -> init:'a -> 'b list -> 'a = <fun>

# let add = (+) and i = 0 
in ListLabels.fold_left ~add ~i [1;2;3];;

produces

- : f:((add:(int -> int -> int) -> i:int -> 'a) ->
   int -> add:(int -> int -> int) -> i:int -> 'a) ->
init:(add:(int -> int -> int) -> i:int -> 'a) -> 'a = <fun>

Solution

The man says "beware that functions like ListLabels.fold_left whose result type is a type variable will never be considered as totally applied."

Here is what happens in your example. Beware it's a bit involved.

# ListLabels.fold_left;;
- : f:('a -> 'b -> 'a) -> init:'a -> 'b list -> 'a = <fun>

is just the classic use: ListLabels.fold_left taks 3 arguments, namely a function labeled f, an initializer init and a list.

Now, in

let add = (+) and i = 0 
in ListLabels.fold_left ~add ~i [1;2;3];;

the application ListLabels.fold_left ~add ~i [1;2;3] is considered incomplete (as the man says). That means that `ListLabels.fold_left receives first its unamed argument, [1;2;3] and returns a function of type f:('a -> int -> 'a) -> init:'a -> 'a. Let us call this function foo.

Since you're giving two named arguments, labeled add and i, the type 'a is inferred to be a functional type, of type add:'c -> ~i:'d -> 'e.

Based on the type of the variables add and i, the type 'c must be int -> int -> int, and 'd must be int.

Replacing those values in the type 'a, we derive that the type 'a is add:(int -> int -> int) -> i:int -> 'e. And replacing this in the type of foo (I'm glad there is copy-pasting ;-), its type is

f:((add:(int -> int -> int) -> i:int -> 'e)
    -> int
    -> (add:(int -> int -> int) -> i:int -> 'e))
-> init:(add:(int -> int -> int) -> i:int -> 'e)
-> (add:(int -> int -> int) -> i:int -> 'e)

Removing unecessary parentheses, and alpha converting (i.e. renaming) 'e to 'a, we get

f:((add:(int -> int -> int) -> i:int -> 'a)
    -> int
    -> add:(int -> int -> int) -> i:int -> 'a)
-> init:(add:(int -> int -> int) -> i:int -> 'a)
-> add:(int -> int -> int) -> i:int -> 'a

That is the type of foo. But remember that you are passing two arguments to foo, labeled ~add and ~i. So the value you get at the end is not of type add:(int -> int -> int) -> i:int -> 'a but indeed of type 'a. And the whole type of your example is, as returned by the compiler,

f:((add:(int -> int -> int) -> i:int -> 'a)
    -> int
    -> add:(int -> int -> int) -> i:int -> 'a)
-> init:(add:(int -> int -> int) -> i:int -> 'a)
-> 'a