To understand the theory of recursive functions you must understand fixed points, but I think there's a simpler way to understand the magic of the Y combinator.

To understand the theory of recursive functions you must understand fixed points, but I think there's a simpler way to understand the magic of the Y combinator. Here's how it works. Say we have a recursive function like map: map f [] = [] -- We'll ignore the base case since there's no recursion here map f (x:xs) = f x : map f xs -- This is the interesting part We want to write this more primitively, without explicit recursion. How can we do that? Well, if it's possible at all, we obviously need to get rid of the map on the right hand side of the second case. How? Well, let's abstract over the recursive call, replacing it with a function that we'll add as parameter to our definition: map' _ f [] = [] -- Still boring map' g f (x:xs) = f x : g g f xs -- Pay attention for later! (Read map' as "map-prime", i.e., a variant of the definition of map.) All we've done so far is replaced map' where it should be on the right-hand side of its own definition with g, and then added g as parameter of the function. We end up with a double g on the right-hand side because of that added parameter. OK, now what? Well, we need somehow to make g be map', the thing we're defining. which means we need somehow to pass our definition of map' to itself, so that (in the second case) we'd end up with something that evaluates to: map' map' f (x:xs) = f x : map' map' f xs Then the right hand side would obviously be right; it's what we were shooting for at the start (assuming we can get map' map' to equal map, which is what we're trying to do). The left hand side looks a little strange [0], but it's just saying that we need the first parameter of our definition to be the the thing we're defining. So how do we make this happen? Well, what is map map f (x:xs)? It's map applied to itself, then to some other arguments we need. So the key, it seems, is to figure out how to apply map to itself. Well, in the lambda calculus that's pretty easy [1]: why f x y = f f x y That is, why is just lambda f. lambda x. lambda y. (f f) x) y OK, so fix takes a function and applies it to itself (after applying it first to arguments x and y). Great. That's what we needed. Now we can take our defintion of map' (the one marked Pay attention for later! above) and do this: map = why map' And I've re-used the name map there because we can easily show that this definition is equivalent to our original definition of map by showing that it reduces to the same expression: map f (x:xs) = why map' f (x:xs) == (by def. of `why`) map' map' f (x:xs) == (by def. of `map'` f x : map' map' f xs Which, if you keep expanding the expression map' map' f xs, you will see is indeed equal to the definition of map. Voilà. So that wasn't too hard. It's basically two steps: (1) abstract over the recursive call, then (2) figure out how to pass the function you're defining to itself. If you look at the Y combinator, you'll see that that's exactly what's going on there. If this didn't make a lot of sense to you, it's probably because I wrote it on my iPad at 4:30 in the morning. It really is just those two steps: abstract over the recursive call, then self-apply. ... To get deeper into the recursive mindset (if you're not there yet) and to build up deliberately to the Y combinator, take a look at one of my favorite books on functional programming, The Little Schemer [2]. (And watch out for the jelly stains!) ------ 0. And it's ill typed, but never mind that. It's not possible to define the Y combinator (or any other fixed-point combinator) in the simply typed-lambda calculus, so just imagine that my Haskell-style syntax is untyped, like the basic lambda calculus. 1. Although, again, there's no way to give fix a good type in the simply typed lambda calculus. 2. http://www.amazon.com/The-Little-Schemer-4th-Edition/dp/0262560992 http://www.amazon.com/The-Little-Schemer-4th-Edition/dp/0262...