4

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?

Will Ness
  • 70,110
  • 9
  • 98
  • 181
Ben DalFavero
  • 161
  • 1
  • 7
  • 1
    you probably need to define `let times x y = x * y ...` otherwise doesn't make much sense. – karakfa Jan 06 '19 at 05:51
  • @karakfa Thank you! Small mental error on my part. Got ahead myself! I will edit. :) – Ben DalFavero Jan 06 '19 at 07:06
  • Haskell's `let` is not `let`, it is `letrec`. – Will Ness Jan 07 '19 at 09:48
  • @WillNess If `let` is actually `letrec`, does that mean `fix` is applied to every bindings, or only recursive ones? – Ben DalFavero Jan 07 '19 at 15:46
  • every and always. in theory at least; a compiler might realize there's no recursion and optimize. and we don't actually have to use fix. recursion can be implemented directly by the implementation, under the hood. – Will Ness Jan 07 '19 at 15:53

3 Answers3

5

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))))
rampion
  • 87,131
  • 49
  • 199
  • 315
  • Thank you! I was already aware of using `fix` along with the extra lambda to do recursion, but hadn't seen mutually recursive bindings done, so thanks! That's really cool. With you scoping example, I see that it's like my failed implementation, but with extra brackets. If I understand currently, l.c. is right associative, and thus these two expressions should evaluate the same, yes? Your example does work in GHCi. It's always cool to see that so much can be done with just the typed lambda calculus. – Ben DalFavero Jan 06 '19 at 07:14
  • Oh, I see the difference. I did `\square times ->` instead of `\times -> (\square`. This makes more sense. I still don't really understand why the brackets are needed. Maybe you could clarify? – Ben DalFavero Jan 06 '19 at 07:18
  • All u need is **U**: `Y = U . (. U)`. :) (well, **B** too). – Will Ness Jan 07 '19 at 09:51
3

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.

chi
  • 111,837
  • 3
  • 133
  • 218
2

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.

Ben DalFavero
  • 161
  • 1
  • 7