什么's the reason of '让rec'用于不纯的功能语言OCaml？

6 回答

• 34

  当您定义函数定义的语义时，作为语言设计者，您可以选择：要么使函数的名称在其自身的范围内可见，要么在其自身的范围内可见 . 这两种选择都是完全合法的，例如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，它有一个answer，可能会让你满意，引用它：

  因此，鉴于类型检查器需要知道哪些定义集是相互递归的，它能做什么？一种可能性是简单地对范围中的所有定义进行依赖性分析，并将它们重新排序到最小的可能组中 . Haskell实际上是这样做的，但是在F＃（和OCaml和SML）等具有无限制副作用的语言中，这是一个坏主意，因为它可能会重新排序副作用 . 因此，它要求用户明确标记哪些定义是相互递归的，因此通过扩展来进行泛化 .

  即使没有任何重新排序，使用任意非纯表达式，可能出现在函数定义中（定义的副作用，而不是评估），也无法构建依赖图 . 考虑从文件中解组和执行函数 .

  总结一下，我们有 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 标志没有技术原因 . 考虑一下，SML存在同样的问题，但默认情况下仍然启用 rec . let ... and ... 语法有一个技术原因，用于定义一组相互递归函数 . 在SML中，这种语法不需要我们在OCaml中放置 rec 标志，从而为我们提供了更大的灵活性，比如能够用 let x = y and y = x 表达式交换值 .

  回复于 2024-05-03T14:53:46+08:00
• 14

  在纯函数式语言中强制执行rec的技术原因是什么？

  递归是一种奇怪的野兽 . 它与纯度有关，但它比这更倾斜 . 要清楚，你可以写"alterna-Haskell"，它保留了它的纯度，它的懒惰，但默认没有递归地绑定 let ，并且需要某种 rec 标记就像OCaml一样 . 有些人甚至更喜欢这个 .

  ---

  从本质上讲，只有很多不同类型的_3042262可能 . 如果我们在OCaml中比较 let 和 let rec ，我们会看到一个小的差异 . 在静态形式语义中，我们可能会写

  Γ ⊢ E : A    Γ, x : A ⊢ F : B
  -----------------------------
     Γ ⊢ let x = E in F : B
  

  如果我们能够在变化的环境中证明 Γ E 具有类型 A 并且如果我们可以在 Γ 中使用 x : A 扩充 Γ ，那么我们可以证明在变量环境中 Γ 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 只是不同的野兽 .

  ---

  那么纯粹是什么意思呢？在最严格的定义中，Haskell甚至没有参与，我们必须消除所有影响，包括不终止 . 实现这一目标的唯一方法是放弃我们编写无限制递归的能力，并且只能小心地替换它 .

  存在大量没有递归的语言 . 也许最重要的是简单类型的Lambda微积分 . 在它的基本形式中，它是常规的lambda演算，但增加了类型有点类型的打字规则

  type ty =
    | Base
    | Arr of ty * ty
  

  事实证明，STLC不能代表递归--- Y组合器和所有其他定点表兄弟组合器都无法输入 . 因此，STLC不是图灵完成 .

  然而，它毫不妥协 . 然而，它通过最完整的仪器实现了这种纯度，完全取消了递归 . 我们_T42288_t导致非终止 - 我们仍将是图灵不完整，但不是那么残废 .

  有些语言尝试这个游戏 . 有一些聪明的方法可以在 data 和 codata 之间的一个分区中添加类型递归，这可以确保您不能编写非终止函数 . 如果你有兴趣，我建议学习一点Coq .

  ---

  但OCaml的目标（以及Haskell的目标）在这里并不精致 . 两种语言都是图灵完全（因而“实用”） . 因此，让我们讨论一些使用递归来增强STLC的更直接的方法 .

  最简单的是添加一个名为 fix 的内置函数

  val fix : ('a -> 'a) -> 'a
  

  或者，更真实的OCaml-y表示法，需要进行eta扩展

  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 是一个允许基本杂质通过图灵完整性及其伴侣效应非终止的窗口 .

  ---

  所以，在一天结束的时候，两种语言中更纯粹的Haskell做出了废除普通绑定的有趣选择，这有点有趣 . 这是唯一的区别：在Haskell中没有表示非递归绑定的语法 .

  在这一点上，它基本上只是一种风格决定 . Haskell的作者确定递归绑定是如此有用，以至于人们可以假设每个绑定都是递归的（并且相互如此，到目前为止，在这个答案中忽略了一堆蠕虫） .

  另一方面，OCaml使您能够完全明确您选择的绑定类型， let 或 let rec ！

  回复于 2024-05-03T14:53:46+08:00
• 0

  我认为这与纯粹的功能无关，这只是一个设计决定，在Haskell你不被允许做

  let a = 0;;
  let a = a + 1;;
  

  而你可以在Caml中做到这一点 .

  在Haskell中，此代码不起作用，因为 let a = a + 1 被解释为递归定义，不会终止 . 在Haskell中你不要创建一个非递归的（所以关键字 rec 是到处都是，但不是写的） .

  回复于 2024-05-03T14:53:46+08:00
• 6

  我不是专家，但我会猜测，直到真正知识渊博的家伙出现 . 在OCaml中，在定义函数期间可能会出现副作用：

  let rec f =
      let () = Printf.printf "hello\n" in
      fun x -> if x <= 0 then 12 else 1 + f (x - 1)
  

  这意味着必须在某种意义上保留函数定义的顺序 . 现在想象两个不同的相互递归函数集是交错的 . 编译器在将它们作为两个单独的相互递归的定义集处理时保留顺序似乎并不容易 .

  使用`let rec ...和``意味着不同的相互递归函数定义集不能像在Haskell中那样在OCaml中交错 . Haskell没有副作用（在某种意义上），因此定义可以自由重新排序 .

  回复于 2024-05-03T14:53:46+08:00
• 18

  这不是一个纯粹的问题，这是一个指定类型检查器应该检查表达式的环境的问题 . 它实际上给你的功率比你原本提供的更多 . 例如（我将在这里编写标准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 有一个数字类型，它没有 .

  它肯定更有必要，因为没有 rec 的情况允许你做这样的事情：

  val foo : int = 5
  val foo = foo + 1
  val foo = foo + 1
  

  现在 foo 的值为7.那个's not because it'已被突变，但是 - 名字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
  

  这使得更清楚的是正在发生的事情是原始定义的阴影，而不是副作用 .

  在风格上重新标识标识符是一个好主意是否值得怀疑 - 它可能会让人感到困惑 . 它在某些情况下很有用（例如，将函数名重新绑定到打印调试输出的自身版本） .

  回复于 2024-05-03T14:53:46+08:00
• 8

  我会说在OCaml中他们试图使REPL和源文件以相同的方式工作 . 因此，重新定义REPL中的某些功能是完全合理的;因此，他们也必须允许它在源头 . 现在，如果您自己使用（重新定义的）函数，OCaml需要某种方式来了解要使用的定义：前一个或新的定义 .

  在Haskell中，他们只是放弃并接受REPL在源文件中使用不同的东西 .

  回复于 2024-05-03T14:53:46+08:00