pro*_*eek 37 recursion ocaml haskell functional-programming
在Real World OCaml一书中,作者let rec阐述了OCaml 用于定义递归函数的原因.
OCaml主要出于技术原因区分非递归定义(使用let)和递归定义(使用let rec):类型推断算法需要知道一组函数定义何时是相互递归的,并且由于不适用于a的原因像Haskell这样的纯语言,必须由程序员明确标记.
let rec在纯函数式语言中强制执行的技术原因是什么？
ivg*_*ivg 34
当您定义函数定义的语义时,作为语言设计者,您可以选择:要么使函数的名称在其自身的范围内可见,要么在其自身的范围内可见.这两种选择都是完全合法的,例如C系列语言远非功能性,在其范围内仍然可以看到定义的名称(这也扩展到C中的所有定义,使其int x = x + 1合法).OCaml语言决定为我们提供额外的灵活性,让我们自己做出选择.这真的很棒.他们决定默认它是隐形的,这是一个相当下降的解决方案,因为我们编写的大多数函数都是非递归的.
关于引用的内容,它并不真正对应于函数定义 - rec关键字的最常见用法.它主要是关于"为什么函数定义的范围不扩展到模块的主体".这是一个完全不同的问题.经过一些研究后,我发现了一个非常相似的问题,它有一个答案,可能会让你满意,一个引用它:
因此,鉴于类型检查器需要知道哪些定义集是相互递归的,它能做什么？一种可能性是简单地对范围中的所有定义进行依赖性分析,并将它们重新排序到最小的可能组中.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中,这种语法不需要我们rec在OCaml中放置标志,从而为我们提供了更多的灵活性,比如能够用let x = y and y = x表达式交换值.
J. *_*son 18
在纯函数式语言中强制执行rec的技术原因是什么？
递归是一种奇怪的野兽.它与纯度有关,但它比这更倾斜.要清楚,你可以编写"alterna-Haskell",它保留了它的纯度,它的懒惰,但let默认情况下没有递归限制,并且需要rec像OCaml那样的某种标记.有些人甚至更喜欢这个.
从本质上讲,只有许多不同类型的"让"可能.如果我们比较let,let rec在OCaml中,我们会看到一个小的差异.在静态形式语义中,我们可能会写
? ? E : A ?, x : A ? F : B
-----------------------------
? ? let x = E in F : B
它说,如果我们能够在一个变量的环境证明?是E有类型的A,如果我们能在同一个环境变量证明? 增加与x : A该F : B那么我们可以证明,在环境变量? 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变量.
在这个意义上,let并且let rec仅仅是不同的东西.
那么纯粹是什么意思呢？在最严格的定义中,Haskell甚至没有参与,我们必须消除所有影响,包括不终止.实现这一目标的唯一方法是放弃我们编写无限制递归的能力,并且只能小心地替换它.
存在大量没有递归的语言.也许最重要的是简单类型的Lambda微积分.在它的基本形式中,它是常规的lambda演算,但增加了类型有点类型的打字规则
type ty =
| Base
| Arr of ty * ty
事实证明,STLC不能代表递归--- Y组合器和所有其他定点表兄弟组合器都无法输入.因此,STLC不是图灵完成.
然而,这是不折不扣的纯.然而,它通过最完整的仪器实现了这种纯度,完全取消了递归.我们真正喜欢的是某种平衡的,谨慎的递归,它不会导致不终止 - 我们仍将是图灵不完整,但不是那么残废.
有些语言尝试这个游戏.有一些聪明的方法可以在两者之间添加类型递归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 .我们确实可以fix在OCaml中写(至少后者),但那是在作弊.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))
在这一点上它应该再次清楚:let并且let rec是非常不同的野兽.它们具有不同程度的语言能力,let rec是通过图灵完整性及其伴侣效应非终止来允许基本杂质的窗口.
所以,在一天结束的时候,两种语言中较纯粹的Haskell做出了废除普通let绑定的有趣选择,这有点有趣.这是唯一的区别:在Haskell中没有表示非递归绑定的语法.
在这一点上,它基本上只是一种风格决定.Haskell的作者确定递归绑定是如此有用,以至于人们可以假设每个绑定都是递归的(并且相互如此,到目前为止,在这个答案中忽略了一堆蠕虫).
另一方面,OCaml使您能够完全明确您选择的绑定类型,let或者let rec!
Tho*_*ash 14
我认为这与纯粹的功能无关,这只是一个设计决定,在Haskell你不被允许做
let a = 0;;
let a = a + 1;;
而你可以在Caml中做到这一点.
在Haskell中,此代码不起作用,因为它let a = a + 1被解释为递归定义而不会终止.在Haskell中,您不必指定定义是递归的,因为您无法创建非递归定义(因此关键字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 ...和``意味着不同的相互递归函数定义集不能像在Haskell中那样在OCaml中交错.Haskell没有副作用(在某种意义上),因此定义可以自由重新排序.
这不是一个纯粹的问题,这是一个指定类型检查器应该检查表达式的环境的问题.它实际上给你的功率比你原本提供的更多.例如(我将在这里编写标准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
没有类型检查,因为rectypechecker已经决定foo已经反弹到类型的意思'a -> int,并且当它试图弄清楚'a需要什么时,会出现统一失败,因为x = foo力量foo有一个数字类型,它没有"T.
它当然可以"看起来"更为迫切,因为案例rec不允许你做这样的事情:
val foo : int = 5
val foo = foo + 1
val foo = foo + 1
现在它foo具有值7.这不是因为它已经被改变了,但是 - 名字 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
这使得更清楚的是正在发生的事情是原始定义的阴影,而不是副作用.
在风格上重新标识标识符是一个好主意是否值得怀疑 - 它可能会让人感到困惑.它在某些情况下很有用(例如,将函数名称重新绑定到打印调试输出的自身版本).