4

我想了解let绑定在 Haskell 中是如何工作的（或者可能是 lambda 演算，如果 Haskell 实现不同？）

我从阅读Write you a Haskell中了解到，这对单个let绑定有效。

let x = y in e == (\x -> e) y

这对我来说很有意义，因为它与绑定在 lambda 演算中的工作方式是一致的。我感到困惑的是使用多个let绑定，其中一个绑定可以引用上面的绑定。我将提供一个简单的例子。

原始代码：

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)

这似乎不起作用，因为times在 lambda 调用 square 时未定义。然而，这可以通过这个实现来解决：

(\square -> square 5) ((\times x -> times x x) (\x -> x * x))

这是实现此绑定的正确方法，至少在 lambda 演算中是这样吗？

4

3 回答 3

5

/示例可以使用范围定义为 lambda 函数times：square

(\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 组合器定义为

(\f -> (\x -> f (x x))(\x -> f (x x)))

这使您可以根据自身定义函数和值。由于打字限制，该公式不是合法的haskell，但有一些方法可以解决这个问题。

使用 y-combinator 可以让我们使用 lambda 演算来表达上面的 let 绑定：

(\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))))
于 2019-01-06T06:06:55.303 回答
3

请注意，多个let绑定可以简化为一个，定义一对（一般情况下为元组）。例如我们可以重写

let times x y = x * y
    square x = times x x
in square 5

作为

let times = \x y -> x * y
    square = \x -> times x x
in square 5

然后

let (times, square) = (\x y -> x * y, \x -> times x x)
in square 5

然后，如果需要，

let pair = (\x y -> x * y, \x -> fst pair x x)
in snd pair 5

之后，我们可以应用通常的 lambda 演算转换。如果对定义最终是递归的，就像上面的例子一样，我们需要一个定点组合器。

(\pair -> snd pair 5) (fix (\pair -> (\x y -> x * y, \x -> fst pair x x)))

请注意，这种翻译不符合类型推断算法，它let以一种特殊的方式处理，引入了多态性。不过，如果我们只关心程序的动态方面，这并不重要。

于 2019-01-06T09:20:01.167 回答
2

我将回答我自己的问题，以便为那些访问这个问题的人提供一个有用的观点。

我们想用两个 let 绑定来实现以下程序：

let times a b = a * b
    square x = times x x
in square 5

首先，让我们将其简化为我们想要的本质：

square 5

很简单。但是，square在这种情况下是未定义的！好吧，我们可以使用我们的语言提供给我们的机制来绑定它——一个 lambda。这给了我们(\ square -> square 5) (\x -> times x x). 现在square定义了，但它的表亲times没有……好吧，我们需要另一个 lambda！我们的最终程序应如下所示：

(\times -> (\square -> square 5) (\x -> times x x)) (\a b -> a * b)

请注意，(\times -> ...)完全包含了我们的最后一步，因此times它将在绑定的范围内。这与@rampion 给出的答案一致，并减少如下：

(\times -> (\square  -> square 5) (\x -> times x x)) (\a b -> a * b) =>
(\square -> square 5) (\x -> (\a b -> a * b) x x)                    =>
(\square -> square 5) (\x -> (\b -> x * b) x)                        => 
(\square -> square 5) (\x -> x * x)                                  => 
(\x -> x * x) 5                                                      =>
5 * 5                                                                => 
25

如果square函数没有依赖times，我们本可以轻松编写(\times square -> ....。依赖意味着我们必须嵌套这两个环境，一个包含times，另一个在可以使用它的定义的内部。

感谢您所有的帮助！我被 lambda 演算的简单性和威力所震撼。

于 2019-01-06T17:14:33.037 回答