let rec for values and let rec for functions in ocaml

Question

What is the best intuition for why the first definition would be refused, while the second one would be accepted ?

let rec a = b (* This kind of expression is not allowed as right-hand side of `let rec' *)
and b x = a x

let rec a x = b x (* oki doki *)
and b x = a x

Is it linked to the 2 reduction approaches : one rule for every function substitution (and a Rec delimiter) VS one rule per function definition (and lambda lifting) ?

Answer 1

Verifying that recursive definitions are valid is a very hard thing to do.

Basically, you want to avoid patterns in this kind of form:

let rec x = x

In the case where every left-hand side of the definitions are function declarations, you know it is going to be fine. At worst, you are creating an infinite loop, but at least you are creating a value. But the x = x case does not produce anything and has no semantic altogether.

Now, in your specific case, you are indeed creating functions (that loop indefinitely), but checking that you are is actually harder. To avoid writing a code that would attempt exhaustive checking, the OCaml developers decided to go with a much easier algorithm.

You can have an outlook of the rules here. Here is an excerpt (emphasis mine):

It will be accepted if each one of expr1 … exprn is statically constructive with respect to name1 … namen, is not immediately linked to any of name1 … namen, and is not an array constructor whose arguments have abstract type.

As you can see, direct recursive variable binding is not permitted.

This is not a final rule though, as there are improvements to that part of the compiler pending release. I haven't tested if your example passes with it, but some day your code might be accepted.