The Why of Y (2001) [pdf] | Hacker News Reader

The Why of Y (2001) [pdf]

dreamsongs.com

29 pointspmoriarty6 comments

The article is called "The Why of Y", but there is no discussion of "why", just a derivation of the Y combinator. Pun aside, it should really be called "The How of Y". In fact, "how" is used four times in the first two sentences:

> Did you ever wonder how Y works and how anyone could ever have thought of it? In this note I’ll try to explain to you not only how it works, but how someone could have invented it.

Is there a "why"? That is, why would anyone care about the Y combinator? There's theoretical interest, of course, if you're into that kind of thing. It's also a great party trick, particularly if you're able to quickly reproduce it in Python or Javascript. Beyond that there is just one real-life, practical use I have ever found for the Y combinator. I was messing around with Smalltalk and I wanted to write a basic recursive factorial function. But Smalltalk requires some keyword to be able to do recursion, and I didn't know it. However, I did know how to use anonymous functions (I think they call them blocks), and I also knew the Y combinator, so I was successfully able to implement my recursive function without actually using recursion.

Another great exposition on the applicative-order Y combinator can be found at the end of Chapter 9 of The Little Schemer.

It is interesting to contrast with how in Haskell, one can simply define Y as

  Y f = f (Y f)

owing to the fact that it is lazily evaluated.

Of course, the definition we actually use is this:

    -- (1)
    fix f = let x = f x in x

Because it has better memory usage; the definition you provided is translated to the following STG:

    -- (2)
    fix f = let x = fix f in f x

So whereas #1 is a thunk that refers to itself, #2 is a recursive function, and importantly not tail-recursive.

I'm not proficient in Haskell, but how would the compiler be able to statically type that expression?

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

Because f is applied to an argument, it must be a function of generic type t -> u. Because y is applied to f, it must be a function of type (t -> u) -> v. Then the type of y f is v. Because f is applied to y f, t = v. Then the type of f (y f) is u. Because y f is defined as f (y f), the two expressions need to have the same type, t = u. Therefore f is of type t -> t and y is of type (t -> t) -> t.

It's true that the original non-recursive definition of Y doesn't typecheck in Haskell:

  Prelude> \f->(\x->f(x x))(\x->f(x x))

  <interactive>:5:14:
    Occurs check: cannot construct the infinite type: r0 ~ r0 -> t
    ...

Reply on news.ycombinator.com