OCaml's rectype inference

Question

While playing with -rectypes option of OCaml at some point I'm just lost.

This expression is pretty much typable:

# fun x -> x x;;
- : ('a -> 'b as 'a) -> 'b = <fun>

But here OCaml fell in infinite loop:

# (fun x -> x x) (fun x -> x x);;
  C-c C-cInterrupted.

Ok, I can understand, recursive type system is a quite difficult thing. But first of all, I really want to know the type of this expression and does it typable at all, and secondly, in this context, I don't understand how OCaml still can type this:

# fun _ -> (fun x -> x x) (fun x -> x x);;
- : 'a -> 'b = <fun>

So, can someone elaborate a bit on this topic?

Answer 1

Let's first try to evaluate your expression.

# (fun x -> x x) (fun x -> x x);;
# let x = (fun x -> x x) in x x;; (* applying the function on the left *)
# (fun x -> x x) (fun x -> x x);; (* inlining the let-binding *)
(* We came back to our original state, infinite loop *)

So the infinite loop doesn't come from the typing system, but from the semantics of the expression you gave it to.

You can get the type of an expression without evaluating it using ocamlc -i

$ echo 'let x = (fun x -> x x) (fun x -> x x)' > rectypes.ml
$ ocamlc -i -rectypes rectypes.ml                                                                                                                                                                                                           
val x : 'a

So here it is, you created a value of type 'a (which usually means "this expression never returns").

Note that you can do the same kind of trick without using rectypes:

# let x =
   let rec f () = f () in
   f ();;

As you can understand now, your last bit of code takes any argument and never returns, hence the 'a -> 'b type.