CODEWITHSUNDEEP
ocamltype-inferencehindley-milner
Kevin Wu
Kevin Wu

Reputation: 1467

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?

Upvotes: 1

Views: 135

Answers (2)

glennsl
glennsl

Reputation: 29106

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.

Upvotes: 4

Alexey Romanov
Alexey Romanov

Reputation: 170713

Yes, it should, and that's exactly what unit -> 'a means: given any type 'a the caller asks for, the function promises to return an 'a.

Upvotes: 4

Related Questions