如何理解 Haskell 中的嵌套 lambda 函数答案

【问题标题】：How to understand nested lambda functions in Haskell如何理解 Haskell 中的嵌套 lambda 函数
【发布时间】：2019-03-29 07:27:17
【问题描述】：

我试图理解 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 的新手，我对这些类型的转换不是很有信心。如果不正确，什么是正确的转换？

【问题讨论】：

f x = x (x $) = x x。它没有类型、lambda 或没有 lambda。通过 eta-expansion f x y = x x y 仍然没有类型。 g x = id x = x。我无法理解你的推理。
@WillNess 它没有 Rank-1 类型但有 Rank-2 类型：(forall a. a -> b) -> b。
@AaditMShah 很有趣。看起来它并不能帮助我们输入f . (. f)。 :)
@WillNess Lol，Y 组合器？让我试着看看我是否可以为此设计一种类型。很可能我将无法做到。 AFAIK，小欧米茄无法输入。
@AaditMShah 我用谷歌搜索“y 组合器是否有 Rank-2 类型”，但没有立即出现明显的“是/否”答案。当然可以用newtype来完成...

标签： haskell functional-programming

【解决方案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 演算。

【讨论】：

已删除并道歉。
稍微严格一点：f x = x x 可以用 rank-2 类型输入（在 GHC 中是这样，但在标准 Haskell 中不是），但不能推断。
我同意@AlexeyRomanov。您可以将类型(forall a. a -> b) -> b 分配给f x = x x。
@AaditMShah 啊，对。在我修改后的答案中，我选择了较短的类型f :: (forall a. a) -> b，但你的更有用，因为它允许非底部常量函数。
f x y = x x y 与正确的定义等价，因此并非完全错误。不过，“推导”完全不在其中。

【解决方案2】：

GHCi 提示符下的:type 命令是您的朋友。让我们先举第二个例子

λ> :type let g = \x -> (\y -> y) x in g
let g = \x -> (\y -> y) x in g :: p -> p

所以g 是类型良好的，并且是编写标识函数:: p -> p 的一种复杂方式。具体来说，g 需要一些x 并将标识函数(\y -> y) 应用于x，从而得到x。 GHCi 在给出类型时使用了一个新的类型名称p，以避免混淆。不，您的 g x y = ... 不等效。（用:type检查。）

您可以将 :type 缩写为 :t。那么让我们以你的第一个例子为例。

λ> :t let f = \x -> x (\y -> x y) in f
* Occurs check: cannot construct the infinite type: t2 ~ t2 -> t3
* In the first argument of `x', namely `(\ y -> x y)'
  In the expression: x (\ y -> x y)
  In the expression: \ x -> x (\ y -> x y)
* Relevant bindings include
    x :: t2 -> t3 (bound at <interactive>:1:10)
    f :: (t2 -> t3) -> t3 (bound at <interactive>:1:5)

呃。你推荐的f和那个一样吗？

λ> :t let f x y = x x y in f
* Occurs check: cannot construct the infinite type:
    t3 ~ t3 -> t4 -> t5
* In the first argument of `x', namely `x'

它至少看起来像一个类似的错误消息。这些t2, t3, t4, t5 是什么？同样是 GHCi 为类型使用新名称，以避免混淆。

查看let f = ...，GHCi 看到x 应用于某物，因此它给出x :: t2 -> t3，其中t2 是其参数的类型，t3 是返回类型。它还看到f = \x -> x (blah)。所以f 的返回类型必须是x 返回的任何类型，即t3，而f 的参数是x。所以f :: (t2 -> t3) -> t3。

在(blah) 中，x 应用于某物。所以某物（即y）必须是x的参数类型，返回类型必须是x的返回类型。 IE。 (\y -> x y) :: t2 -> t3。 Errk：那么我们必须让x 的参数类型与此相同，因为x 应用于它。我们写“same as”的方式是~。

然后错误消息告诉您 GHCi 正在尝试理解 t2 ~ (t2 -> t3)。（-> 绑定比 ~ 更紧密。）如果您尝试将 t2 的等价替换为 RHS，您将得到 t2 ~ (((... -> t3) -> t3)-> t3) 无限。

您为f x y = 建议的等效项不等效（消息/键入略有不同）。但它们都是无限类型，所以不允许。

【讨论】：