Type inference with mutual recursion

Question

I've been thinking about how type inference works in the following OCaml program:

let rec f x = (g x) + 5
and g x = f (x + 5);;

Granted, the program is quite useless (looping forever), but what about the types? OCaml says:

val f : int -> int = <fun>
val g : int -> int = <fun>

This would exactly be my intuition, but how does the type inference algorithm know this?

Say the algorithm considers "f" first: the only constraint it can get there is that the return type of "g" must be "int", and therefore its own return type is also "int". But it cannot infer the type of its argument by the definition of "f".

On the other hand, if it considers "g" first, it can see that the type of its own argument must be "int". But without having considered "f" before, it can't know that the return type of "g" is also "int".

What is the magic behind it?

Answer 1

Say the algorithm considers "f" first: the only constraint it can get there is that the return type of "g" must be "int", and therefore its own return type is also "int". But it cannot infer the type of its argument by the definition of "f".

It can't infer it to a concrete type, but it can infer something. Namely: the argument type of f must be the same as the argument type of g. So basically after looking at f, ocaml knows the following about the types:

for some (to be determined) 'a:
f: 'a -> int
g: 'a -> int

After looking at g it knows that 'a must be int.

For a more in-depth look on how the type inference algorithm works, you can read the Wikipedia article about Hindley-Milner type inference or this blog post, which seems to be much friendlier than the Wikipedia article.

Answer 2

Here is my mental model of what goes on, which may or may not match reality.

let rec f x =

Ok, at this point we know that f is a function that takes argument x. Thus we have:

f: 'a -> 'b
x: 'a

for some 'a and 'b. Next:

(g x)

Ok, now we know g is a function that can be applied to x, so we add

g: 'a -> 'c

to our list of information. Continuing...

(g x) + 5 

Aha, the return type of g must be int, so now we have solved 'c=int. At this point we have:

f: 'a -> 'b
x: 'a
g: 'a -> int

Moving on...

and g x =

Ok, there's a different x here, let's assume the original code had y instead, to keep things more obvious. That is, let's rewrite the code as

and g y = f (y + 5);; 

Ok, so we are at

and g y = 

so now our info is:

f: 'a -> 'b
x: 'a
g: 'a -> int
y: 'a

since y is an argument to g... and we keep going:

f (y + 5);; 

and this tells us from y+5 that y has type int, which solves 'a=int. And since this is the return value of g, which we already know must be int, this solves 'b=int. That was a lot in one step, if the code were

and g y = 
    let t = y + 5 in
    let r = f t in
    f r;; 

then the first line would show y is an int, thus solving for 'a, and then the next line would say that r has type 'b, and then the final line is the return of g, which solves 'b=int.