In this treatment of let a lambda calculus version of let is given
(\f.z)(\x.y)
with the words
f is defined by f x = y in the expression z, and then as
let f x = y in z
I know from a beginner's perspective how Haskell's let works, i.e., the definitions follows the let and expressions (do something with those definitions) follows the in.
let <definitions> in <expression>
But this most general lambda calculus description is baffling. For example, I assume there could be a Haskell lambda function version of let f x = y in z. Could someone write this out -- and maybe give an example or two -- in Haskell? Just guessing, it seems a first lambda function takes a second lambda function -- somehow?
(\x -> y)(\f -> z)
But this is just a guess.
The Haskell version is exactly the same as the lambda calculus version but with Haskell syntax:
(\f -> z) (\x -> y)
Why?
let f x = y in z
^^^^^^^ "local" function called "f"
let f = (\x -> y) in z
^^^^^^^^^^^^^ same thing without the function syntax
We are just introducing a new variable f which holds the value (\x -> y).
How do we introduce a variable in lambda calculus? We define a function and then call it, like this:
(\x.zzzzzzzzzzzzzzzzzzz) 1
^^^^^^^^^^^^^^^^^^^ inside this part, x is 1
(lambda calculus doesn't have numbers, but you get the idea)
So we're just introducing a variable called f whose value is (\x.y)