Haskell在lambda演算中`let`绑定

Question

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

我从阅读中理解为你写了一个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演算中是这样吗？

Answer 1

的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)))

这使您可以根据自己定义函数和值.由于打字限制,这种表述不是合法的haskell,但有办法解决这个问题.

使用y-combinator让我们使用lambda演算来表达上面的let-bindings:

(\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))))