7

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?

Improve this question
1
  • Where did you find the implementation? It looks like it "cheats" by recursing directly in Y. Commented Nov 27, 2018 at 3:31

2 Answers 2

Reset to default
5

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))
Improve this answer
Sign up to request clarification or add additional context in comments.

2 Comments

Thanks for your answer. I would love also to know how did we infer that f is of type (A => B) => A => B ?
Are you sure the version by @ecdhe is t equivalent to yours? In a call-by-value setting the eta-reduction does change semantics. I don't think this version should work, unless you eta-expand inside the Y on the right hand side.
4

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
Improve this answer

2 Comments

Great answer! Thank you.
great answer. I especially like the precision of your writing: "type of infinite depth" is precise and clear, the usual "infinite type" is confusing and vague.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.