我想了解 let
绑定(bind)如何在 Haskell 中工作(或者可能是 lambda 演算,如果 Haskell 实现不同?)
我从阅读 Write you a Haskell 中了解到,这对单个 let
绑定(bind)有效。
let x = y in e == (\x -> e) y
这对我来说很有意义,因为它与绑定(bind)在 lambda 演算中的工作方式一致。我感到困惑的是使用多个
let
绑定(bind),其中一个绑定(bind)可以引用上面的绑定(bind)。我将提供一个简单的例子。原始代码:
let times x y = x * y
square x = times x x
in square 5
我对实现的猜测:
(\square times -> square 5) (\x -> times x x) (\x -> x * x)
这似乎不起作用,因为当 lambda 调用 square 时未定义
times
。但是,这可以通过以下实现解决:(\square -> square 5) ((\times x -> times x x) (\x -> x * x))
这是实现这种绑定(bind)的正确方法吗,至少在 lambda 演算中?
最佳答案
times
/square
示例可以使用作用域以 lambda 函数的形式表示:
(\times -> (\square -> square 5)(\x -> times x x))(\x y -> x * y)
但是对于递归或相互递归的 let-bindings 来说,作用域是不够的
let ones = 1 : ones in take 5 ones
let even n = n == 0 || odd (abs n - 1)
odd n = n /= 0 && even (abs n - 1)
in even 7
在 lambda 演算中,您可以将递归的 y-combinator 定义为
(\f -> (\x -> f (x x))(\x -> f (x x)))
这使您可以根据自身定义函数和值。由于输入限制 but there are ways around that ,该公式不是合法的haskell。
使用 y 组合器让我们可以使用 lambda 演算来表达上述 let 绑定(bind):
(\ones -> take 5 ones)((\f -> (\x -> f (x x))(\x -> f (x x)))(\ones -> 1 : ones))
(\evenodd -> evenodd (\x y -> x) 7)((\f -> (\x -> f (x x))(\x -> f (x x)))(\evenodd c -> c (\n -> n == 0 || evenodd (\x y -> y) (abs n - 1)) (\n -> n /= 0 && evenodd (\x y -> x) (abs n - 1))))
关于lambda 演算中的 Haskell `let` 绑定(bind),我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/54058816/