Type Inference in OCaml

Question

I'm trying to wrap my head around OCaml's type inference notation.

For example:

# let f x = x [];; 
val f : ('a list -> 'b) -> 'b = <fun>

makes sense to me. The val f takes in a function x that takes in a list of 'a type and returns something of 'b type. Then f returns a 'b type as well since it just calls x.

However, once we get more arguments I get more confused.

# let g a b c = a b c;;
val g : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>

Can I assume that if the function has arguments, then the first parameters of the type inference will always be the arguments? And if I call a b c, is the order ((a b) c) or (a (b c))?

# let rec h m n ls = match ls with
  | [] -> n
  | x::t -> h m (m n x) t;;
val h : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a = <fun>

As for this one I'm confused as to how ('a -> 'b -> 'a) -> 'a was derived. I can see that 'b list corresponds to the ls variable and the last 'a corresponds to the type of the terminal symbol n.

Answer 1

Can I assume that if the function has arguments, then the first parameters of the type inference will always be the arguments?

Yes, the first parameter of function type is the type of its first argument.

And if I call a b c, is the order ((a b) c) or (a (b c))?

The order is ((a b) c) (you can think in this simpler way)

As for this one I'm confused as to how ('a -> 'b -> 'a) -> 'a was derived. I can see that 'b list corresponds to the ls variable and the last 'a corresponds to the type of the terminal symbol n.

You are right. ls has type 'b list and n has type 'a.

Let's think about the type of m:

1. You know n has type 'a, so you can derive (m n x) also has type 'a
2. You know ls has type 'b list, so you can derive x has type 'b
3. m takes two arguments of type 'a and type 'b, and produces result of type 'a. So, m has type 'a -> 'b -> 'a

Therefore, the whole function has type ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a