为什么这个函数的类型是 (a -> a) -> a？

Question

为什么这个函数的类型是 (a -> a) -> a？

Prelude> let y f = f (y f)
Prelude> :t y
y :: (t -> t) -> t

它不应该是一个无限/递归类型吗？ 我本来想试着表达一下我认为它的类型应该是什么，但出于某些原因我无法做到。

y :: (t -> t) -> ?WTFIsGoingOnOnTheRHS?

我不明白 f (y f) 怎么会得出一个值。下面的表达方式对我来说更容易理解：

Prelude> let y f x = f (y f) x
Prelude> :t y
y :: ((a -> b) -> a -> b) -> a -> b

但这仍然非常令人困惑。发生了什么？

- TheIronKnuckle

---

假设这是真正的代码，那么就解雇那个想出这个代码的人吧。 - Martin James

@MartinJames: 嗯？你认为代码有什么问题吗？虽然这不是定义函数的最佳方式，但这是最简单的方法。 - C. A. McCann

@MartinJames，那个函数是一个被广泛研究的函数，叫做Y组合子。（我想这是对的-我现在无法检查维基百科！）无论如何，也许你会因为成为一个文化低俗者而被解雇 :-) - Aaron McDaid

实际上这不是Y组合子，它只是等价于它；这是一个具有显式命名递归的不动点函数，而Y组合子的创新在于实现了没有任何语言支持的递归。P.S. 尝试将“?banner=none”附加到维基百科的URL中 :) - ehird

我还想补充一点，Y组合子是无类型λ演算中固定点组合子的特定实现：λf.(λx.f (x x)) (λx.f (x x))。然而，在Haskell中这不能简单地进行类型标注（在简单类型λ演算中也不可能进行类型标注；双关语）。自应用(x x)的需要要求在类型层面上进行递归。在Haskell中，您可以通过将其包装到newtype Rec a = In { out :: Rec a -> a }中来避免类型递归a = a -> a。 - Vitus

Answer 1

首先，y 必须是一种类型为 (a -> b) -> c 的函数，其中的 a、b 和 c 我们还不确定；因为它需要一个函数 f 并将其应用到一个参数上，所以它必须是一个接受函数的函数。

由于 y f = f x（同样是对于某个 x），我们知道 y 的返回类型必须是 f 本身的返回类型。因此，我们可以稍微调整一下 y 的类型：它必须是一种类型为 (a -> b) -> b 的函数，其中的 a 和 b 我们还不确定。

要找出 a 是什么，我们只需要看一下传递给 f 的值的类型。它是 y f，这是我们现在正在尝试找出类型的表达式。我们说 y 的类型为 (a -> b) -> b（其中的 a、b 等等），所以我们可以说这个 y f 的应用程序必须是类型为 b 本身。

因此，传递给 f 的参数的类型是 b。把所有这些重新组合在一起，我们得到的是 (b -> b) -> b —— 当然，这与 (a -> a) -> a 是相同的。

这里有一个更直观但不够精确的理解：我们说 y f = f (y f)，可以展开成等价的形式 y f = f (f (y f))，y f = f (f (f (y f)))，以此类推。因此，我们知道我们总是可以在整个表达式周围再应用一个 f。既然被讨论的“整个表达式”是将 f 应用到一个参数上的结果，那么 f 必须具有类型 a -> a；而且由于我们刚刚得出整个表达式是将 f 应用到一个参数上的结果，y 的返回类型必须与 f 本身的类型相同 — 综合起来，就是 (a -> a) -> a。

- ehird

---

基本上没错！它被称为“统一”（unification）。 - ehird

Answer 2

其他人的答案已经很好了，我只想补充两点。

你正在定义的函数通常被称为fix，它是一个不动点组合子：一个计算另一个函数的不动点的函数。在数学中，函数f的不动点是一个参数x，使得f x = x。这已经让你推断出fix的类型必须是(a -> a) -> a；“从a到a的函数，并返回a”。

你将函数命名为y，似乎是根据Y组合子，但这是一个不准确的名称：Y组合子是一个特定的不动点组合子，但并不与你在此处定义的相同。

我不理解如何将f(y f)解析为一个值。

嗯，技巧在于Haskell是一种非严格（也称为“惰性”）语言。如果f在所有情况下都不需要评估其y f参数，则可以终止对f(y f)的计算。因此，如果您正在定义阶乘（如John L所示），则fac(y fac) 1在不评估y fac的情况下计算为1。

严格语言无法做到这一点，因此在这些语言中，您无法以这种方式定义固定点组合子。在这些语言中，文本书上的固定点组合子是Y组合子。

- Luis Casillas

Answer 3

< p > @ehird已经很好地解释了类型，所以我想通过一些例子展示它如何解析为一个值。< /p >

f1 :: Int -> Int
f1 _ = 5

-- expansion of y applied to f1
y f1
f1 (y f1)  -- definition of y
5          -- definition of f1 (the argument is ignored)

-- here's an example that uses the argument, a factorial function
fac :: (Int -> Int) -> (Int -> Int)
fac next 1 = 1
fac next n = n * next (n-1)

y fac :: Int -> Int
fac (y fac)   -- def. of y
  -- at this point, further evaluation requires the next argument
  -- so let's try 3
fac (y fac) 3  :: Int
3 * (y fac) 2             -- def. of fac
3 * (fac (y fac) 2)       -- def. of y
3 * (2 * (y fac) 1)       -- def. of fac
3 * (2 * (fac (y fac) 1)  -- def. of y
3 * (2 * 1)               -- def. of fac

您可以用相同的方法进行任何函数的跟踪，以查看会发生什么。这两个示例都会收敛到某些值，但并非总是如此。

- John L

Answer 4

让我来介绍一个组合子。它被称为“不动点组合子”，具有以下属性：

属性： "不动点组合子" 接受一个函数 f :: (a -> a)，并“发现”这个函数的一个“不动点” x :: a，使得 f x == x。一些实现可能更好或更差地“发现”，但假设它终止，则将生成输入函数的固定点。满足该属性的任何函数都可以称为“不动点组合子”。

将此“不动点组合子”称为 y。根据刚才说的话，以下是正确的：

-- as we said, y's input is f :: a -> a, and its output is x :: a, therefore
y :: (a -> a) -> a

-- let x be the fixed point discovered by applying f to y
y f == x -- because y discovers x, a fixed point of f, per The Property
f x == x -- the behavior of a fixed point, per The Property

-- now, per substitution of "x" with "f x" in "y f == x"
y f == f x
-- again, per substitution of "x" with "y f" in the previous line
y f == f (y f)

那么，你已经通过不动点组合子的本质属性来定义了y：y f == f (y f)。你可以假设y f发现了x，也可以假设x代表一个发散的计算，仍然得出相同的结论（如我所知）。由于您的函数满足该属性，我们可以得出它是一个不动点组合子，并且我们已经声明的其他属性，包括类型，适用于您的函数。这并不是一个确凿的证明，但我希望它能提供额外的见解。

- Dan Burton