让我们记住值,并让我们记住ocaml中的函数

nic*_*las 5 ocaml

为什么第一个定义会被拒绝的最佳直觉是什么,而第二个定义会被接受?

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
Run Code Online (Sandbox Code Playgroud)

它是否与2种减少方法相关联:每个函数替换(和Rec定界符)的一个规则VS每个函数定义一个规则(和lambda提升)?

Pat*_*atJ 5

验证递归定义是否有效是一件非常困难的事情.

基本上,您希望避免使用这种形式的模式:

let rec x = x
Run Code Online (Sandbox Code Playgroud)

在定义的每个左侧都是函数声明的情况下,您知道它会没问题.在最坏的情况下,您正在创建一个无限循环,但至少您正在创建一个值.但是这个x = x案子并没有产生任何东西,也没有任何语义.

现在,在您的特定情况下,您确实正在创建函数(无限循环),但检查您是否实际上更难.为了避免编写试图进行详尽检查的代码,OCaml开发人员决定使用更简单的算法.

您可以在此处查看规则.这是摘录(强调我的):

如果每个人将接受expr1...... exprn相对于静态建设性name1...... namen,不立即链接到任何的name1...... namen,而不是一个数组构造方法的参数有抽象类型.

如您所见,不允许直接递归变量绑定.

这不是最终规则,因为编译器挂起版本的那部分有改进.我没有测试你的例子是否通过它,但有一天你的代码可能会被接受.