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?

Pizzeria

Assuming this is real code, just fire whoever came up with this. – Hypersonic

@MartinJames: Huh? What do you think is wrong with the code? It's not the best way to define the function, but it's the simplest. – Orleans

@MartinJames, that function is a well-studied function called the Y Combinator. (I think that's right - I can't double-check Wikipedia at the moment!) Anyway, maybe you would get fired for being such a philistine :-) – Radiophotograph

@AaronMcDaid: It's actually not the Y combinator, it's just equivalent to it; this is a fixed-point function with explicit named recursion, while the Y combinator's innovation is to implement recursion without any language support for it. P.S. Try appending ?banner=none to Wikipedia URLs :) – Cuckoo

I'd also like to add, that Y combinator is particular implementation of fixed-point combinator in untyped lambda calculus: λf.(λx.f (x x)) (λx.f (x x)). However, this cannot be simply typed in Haskell (and is impossible to type in simply-typed lambda calculus; pun intended). The need for self application (x x) requires recursion at type level. In Haskell, you can avoid type recursion a = a -> a by wrapping it into newtype Rec a = In { out :: Rec a -> a }. – Seclusive

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.

Cuckoo

@TheIronKnuckle: Pretty much! It's called [unification](en.wikipedia.org/wiki/Unification_(computer_science)). – Cuckoo

Answer 2

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.

Phenosafranine

Answer 3

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

Quadriplegia

Answer 4

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.

Growler