Value restriction and mutually recursive functions

Learning
1

Hi,

The following code is well typed:

let main () =

  let aux x = 100 in

  (aux 1) + (aux true)

let _ =

  print_int (main ())

But the following isn’t:

let rec aux x = 100

and main () =

  (aux 1) + (aux true)

let _ =

  print_int (main ())

I would say that there’s some value restriction going on here, but I’m used to that when I’m using references. I’m trying to understand the reason why this is not possible, I kinda have the intuition, but I’m looking for a more formal answer, so I’d like to know if there’s a research paper explaining what’s going on in that kind of cases ?

Cheers !

2

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
3

Thanks, that’s what I was looking for.

So, I get your example working, and indeed, if I remove type annotations it doesn’t work anymore. But, this one is not working:

let rec aux (x : 'a) : int = 42
and main () = (aux 1) + (aux true)

Which makes me feel like there’s not only the problem of type inference, but also something else going on, my guess would be that it’s about the way recursive closures are handled by the compiler. Do you have an explanation for this ?

4

The root issue is that your annotation is less explicit. A small example of the problem is

let sum: 'a -> 'b -> 'c = fun x y -> x + y

Notice that the typechecker is happy with sum even if its type is in fact int -> int -> int and not a polymorphic type , something like for all 'a, 'b and 'c, 'a -> 'b -> 'c . The reason is that 'a, 'b and 'c are unification type variables that can be freely unified with any concrete type. So going from 'a -> 'b -> 'c to int -> int -> int is perfectly valid.

Thus in your case, the the type of aux : 'a -> int is unified to aux: int -> int at the first call of aux 1. Consequently aux true fails with

Error: This expression has type bool but an expression was expected of type int

This is why it is necessary to use an explicit polymorphic annotation (or universal quantification). Going back to my toy example, this means writing

let sum: 'a 'b 'c. 'a -> 'b -> 'c = fun x y -> x + y

with this explicit annotation, the typechecker fails with an error

Error: This definition has type int → int → int which is less general than
'a 'b 'c. 'a → 'b → 'c

Here, 'a 'b 'c. 'a -> 'b -> 'c is the OCaml syntax for for all types 'a, 'b, 'c. sum: 'a -> 'b -> 'c . Thus the typechecker knows that you intended the function to be polymorphic and can fail here.

Similarly with the explicit polymorphic annotation

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

the typechecker knows from the definition that aux is polymorphic in its first argument and that it should not deduce that aux:int -> _ from the call aux 1 .

See also the manual .

3 Likes