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

Question

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

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

它不应该是无限/递归类型吗？ 我本来想尝试用语言表达我认为它应该是什么样的类型，但由于某种原因我无法做到这一点。

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

我不明白 f (yf) 如何解析为一个值。以下内容对我来说更有意义：

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

但它仍然令人困惑。这是怎么回事？

Answer 1

好吧，y 必须是 (a -> b) ->; 类型。 c，对于某些 a、b 和 c 我们还不知道；毕竟，它接受一个函数 f，并将其应用于参数，因此它必须是一个接受函数的函数。

由于yf = 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) ->; 是一样的。一个。

这是一个更直观但不太精确的观点：我们说 yf = f (yf)，我们可以将其扩展为等效的 yf = f (f (yf)) 、yf = f (f (f(yf))) 等等。因此，我们知道我们总是可以在整个事物周围应用另一个 f，并且由于所讨论的“整个事物”是将 f 应用于参数的结果，< code>f 必须具有类型 a ->一个；由于我们刚刚得出结论，整个事情是将 f 应用于参数的结果，因此 y 的返回类型必须是 f 的返回类型本身 - 再次组合在一起，作为 (a -> a) ->一个。

Answer 2

仅补充两点以补充其他人的答案。

您定义的函数通常称为 fix，它是一个固定-点组合器：计算另一个点的固定点的函数 功能。在数学中，函数f的不动点是一个参数x，使得fx = x。这已经允许您推断 fix 的类型必须是 (a -> a) ->;一个； “该函数接受从 a 到 a 的函数，并返回 a。”

您已将函数命名为 y，它似乎位于 之后Y 组合器，但这是一个不准确的名称：Y 组合器是一个特定的定点组合器，但与您在此处定义的不同。

我不明白 f (yf) 如何解析为值。

好吧，诀窍在于 Haskell 是一种非严格（又名“惰性”）语言。如果 f 在所有情况下都不需要计算其 y f 参数，则 f (yf) 的计算可以终止。因此，如果您定义阶乘（如 John L 所示），fac (y fac) 1 的计算结果为 1，而不计算 y fac。

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

Answer 3

@ehird 在解释类型方面做得很好，所以我想通过一些示例来展示它如何解析为值。

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

您可以对任何您喜欢的函数执行相同的步骤，看看会发生什么。这两个例子都收敛于值，但这并不总是发生。

Answer 4

让我讲述一下组合器。它称为“定点组合器”，具有以下属性：

属性：“定点组合器”采用函数 f :: (a -> a) 和发现该函数的“不动点”x :: a，使得fx == 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：
yf == f (yf)。您可以假设 x 表示发散计算，但仍然得出相同的结论 (iinm)，而不是假设 y f 发现 x。

由于您的函数满足该属性，因此我们可以得出结论，它是一个定点组合器，并且我们声明的其他属性（包括类型）适用于您的函数。

这并不是一个可靠的证据，但我希望它能提供额外的见解。