haskell 不纯的函数式语言OCaml使用“let rec”的原因是什么?

fquxozlt  于 2022-11-14  发布在  其他
关注(0)|答案(6)|浏览(191)

在《真实的世界OCaml》一书中,作者提出了为什么OCaml使用let rec来定义递归函数。
OCaml区分非递归定义(使用let)和递归定义(使用let rec)主要是出于技术原因:类型推理算法需要知道一组函数定义何时是相互递归的,并且由于不适用于像Haskell这样的纯语言的原因,这些定义必须由程序员显式地标记。
是什么技术原因强制let rec,而纯函数式语言不强制?

mwyxok5s

mwyxok5s1#

当您定义函数定义的语义时,作为语言设计者,您有以下选择:要么使函数名在其自身的作用域中可见,要么不可见。这两种选择都是完全法律的的,例如,C族语言虽然远离函数,但仍然在其作用域中具有可见的定义名(这也扩展到C语言中的所有定义,使int x = x + 1法律的)。OCaml语言决定给予我们额外的灵活性,让我们自己做出选择。这真的很棒。他们决定在默认情况下使其不可见,这是一个相当不错的解决方案,因为我们编写的大多数函数都是非递归的。
关于引用,它并不真正对应于函数定义--rec关键字最常见的用法。它主要是关于“为什么函数定义的作用域不扩展到模块的主体”。这是一个完全不同的问题。经过一些研究,我找到了一个非常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。这 * 是 * 一个技术原因,for let ... and ...语法定义了一组相互递归函数。在SML中,这种语法不要求我们放置rec标志,而在OCaml中则需要,因此给了我们更多的灵活性。例如使用let x = y and y = x表达式交换值的功能。

3ks5zfa0

3ks5zfa02#

是什么技术原因强制使用let rec而不是纯函数式语言?
递归是一种奇怪的东西。它与纯粹性有关,但它比这更间接一些。为了清楚起见,你可以写“alternate-Haskell”,它保留了它的纯粹性和惰性,但默认情况下没有递归绑定的let,它需要某种rec标记,就像OCaml一样。有些人甚至更喜欢这样。
本质上,“let“s possible有很多不同的类型。如果我们比较OCaml中的letlet rec,我们会发现一个小的区别。在静态形式语义中,我们可以写

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

即如果我们可以在可变环境Γ中证明E具有类型A,并且如果我们可以在相同的可变环境Γ中证明F : B具有x : A的 * 增广 *,则我们可以证明在可变环境Γlet x = E in F具有类型B
要注意的是Γ参数。这只是一个(“变量名”,“值”)对的列表,如[(x, 3); (y, "hello")],增加列表如Γ, x : A,只是意味着将(x, A)添加到它上面(抱歉,语法颠倒了)。
特别地,让我们为let rec编写相同的形式

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

特别是,唯一的区别是我们的前提都不能在简单的Γ环境中工作;允许两者都假定x变量的存在。
从这个意义上说,letlet rec是完全不同的野兽。
那么,纯粹意味着什么呢?在最严格的定义下,我们必须消除包括非终止性在内的所有影响,而Haskell甚至没有参与其中。实现这一点的唯一方法是取消我们编写无限制递归的能力,并小心地替换它。
有很多语言没有递归。也许最重要的一个是简单类型的Lambda演算。它的基本形式是常规的lambda演算,但增加了类型规则,其中类型有点像

type ty =
  | Base
  | Arr of ty * ty

结果表明,STLC不能表示递归---Y组合子和所有其他定点的同类组合子都不能被类型化。因此,STLC不是图灵完备的。
然而,它是毫不妥协的“纯粹”。然而,它通过完全禁止递归,用最钝的手段达到了这种纯粹。我们真正想要的是某种平衡的、谨慎的递归,它不会导致非终结性--我们仍然是图灵不完全,但不会那么残废。
有些语言尝试过这个游戏。有一些聪明的方法可以沿着datacodata之间的分界线上添加类型递归,这样就可以确保你不能编写非终止函数。如果你感兴趣,我建议你学习一下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带来什么?
原来,答案是: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))

在这一点上,应该再次明确:letlet rec是两种截然不同的动物,它们体现了不同层次的语言权力,而let rec则是通过图灵完备性及其伙伴效应的不终止性允许基本不纯性的一个窗口。
因此,在一天结束的时候,有点有趣的是,Haskell,这两种语言中更纯粹的一种,做出了废除普通let绑定的有趣选择。这确实是唯一的区别:在Haskell中没有用于表示非递归绑定的语法。
Haskell的作者认为递归绑定非常有用,以至于我们可以假设 every binding都是递归的(相互之间也是递归的,到目前为止,这个答案忽略了一堆蠕虫)。
另一方面,OCaml让你能够完全明确你选择的绑定类型,letlet rec

w8rqjzmb

w8rqjzmb3#

我认为这与纯粹的功能无关,这只是一个设计决策,在Haskell中不允许这样做

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

而你可以在Caml里做。
在Haskell中,这段代码不起作用,因为let a = a + 1被解释为递归定义,并且不会终止。在Haskell中,你不必指定一个定义是递归的,因为你不能创建一个非递归的定义(所以关键字rec无处不在,但没有被写入)。

lndjwyie

lndjwyie4#

我不是Maven,但我会先做一个猜测,直到真正有知识的人出现。在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'的使用意味着不同的递归函数定义集在OCaml中不能像在Haskell中那样交错。Haskell没有副作用(在某种意义上),因此定义可以自由地重新排序。

hk8txs48

hk8txs485#

这不是一个纯粹性的问题,而是一个指定类型检查器应该在什么环境中检查表达式的问题。它实际上给了你比其他方法更多的能力。例如(我在这里要写标准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,这并不是因为它被改变了,但是---name foo已经被重新绑定了3次,而且碰巧每一次绑定都隐藏了一个名为foo的变量的前一个绑定。

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

除了在重新绑定标识符foo后,foofoo'在环境中不再可用。以下内容也是法律的的:

val foo : int = 5
val foo : real = 5.0

这就更清楚地表明,所发生的事情是对原始定义的“遮蔽”,而不是副作用。
重新绑定标识符在风格上是否是一个好主意是值得怀疑的--它可能会让人感到困惑。在某些情况下它可能很有用(例如,将函数名重新绑定到打印调试输出的自身版本)。

iszxjhcz

iszxjhcz6#

我认为在OCaml中,他们试图让REPL和源文件以同样的方式工作。因此,它们必须在源代码中也允许它。现在,如果你在函数本身中使用(redefined),OCaml需要某种方式来知道使用哪种定义:前一个或新的。
在Haskell中,他们已经放弃并接受了REPL与源文件不同的工作方式。

相关问题