How does currying work with lambdas in Haskell?

Question

Just looking at learn you a Haskell (great work) and under the section curried functions there is an example that says the following two functions are the same:

addThree x y z = x + y + z  
addThree = \x -> \y -> \z -> x + y + z  

What confuses me here is how currying is applied to lambda(s). With the type of the function being

addThree :: (Num a) => a -> a -> a -> a  

When lambdas are used is the function equal to \x -> (\y -> (\z -> x + y + z)) ? If this is the case, then is x + y treated as a constant in the innermost lambda? That is, \z -> c + z where c is x + y ?

Answer 1

When reading type signatures like addThree :: Num a => a -> a -> a -> a you should mentally add in the appropriate parentheses as arrows right associate

addThree :: Num a => a ->  a ->  a -> a
addThree :: Num a => a -> (a -> (a -> a))

which perhaps helps to describe how single-argument lambdas are sufficient to represent a function like this.

When talking about curried lambdas, you can look at things from a few directions. Let's examine that inner fragment, for instance

\z -> x + y + z

If that were all you were given and asked to interpret it, you'd have to throw your hands up in frustration—there's no definition at all for what x and y should mean. They are known as "free" variables because they are not constrained by the lambda.

In order to give them definition, we must wrap more lambdas which bind meaning to x and y.

\x -> \y ->     \z -> x + y + z       -- ok!

So, looking from the inside out, the expression is meaningless without those outer lambdas.

However, as you begin to evaluate the expression under application

(\x -> \y -> \z -> x + y + z) 1 2 3

then a different story emerges. Now, you must handle each lambda binding entirely on its own. The rule is that in order to evaluate a lambda being applied to a value, you substitute the bound variable for that value everywhere inside of it.

(\x -> \y -> \z -> x + y + z) 1 2
(      \y -> \z -> 1 + y + z)   2
(            \z -> 1 + 2 + z)    

So, from the outside, the expression \z -> x + y + z never exists, the x and y are eliminated before we get that far.

It's worth noting, however, that this is not quite the same as c + z still! We do not evaluate the body of the inner lambda prior to binding the third argument. There's, in some sense, no way to know what's inside a lambda until we give it some value; (\z -> 1 + 2 + z) is completely opaque. Only once the final argument has been applied can we begin to evaluate the addition inside the body.

Broadly this is what's known as the difficulty of working "underneath a binder".