Why is the type of this function (a -> a) -> a?

Question

Why is the type of this function (a -> a) -> a?

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

Shouldn't it be an infinite/recursive type? I was going to try and put into words what I think it's type should be, but I just can't do it for some reason.

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

I don't get how f (y f) resolves to a value. The following makes a little more sense to me:

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

But it's still ridiculously confusing. What's going on?

Answer 1

Well, y has to be of type (a -> b) -> c, for some a, b and c we don't know yet; after all, it takes a function, f, and applies it to an argument, so it must be a function taking a function.

Since y f = f x (again, for some x), we know that the return type of y must be the return type of f itself. So, we can refine the type of y a bit: it must be (a -> b) -> b for some a and b we don't know yet.

To figure out what a is, we just have to look at the type of the value passed to f. It's y f, which is the expression we're trying to figure out the type of right now. We're saying that the type of y is (a -> b) -> b (for some a, b, etc.), so we can say that this application of y f must be of type b itself.

So, the type of the argument to f is b. Put it all back together, and we get (b -> b) -> b — which is, of course, the same thing as (a -> a) -> a.

Here's a more intuitive, but less precise view of things: we're saying that y f = f (y f), which we can expand to the equivalent y f = f (f (y f)), y f = f (f (f (y f))), and so on. So, we know that we can always apply another f around the whole thing, and since the "whole thing" in question is the result of applying f to an argument, f has to have the type a -> a; and since we just concluded that the whole thing is the result of applying f to an argument, the return type of y must be that of f itself — coming together, again, as (a -> a) -> a.

Answer 2

@ehird's done a good job of explaining the type, so I'd like to show how it can resolve to a value with some examples.

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

You can follow the same steps with any function you like to see what will happen. Both of these examples converge to values, but that doesn't always happen.

Answer 3

Let me tell about a combinator. It's called the "fixpoint combinator" and it has the following property:

The Property: the "fixpoint combinator" takes a function f :: (a -> a) and discovers a "fixed point" x :: a of that function such that f x == x. Some implementations of the fixpoint combinator might be better or worse at "discovering", but assuming it terminates, it will produce a fixed point of the input function. Any function that satisfies The Property can be called a "fixpoint combinator".

Call this "fixpoint combinator" y. Based on what we just said, the following are true:

-- 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)

So there you go. You have defined y in terms of the essential property of the fixpoint combinator:
y f == f (y f). Instead of assuming that y f discovers x, you can assume that x represents a divergent computation, and still come to the same conclusion (iinm).

Since your function satisfies The Property, we can conclude that it is a fixpoint combinator, and that the other properties we have stated, including the type, are applicable to your function.

This isn't exactly a solid proof, but I hope it provides additional insight.

Answer 4

Just two points to add to other people's answers.

The function you're defining is usually called fix, and it is a fixed-point combinator: a function that computes the fixed point of another function. In mathematics, the fixed point of a function f is an argument x such that f x = x. This already allows you to infer that the type of fix has to be (a -> a) -> a; "function that takes a function from a to a, and returns an a."

You've called your function y, which seems to be after the Y combinator, but this is an inaccurate name: the Y combinator is one specific fixed point combinator, but not the same as the one you've defined here.

I don't get how f (y f) resolves to a value.

Well, the trick is that Haskell is a non-strict (a.k.a. "lazy") language. The calculation of f (y f) can terminate if f doesn't need to evaluate its y f argument in all cases. So, if you're defining factorial (as John L illustrates), fac (y fac) 1 evaluates to 1 without evaluating y fac.

Strict languages can't do this, so in those languages you cannot define a fixed-point combinator in this way. In those languages, the textbook fixed-point combinator is the Y combinator proper.