haskell - 如何理解 Haskell 中嵌套的 lambda 函数

Question

我试图理解 Haskell 中以下 2 个 lambda 表达式的含义:

f = \x -> x (\y -> x y)
g = \x -> (\y -> y) x

我试着转换它们，我得到了这个:

f x y = x x y
g x y = y x

这是正确的吗？我假设这两个函数的参数必须是 x 和 y，因为它们都可以在函数描述的 lambda 表达式中找到。我基本上是这样理解的:f(x) = x f(y) and f(y) = y x。对于 g，g(x) = g(y) x 和 g(y) = y。但由于我是 Haskell 的新手，我对这些类型的转换不是很有信心。如果不正确，什么是正确的转换？

Answer 1

两者都不正确。您的解决方案使用函数

f x y = x x y
g x y = y x

实际上是什么意思

f = \x -> (\y -> x x y)
g = \x -> (\y -> y x)

以及那些与原始表达方式不同的地方

f = \x -> x (\y -> x y)
g = \x -> (\y -> y) x

以上两个方程可以改写为

f x = x (\y -> x y)
g x = (\y -> y) x

但是从这里开始，没有办法将剩余的 lambda 转化为更多的 f 或 g 参数。充其量，我们可以使用 beta/eta 转换来简化它们并得到

f x = x x            -- eta  (\y -> x y) = x
g x = x              -- beta (\y -> y) x = x

(另见 Will Ness 下面的评论，他指出通过 f 中的额外 eta 扩展，我们可以达到 OP 的定义。不过，这是偶然的。)

最后，请注意，Haskell 不会接受 f x = x x，因为它不能被键入，除非我们使用 rank-2 类型并显式提供类型注释，如 f::(forall a. a) -> b.原始代码 f =\x -> x (\y -> x y) 存在同样的问题。这在无类型语言中也很好，例如编程语言理论中的无类型 lambda 演算。