CODEWITHSUNDEEP
haskellrecursionletlambda-calculusletrec
Ben DalFavero
Ben DalFavero

Reputation: 161

Haskell `let` bindings in lambda calculus

I want to understand how let bindings work in Haskell (or maybe lambda calculus, if the Haskell implementation differs?)

I understand from reading Write you a Haskell that this is valid for a single let binding.

let x = y in e == (\x -> e) y

This makes sense to me, since it's consistent with how bindings work in the lambda calculus. Where I'm confused is using multiple let bindings, where one binding can reference the bindings above. I will provide a trivial example.

Original code:

let times x y = x * y
    square x = times x x
in square 5

My guess at the implementation:

(\square times -> square 5) (\x -> times x x) (\x -> x * x)

This seems not to work because times is not defined when square is called by the lambda. However, this can by solved by this implementation:

(\square -> square 5) ((\times x -> times x x) (\x -> x * x))

Is this the proper way to implement this binding, at least in the lambda calculus?

Upvotes: 4

Views: 1459

Answers (3)

Ben DalFavero
Ben DalFavero

Reputation: 161

I will answer my own question to maybe provide a helpful perspective to those who visit this question.

We want to implement the following program with two let bindings:

let times a b = a * b
    square x = times x x
in square 5

To start with, let's simplify this to the essence of what we want:

square 5

Simple enough. However, square in this case is undefined! Well, we can bind it using the mechanism our language provides us with - a lambda. This gives us (\ square -> square 5) (\x -> times x x). Now square is defined, but its cousin times is not... Well, we need another lambda! Our final program should look like this:

(\times -> (\square -> square 5) (\x -> times x x)) (\a b -> a * b)

Notice that the (\times -> ...) completely encloses our last step, so that times will be in scope as it is bound. This is consistent with the answer given by @rampion, and reduces as follows:

(\times -> (\square  -> square 5) (\x -> times x x)) (\a b -> a * b) =>
(\square -> square 5) (\x -> (\a b -> a * b) x x)                    =>
(\square -> square 5) (\x -> (\b -> x * b) x)                        => 
(\square -> square 5) (\x -> x * x)                                  => 
(\x -> x * x) 5                                                      =>
5 * 5                                                                => 
25

If the square function had not depended on times, we could have easily written (\times square -> ..... The dependency means that we must nest these two environments, one containing times, and another inside of that which can use its definition.

Thanks for all of your help! I'm blown away by the simplicity and power of the lambda calculus.

Upvotes: 2

chi
chi

Reputation: 116174

Note that multiple let bindings can be reduced to a single one, defining a pair (tuple, in the general case). E.g. we can rewrite

let times x y = x * y
    square x = times x x
in square 5

as

let times = \x y -> x * y
    square = \x -> times x x
in square 5

then

let (times, square) = (\x y -> x * y, \x -> times x x)
in square 5

then, if wanted,

let pair = (\x y -> x * y, \x -> fst pair x x)
in snd pair 5

After that, we can apply the usual lambda calculus translation. If the pair definition ends up to be recursive, as in the case above, we need a fixed point combinator.

(\pair -> snd pair 5) (fix (\pair -> (\x y -> x * y, \x -> fst pair x x)))

Note that this translation does not play along type inference algorithms, which handle let in a special way, introducing polymorphism. This is not important if we only care about the dynamic aspects of our program, though.

Upvotes: 3

rampion
rampion

Reputation: 89093

The times/square example can be expressed in terms of lambda functions using scoping:

(\times -> (\square -> square 5)(\x -> times x x))(\x y -> x * y)

But scoping isn't enough for recursive or mutually recursive let-bindings like

let ones = 1 : ones in take 5 ones

let even n = n == 0 || odd (abs n - 1)
    odd n  = n /= 0 && even (abs n - 1)
in even 7

In the lambda calculus you can define the y-combinator for recursion as

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

This lets you define functions and values in terms of themselves. That formulation isn't legal haskell due to typing constraints but there are ways around that.

Using the y-combinator lets us express the above let-bindings using the lambda calculus:

(\ones -> take 5 ones)((\f -> (\x -> f (x x))(\x -> f (x x)))(\ones -> 1 : ones))

(\evenodd -> evenodd (\x y -> x) 7)((\f -> (\x -> f (x x))(\x -> f (x x)))(\evenodd c -> c (\n -> n == 0 || evenodd (\x y -> y) (abs n - 1)) (\n -> n /= 0 && evenodd (\x y -> x) (abs n - 1))))

Upvotes: 5

Related Questions