пусть rec для значений и пусть rec для функций в ocaml

Question

Какова лучшая интуиция, почему первое определение будет отклонено, а второе будет принято?

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

Связано ли это с 2 подходами сокращения: одно правило для каждой подстановки функции (и разделитель Rec) VS одно правило для определения функции (и лямбда-лифтинг)?

Answer 1

Проверка правильности рекурсивных определений - очень сложная задача.

По сути, вам нужно избегать шаблонов в такой форме:

let rec x = x

В случае, когда каждыйлевая часть определений - это объявления функций, вы знаете, что все будет хорошо.В худшем случае вы создаете бесконечный цикл, но по крайней мере вы создаете значение.Но случай x = x ничего не производит и не имеет вообще никакой семантики.

Теперь, в вашем конкретном случае вы действительно создаете функции (которые зацикливаются на неопределенный цикл), но проверить, что вы на самом деле сложнее.Чтобы избежать написания кода, который попытался бы провести исчерпывающую проверку, разработчики OCaml решили использовать гораздо более простой алгоритм.

Вы можете ознакомиться с правилами здесь .Вот выдержка (выделено мной):

Будет принято, если каждый из expr1… exprn является статически конструктивным по отношению к name1… namen, не сразу связывается ни с одним из name1… namen и не является конструктором массива, аргументы которого имеют абстрактный тип.

Как видите, прямое рекурсивное связывание переменных не являетсяразрешено.

Это не окончательное правило, поскольку в этой части компилятора есть улучшения , ожидающие выпуска .Я не проверял, соответствует ли ваш пример этому, но однажды ваш код может быть принят.