6

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) ?

nicolas
  • 9,549
  • 3
  • 39
  • 83
  • I think this is caused by [the value restriction](https://stackoverflow.com/questions/22507448/the-value-restriction) and explicitly passing the argument is called eta expansion. I have no idea how to explain this in any way that is intuitive though. – glennsl Nov 16 '18 at 11:13
  • me neither. it's a tad annoying compared to haskell, although I am sure there are very good reason for that.. – nicolas Nov 16 '18 at 14:24

1 Answers1

6

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 expr1exprn is statically constructive with respect to name1namen, is not immediately linked to any of name1namen, 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.

PatJ
  • 5,996
  • 1
  • 31
  • 37