Search code examples
ocamltype-inferencehindley-milner

Inferred type of an infinitely recursive function

For a loop like below:

let rec loop () = loop ()

the signature according to try.ocamlpro.com is:

val loop : unit -> 'a = <fun>

Why is this the case? loop() never stops calling itself so shouldn't it return anything?

Solution

  • I'm sure someone can, and will, explain exactly how this is inferred, but it is a property of the Hindley-Milner type system and its inference algorithm that it will be able to deduce the most general type of an expression. And that is of course 'a, which will unify with anything.

    So, just intuitively, if you start with the most general type, 'a, then try to find constraints that narrow it, you won't find anything in this case. The only expression that can constrain it is the recursive call, which we already assume is 'a, so there's no conflict.