为什么这个函数的类型(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(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并将它应用于一个参数,所以它必须是一个函数.

因为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.

Answer 2

@ 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 3

只需两点即可添加到其他人的答案中.

您定义的函数通常被调用fix,它是一个定点组合器:一个计算另一个函数的固定点的函数.在数学中,函数的固定点f是一个参数x,使得f x = x.这已经可以让你推断的类型fix必须是(a -> a) -> a; "函数,它从功能a到a,并返回a".

你已经调用了你的函数y,它似乎是在Y组合子之后,但这是一个不准确的名称:Y组合子是一个特定的固定点组合子,但与你在这里定义的组合不同.

我不知道f(yf)如何解析为一个值.

好吧,诀窍是Haskell是一种非严格(又称"懒惰")的语言.f (y f)如果f不需要y f在所有情况下评估其参数,则可以终止计算.因此,如果您正在定义阶乘(如John L所示),则fac (y fac) 1在不进行评估的情况下求值为1 y fac.

严格的语言不能这样做,因此在这些语言中,您无法以这种方式定义定点组合器.在这些语言中,教科书定点组合器是Y组合器.

Answer 4

让我讲一个组合子.它被称为"fixpoint combinator",它具有以下属性:

物业:在"不动点组合子"需要的功能f :: (a -> a)和发现一个"定点" x :: a该功能使得f x == x.固定点组合器的某些实现在"发现"时可能更好或更差,但假设它终止,它将产生输入函数的固定点.满足The Property的任何函数都可以称为"fixpoint combinator".

称之为"fixpoint combinator" 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)

你去吧 您已经根据fixpoint combinator的基本属性进行了定义 y:
y f == f (y f).而不是假设y f发现x,你可以假设x代表一个不同的计算,并仍然得出相同的结论(iinm).

由于您的函数满足The Property,我们可以得出结论它是一个fixpoint combinator,并且我们声明的其他属性(包括类型)适用于您的函数.

这不是一个可靠的证明,但我希望它提供额外的见解.