Haskell `let` bindings in lambda calculus

Question

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?

Answer 1

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))))