Value restriction and mutually recursive functions

The short answer is that OCaml has the restriction that a recursive function let rec f = e₁ in e₂ cannot be polymorphically-recursive: that is, it can only be used with a single type within its own definition (e₁) . Mutually-recursive functions let f₁ = e₁ and f₂ = e₂ ... have a corresponding restriction: every function fᵢ in the group can only be used with a single type in the definitions eᵢ. The reason for the restriction is that type inference for polymorphic recursion is undecidable in the general case.

However, although type inference for polymorphic recursion is undecidable, type checking (i.e. when the types are already known) is fine, so the second program will pass type checking if aux is annotated with a suitable polymorphic type. The following is accepted:

let rec aux : 'a. 'a -> int = fun x -> 100
and main () = (aux 1) + (aux true)

Fritz Henglein’s 1993 paper Type inference with polymorphic recursion is the place to look for the details about undecidability. Most references on ML type inference, from Milner’s 1978 paper to Pierce’s book (end of chapter 22) are likely to touch on the restriction briefly.

7 Likes