Understanding the implementation of Y-Combinator

Question

I would like to understand in mint detail please how we managed to get from the lambda calculus expression of Y-combinator :

Y = λf.(λx.f (x x)) (λx.f (x x))

to the following implementation (in Scala) :

def Y[A, B](f: (A => B) => A => B): A => B = (x: A) => f(Y(f))(x)

I am pretty new to functional programming but I have a decent understanding of lambda calculus and how the substitution process works. I am having however some hard time understanding how did we get from the formal expression to the implementation.

Besides, I would love to know how to tell the type and number of arguments of my function and its return type of whatever lambda?

Answer 1

First, the Scala code is a long way of writing:

def Y[A, B](f: (A => B) => A => B): A => B = f(Y(f))

Here, f is partially applied. (It looks like the code author chose to use a lambda to make this more explicit.)

Now, how do we arrive at this code? Wikipedia notes that Y f = f (Y f). Expanding this to something Scala-like, we have def Y(f) = f(Y(f)). This wouldn't work as a definition in lambda calculus, which doesn't allow direct recursion, but it works in Scala. To make this into valid Scala, we need to add types. Adding a type to f results in:

def Y(f: (A => B) => A => B) = f(Y(f))

Since A and B are free, we need to make them type parameters:

def Y[A, B](f: (A => B) => A => B) = f(Y(f))

Since it's recursive, we need to add a return type:

def Y[A, B](f: (A => B) => A => B): A => B = f(Y(f))

Answer 2

Note that what you wrote is not an implementation of the Y combinator. The "Y combinator" is a specific "fixed-point combinator" in the λ-calculus. A "fixed-point" of a term g is just a point x such that,

g(x) = x 

A "fixed-point combinator" F is a term that can be used to "produce" fix points. That is, such that,

g(F(g)) = F(g)

The term Y = λf.(λx.f (x x)) (λx.f (x x)) is one among many that obeys that equation, i.e. it is such that g(Y(g)) = Y(g) in the sense that one term can be reduced to the other. This property means such terms, including Y can be used to "encode recursion" in the calculus.

Regarding typing note that the Y combinator cannot be typed in the simply typed λ-calculus. Not even in polymorphic calculus of system F. If you try to type it, you get a type of "infinite depth". To type it, you need recursion at the type level. So if you want to extend e.g. simply typed λ-calculus to a small functional programming language you provide Y as a primitive.

You're not working with λ-calculus though, and your language already comes with recursion. So what you wrote is a straightforward definition for fixed-point "combinator" in Scala. Straightforward because being a fixed-point follows (almost) immediately from the definition.

Y(f)(x) = f(Y(f))(x)

is true for all x (and it is a pure function) therefore,

Y(f) = f(Y(f))

which is the equation for fixed-points. Regarding the inference for the type of Y consider the equation Y(f)(x) = f(Y(f))(x) and let,

f : A => B
Y : C => D 

since Y : C => D takes f : A => B as an input then,

C = A => B

since Y f : D is an input of f : A => B then

D = A

and since the output Y f : D is the same as that of f(Y(f)) : B then

D = B

thus far we have,

Y : (A => A) => A 

since Y(f) is applied to x, Y(f) is a function, so

A = A1 => B1 

for some types A1 and B1 and thus,

Y : ((A1 => B1) => (A1 => B1)) => A1 => B1