'let rec' 对于不纯函数式语言 OCaml 的原因是什么？
What's the reason of 'let rec' for impure functional language OCaml?
在Real World OCaml一书中，作者提出了为什么OCaml使用let rec来定义递归函数。
OCaml distinguishes between nonrecursive definitions (using let) and recursive definitions (using let rec) largely for technical reasons: the type-inference algorithm needs to know when a set of function definitions are mutually recursive, and for reasons that don't apply to a pure language like Haskell, these have to be marked explicitly by the programmer.
强制执行 let rec 而不是纯函数式语言的技术原因是什么？
我不是专家，但我会猜测，直到真正有知识的人出现。在 OCaml 中，函数定义期间可能会发生副作用：
let rec f =
let () = Printf.printf "hello\n" in
fun x -> if x <= 0 then 12 else 1 + f (x - 1)
这意味着在某种意义上必须保留函数定义的顺序。现在假设两组不同的相互递归函数交织在一起。编译器在将它们作为两个独立的相互递归定义集处理时保留顺序似乎一点也不容易。
使用 `let rec ... and`` 意味着不同的相互递归函数定义集不能像在 Haskell 中那样在 OCaml 中交错。 Haskell 没有副作用（在某种意义上），因此可以自由重新排序定义。
我认为这与纯粹的功能无关，这只是一个设计决定，在 Haskell 中你不能这样做
let a = 0;;
let a = a + 1;;
而您可以在 Caml 中完成。
在 Haskell 中，此代码将不起作用，因为 let a = a + 1 被解释为递归定义并且不会终止。
在 Haskell 中，您不必仅仅因为无法创建非递归定义就指定递归定义（因此关键字 rec 无处不在，但并未写入）。
当你定义函数定义的语义时，作为语言设计者，你有选择：要么使函数的名称在其自身的范围内可见，要么不可见。这两种选择都是完全合法的，例如 C 系列语言远非功能性语言，但在其范围内仍然有可见的定义名称（这也扩展到 C 中的所有定义，使 int x = x + 1 合法）。 OCaml 语言决定给我们额外的灵活性，让我们自己做出选择。那真的很棒。他们决定让它默认不可见，这是一个相当低级的解决方案，因为我们编写的大多数函数都是非递归的。
关于引用，它并不真正对应于函数定义 - rec 关键字的最常见用法。主要是关于 "Why the scope of function definition doesn't extend to the body of the module"。这是一个完全不同的问题。
经过一些研究，我发现了一个非常 similar question, that has an answer，可能会让你满意，引用它：
So, given that the type checker needs to know about which sets of
definitions are mutually recursive, what can it do? One possibility is
to simply do a dependency analysis on all the definitions in a scope,
and reorder them into the smallest possible groups. Haskell actually
does this, but in languages like F# (and OCaml and SML) which have
unrestricted side-effects, this is a bad idea because it might reorder
the side-effects too. So instead it asks the user to explicitly mark
which definitions are mutually recursive, and thus by extension where
generalization should occur.
即使没有任何重新排序，使用函数定义中可能出现的任意非纯表达式（定义的副作用，而不是评估），也无法构建依赖图。考虑从文件中解组和执行函数。
总而言之，let rec构造有两种用法，一种是创建自递归函数，如
let rec seq acc = function
| 0 -> acc
| n -> seq (acc+1) (n-1)
另一种是定义相互递归函数：
let rec odd n =
if n = 0 then true
else if n = 1 then false else even (n - 1)
and even n =
if n = 0 then false
else if n = 1 then true else odd (n - 1)
在第一种情况下，没有技术原因坚持一个或另一个解决方案。这只是一个品味问题。
第二种情况更难。推断类型时，您需要将所有函数定义拆分为由相互依赖的定义组成的簇，以缩小类型环境。在 OCaml 中更难制作，因为您需要考虑副作用。 （或者您可以继续而不将其拆分为主要组件，但这会导致另一个问题——您的类型系统将受到更多限制，即，将不允许更多有效程序）。
但是，重新审视原始问题和 RWO 的引述，我仍然很确定添加 rec 标志没有技术原因。考虑一下，具有相同问题但仍默认启用 rec 的 SML。 是技术原因，因为let ... and ...语法定义了一组相互递归函数。在 SML 中，这种语法不需要我们放置 rec 标志，而在 OCaml 中则需要，因此给了我们更多的灵活性，比如使用 let x = y and y = x 表达式交换值的能力。
我想说的是，在 OCaml 中，他们试图让 REPL 和源文件以相同的方式工作。所以，在 REPL 中重新定义一些函数是完全合理的；因此，他们也必须在源代码中允许它。现在，如果您使用（重新定义的）函数本身，OCaml 需要某种方式来知道要使用哪个定义：以前的定义还是新的定义。
在 Haskell 他们刚刚放弃并接受了 REPL 与源文件不同的工作方式。
What are the technical reasons that enforces let rec while pure functional languages not?
递归是一头奇怪的野兽。它与纯度有关，但比这更倾斜一点。需要明确的是，您可以编写 "alterna-Haskell" ，它保留了它的纯度和惰性，但默认情况下没有递归绑定 let 并且需要某种 rec 标记，就像 OCaml 所做的那样。有些人甚至更喜欢这个。
本质上，"let"可能有很多种。如果我们比较 OCaml 中的 let 和 let rec，我们会发现细微差别。在静态形式语义中，我们可以写成
Γ ⊢ E : A Γ, x : A ⊢ F : B
-----------------------------
Γ ⊢ let x = E in F : B
表示如果我们可以在变量环境 Γ 中证明 E 具有类型 A 并且如果我们可以在相同的变量环境中证明 Γ augmented with x : A that F : B 那么我们可以证明在变量环境中 Γ let x = E in F 具有类型 B.
要注意的是 Γ 论点。这只是像 [(x, 3); (y, "hello")] 这样的 ("variable name", "value") 对的列表，并且像 Γ, x : A 这样扩充列表只是意味着将 (x, A) 添加到它上面（抱歉语法被翻转了）。
特别是，让我们为 let rec
编写相同的形式
Γ, x : A ⊢ E : A Γ, x : A ⊢ F : B
-------------------------------------
Γ ⊢ let rec x = E in F : B
特别是，唯一的区别是我们的前提都不能在普通的 Γ 环境中工作；两者都可以假定 x 变量的存在。
从这个意义上说，let 和 let rec 完全是不同的野兽。
那么纯洁是什么意思呢？在 strictest 定义中，Haskell 甚至不参与，我们必须消除 all 影响，包括非终止。实现这一目标的唯一方法是取消我们编写不受限制的递归的能力，并谨慎地替换它。
没有递归的语言有很多。也许最重要的是简单类型的 Lambda 微积分。它的基本形式是常规的 lambda 演算，但增加了类型有点像
的类型规则
type ty =
| Base
| Arr of ty * ty
事实证明，STLC 无法表示递归——Y 组合子和所有其他定点表亲组合子都无法键入。因此，STLC 不是图灵完备的。
却毫不妥协纯粹。然而，它通过完全禁止递归来使用最简单的工具来实现这种纯度。我们真正想要的是某种不会导致不终止的平衡、谨慎的递归——我们仍然是图灵不完整的，但不会那么残废。
一些语言尝试这个游戏。有一些聪明的方法可以沿着 data 和 codata 之间的分界线添加类型递归，这确保您不能编写非终止函数。如果你有兴趣，我建议学习一点 Coq。
但 OCaml 的目标（以及 Haskell 的目标）在这里并不精致。这两种语言都是毫不妥协的图灵完备（因此 "practical"）。因此，让我们讨论一些使用递归增强 STLC 的更直截了当的方法。
最直接的方法是添加一个名为 fix
的内置函数
val fix : ('a -> 'a) -> 'a
或者，在需要 eta 扩展的更真实的 OCaml-y 表示法中
val fix : (('a -> 'b) -> ('a -> 'b)) -> ('a -> 'b)
现在，请记住，我们只考虑添加了 fix 的原始 STLC。我们确实可以在 OCaml 中编写 fix（至少是后一个），但目前这是作弊。 fix 购买 STLC 作为原始产品是什么？
原来答案是："everything"。 STLC + Fix（基本上是一种叫做 PCF 的语言）是不纯的，是图灵完备的。它也非常难以使用。
所以这是要跨越的最后一个障碍：我们如何使 fix 更易于使用？通过添加递归绑定！
STLC 已经有了 let 结构。您可以将其视为语法糖：
let x = E in F ----> (fun x -> F) (E)
但是一旦我们添加了 fix，我们也有能力引入 let rec 绑定
let rec x a = E in F ----> (fun x -> F) (fix (fun x a -> E))
此时应该再次清楚：let 和 let rec 是非常不同的野兽。它们体现了不同级别的语言能力，let rec 是 window 通过图灵完整性及其合作伙伴效应非终止允许基本杂质。
所以，在一天结束时，有点有趣的是 Haskell，两种语言中更纯粹的一种，做出了废除普通 let 绑定的有趣选择。这确实是唯一的区别：Haskell.
中没有表示非递归绑定的语法
在这一点上，它基本上只是一个风格决定。 Haskell 的作者确定递归绑定非常有用，以至于人们不妨假设 每个 绑定都是递归的（并且相互如此，在此答案中忽略了一堆蠕虫所以远）。
另一方面，OCaml 使您能够完全明确选择的绑定类型，let 或 let rec!
这不是纯度问题，而是指定类型检查器应在什么环境中检查表达式的问题。它实际上给了您比其他方式更强大的功能。例如（我打算在这里编写标准 ML，因为我比 OCaml 更了解它，但我相信这两种语言的类型检查过程几乎相同），它可以让你区分这些情况：
val foo : int = 5
val foo = fn (x) => if x = foo then 0 else 1
现在，从第二次重新定义开始，foo 的类型为 int -> int。另一方面，
val foo : int = 5
val rec foo = fn (x) => if x = foo then 0 else 1
不进行类型检查，因为 rec 意味着类型检查器已经确定 foo 已被重新绑定到类型 'a -> int，并且当它试图弄清楚那是什么时'a 需要，因为 x = foo 强制 foo 具有数字类型，但它没有。
它当然可以 "look" 更命令，因为没有 rec 的情况允许你做这样的事情：
val foo : int = 5
val foo = foo + 1
val foo = foo + 1
现在 foo 的值为 7。这不是因为它发生了变异，而是 --- name foo 已经反弹了 3 次，它只是碰巧这些绑定中的每一个都隐藏了一个名为 foo 的变量的先前绑定。与此相同：
val foo : int = 5
val foo' = foo + 1
val foo'' = foo' + 1
除了 foo 和 foo' 在标识符 foo 被重新绑定后在环境中不再可用。以下也是合法的：
val foo : int = 5
val foo : real = 5.0
这更清楚地表明正在发生的事情是 遮蔽 原始定义，而不是副作用。
重新绑定标识符在文体上是否是个好主意值得怀疑——它可能会让人感到困惑。它在某些情况下很有用（例如，将函数名称重新绑定到打印调试输出的自身版本）。
在Real World OCaml一书中，作者提出了为什么OCaml使用let rec来定义递归函数。
OCaml distinguishes between nonrecursive definitions (using let) and recursive definitions (using let rec) largely for technical reasons: the type-inference algorithm needs to know when a set of function definitions are mutually recursive, and for reasons that don't apply to a pure language like Haskell, these have to be marked explicitly by the programmer.
强制执行 let rec 而不是纯函数式语言的技术原因是什么？
我不是专家，但我会猜测，直到真正有知识的人出现。在 OCaml 中，函数定义期间可能会发生副作用：
let rec f =
let () = Printf.printf "hello\n" in
fun x -> if x <= 0 then 12 else 1 + f (x - 1)
这意味着在某种意义上必须保留函数定义的顺序。现在假设两组不同的相互递归函数交织在一起。编译器在将它们作为两个独立的相互递归定义集处理时保留顺序似乎一点也不容易。
使用 `let rec ... and`` 意味着不同的相互递归函数定义集不能像在 Haskell 中那样在 OCaml 中交错。 Haskell 没有副作用（在某种意义上），因此可以自由重新排序定义。
我认为这与纯粹的功能无关，这只是一个设计决定，在 Haskell 中你不能这样做
let a = 0;;
let a = a + 1;;
而您可以在 Caml 中完成。
在 Haskell 中，此代码将不起作用，因为 let a = a + 1 被解释为递归定义并且不会终止。
在 Haskell 中，您不必仅仅因为无法创建非递归定义就指定递归定义（因此关键字 rec 无处不在，但并未写入）。
当你定义函数定义的语义时，作为语言设计者，你有选择：要么使函数的名称在其自身的范围内可见，要么不可见。这两种选择都是完全合法的，例如 C 系列语言远非功能性语言，但在其范围内仍然有可见的定义名称（这也扩展到 C 中的所有定义，使 int x = x + 1 合法）。 OCaml 语言决定给我们额外的灵活性，让我们自己做出选择。那真的很棒。他们决定让它默认不可见，这是一个相当低级的解决方案，因为我们编写的大多数函数都是非递归的。
关于引用，它并不真正对应于函数定义 - rec 关键字的最常见用法。主要是关于 "Why the scope of function definition doesn't extend to the body of the module"。这是一个完全不同的问题。
经过一些研究，我发现了一个非常 similar question, that has an answer，可能会让你满意，引用它：
So, given that the type checker needs to know about which sets of definitions are mutually recursive, what can it do? One possibility is to simply do a dependency analysis on all the definitions in a scope, and reorder them into the smallest possible groups. Haskell actually does this, but in languages like F# (and OCaml and SML) which have unrestricted side-effects, this is a bad idea because it might reorder the side-effects too. So instead it asks the user to explicitly mark which definitions are mutually recursive, and thus by extension where generalization should occur.
即使没有任何重新排序，使用函数定义中可能出现的任意非纯表达式（定义的副作用，而不是评估），也无法构建依赖图。考虑从文件中解组和执行函数。
总而言之，let rec构造有两种用法，一种是创建自递归函数，如
let rec seq acc = function
| 0 -> acc
| n -> seq (acc+1) (n-1)
另一种是定义相互递归函数：
let rec odd n =
if n = 0 then true
else if n = 1 then false else even (n - 1)
and even n =
if n = 0 then false
else if n = 1 then true else odd (n - 1)
在第一种情况下，没有技术原因坚持一个或另一个解决方案。这只是一个品味问题。
第二种情况更难。推断类型时，您需要将所有函数定义拆分为由相互依赖的定义组成的簇，以缩小类型环境。在 OCaml 中更难制作，因为您需要考虑副作用。 （或者您可以继续而不将其拆分为主要组件，但这会导致另一个问题——您的类型系统将受到更多限制，即，将不允许更多有效程序）。
但是，重新审视原始问题和 RWO 的引述，我仍然很确定添加 rec 标志没有技术原因。考虑一下，具有相同问题但仍默认启用 rec 的 SML。 是技术原因，因为let ... and ...语法定义了一组相互递归函数。在 SML 中，这种语法不需要我们放置 rec 标志，而在 OCaml 中则需要，因此给了我们更多的灵活性，比如使用 let x = y and y = x 表达式交换值的能力。
我想说的是，在 OCaml 中，他们试图让 REPL 和源文件以相同的方式工作。所以，在 REPL 中重新定义一些函数是完全合理的；因此，他们也必须在源代码中允许它。现在，如果您使用（重新定义的）函数本身，OCaml 需要某种方式来知道要使用哪个定义：以前的定义还是新的定义。
在 Haskell 他们刚刚放弃并接受了 REPL 与源文件不同的工作方式。
What are the technical reasons that enforces let rec while pure functional languages not?
递归是一头奇怪的野兽。它与纯度有关，但比这更倾斜一点。需要明确的是，您可以编写 "alterna-Haskell" ，它保留了它的纯度和惰性，但默认情况下没有递归绑定 let 并且需要某种 rec 标记，就像 OCaml 所做的那样。有些人甚至更喜欢这个。
本质上，"let"可能有很多种。如果我们比较 OCaml 中的 let 和 let rec，我们会发现细微差别。在静态形式语义中，我们可以写成
Γ ⊢ E : A Γ, x : A ⊢ F : B
-----------------------------
Γ ⊢ let x = E in F : B
表示如果我们可以在变量环境 Γ 中证明 E 具有类型 A 并且如果我们可以在相同的变量环境中证明 Γ augmented with x : A that F : B 那么我们可以证明在变量环境中 Γ let x = E in F 具有类型 B.
要注意的是 Γ 论点。这只是像 [(x, 3); (y, "hello")] 这样的 ("variable name", "value") 对的列表，并且像 Γ, x : A 这样扩充列表只是意味着将 (x, A) 添加到它上面（抱歉语法被翻转了）。
特别是，让我们为 let rec
Γ, x : A ⊢ E : A Γ, x : A ⊢ F : B
-------------------------------------
Γ ⊢ let rec x = E in F : B
特别是，唯一的区别是我们的前提都不能在普通的 Γ 环境中工作；两者都可以假定 x 变量的存在。
从这个意义上说，let 和 let rec 完全是不同的野兽。
那么纯洁是什么意思呢？在 strictest 定义中，Haskell 甚至不参与，我们必须消除 all 影响，包括非终止。实现这一目标的唯一方法是取消我们编写不受限制的递归的能力，并谨慎地替换它。
没有递归的语言有很多。也许最重要的是简单类型的 Lambda 微积分。它的基本形式是常规的 lambda 演算，但增加了类型有点像
的类型规则type ty =
| Base
| Arr of ty * ty
事实证明，STLC 无法表示递归——Y 组合子和所有其他定点表亲组合子都无法键入。因此，STLC 不是图灵完备的。
却毫不妥协纯粹。然而，它通过完全禁止递归来使用最简单的工具来实现这种纯度。我们真正想要的是某种不会导致不终止的平衡、谨慎的递归——我们仍然是图灵不完整的，但不会那么残废。
一些语言尝试这个游戏。有一些聪明的方法可以沿着 data 和 codata 之间的分界线添加类型递归，这确保您不能编写非终止函数。如果你有兴趣，我建议学习一点 Coq。
但 OCaml 的目标（以及 Haskell 的目标）在这里并不精致。这两种语言都是毫不妥协的图灵完备（因此 "practical"）。因此，让我们讨论一些使用递归增强 STLC 的更直截了当的方法。
最直接的方法是添加一个名为 fix
val fix : ('a -> 'a) -> 'a
或者，在需要 eta 扩展的更真实的 OCaml-y 表示法中
val fix : (('a -> 'b) -> ('a -> 'b)) -> ('a -> 'b)
现在，请记住，我们只考虑添加了 fix 的原始 STLC。我们确实可以在 OCaml 中编写 fix（至少是后一个），但目前这是作弊。 fix 购买 STLC 作为原始产品是什么？
原来答案是："everything"。 STLC + Fix（基本上是一种叫做 PCF 的语言）是不纯的，是图灵完备的。它也非常难以使用。
所以这是要跨越的最后一个障碍：我们如何使 fix 更易于使用？通过添加递归绑定！
STLC 已经有了 let 结构。您可以将其视为语法糖：
let x = E in F ----> (fun x -> F) (E)
但是一旦我们添加了 fix，我们也有能力引入 let rec 绑定
let rec x a = E in F ----> (fun x -> F) (fix (fun x a -> E))
此时应该再次清楚：let 和 let rec 是非常不同的野兽。它们体现了不同级别的语言能力，let rec 是 window 通过图灵完整性及其合作伙伴效应非终止允许基本杂质。
所以，在一天结束时，有点有趣的是 Haskell，两种语言中更纯粹的一种，做出了废除普通 let 绑定的有趣选择。这确实是唯一的区别：Haskell.
在这一点上，它基本上只是一个风格决定。 Haskell 的作者确定递归绑定非常有用，以至于人们不妨假设 每个 绑定都是递归的（并且相互如此，在此答案中忽略了一堆蠕虫所以远）。
另一方面，OCaml 使您能够完全明确选择的绑定类型，let 或 let rec!
这不是纯度问题，而是指定类型检查器应在什么环境中检查表达式的问题。它实际上给了您比其他方式更强大的功能。例如（我打算在这里编写标准 ML，因为我比 OCaml 更了解它，但我相信这两种语言的类型检查过程几乎相同），它可以让你区分这些情况：
val foo : int = 5
val foo = fn (x) => if x = foo then 0 else 1
现在，从第二次重新定义开始，foo 的类型为 int -> int。另一方面，
val foo : int = 5
val rec foo = fn (x) => if x = foo then 0 else 1
不进行类型检查，因为 rec 意味着类型检查器已经确定 foo 已被重新绑定到类型 'a -> int，并且当它试图弄清楚那是什么时'a 需要，因为 x = foo 强制 foo 具有数字类型，但它没有。
它当然可以 "look" 更命令，因为没有 rec 的情况允许你做这样的事情：
val foo : int = 5
val foo = foo + 1
val foo = foo + 1
现在 foo 的值为 7。这不是因为它发生了变异，而是 --- name foo 已经反弹了 3 次，它只是碰巧这些绑定中的每一个都隐藏了一个名为 foo 的变量的先前绑定。与此相同：
val foo : int = 5
val foo' = foo + 1
val foo'' = foo' + 1
除了 foo 和 foo' 在标识符 foo 被重新绑定后在环境中不再可用。以下也是合法的：
val foo : int = 5
val foo : real = 5.0
这更清楚地表明正在发生的事情是 遮蔽 原始定义，而不是副作用。
重新绑定标识符在文体上是否是个好主意值得怀疑——它可能会让人感到困惑。它在某些情况下很有用（例如，将函数名称重新绑定到打印调试输出的自身版本）。