Haskell - Currying? Need further explanation.

Question

So something like

addList :: [int] -> int
addList = foldl1 (+)

Why does this work? The Currying part. Why no variable?

Thanks

Answer 1

If you define a function like f x y = bla, this is the same as f x = \y -> bla, which is the same as f = \x -> (\y -> bla). In other words f is a function which takes one argument, x, and returns another function which takes one argument, y, and then returns the actual result. This is known as currying.

Analogously when you do f x y, it's the same as (f x) y. I.e. you're calling the function f with the argument x. This returns another function, which you apply to the argument y.

So in other words when you do addList xs = foldl1 (+) xs, you're first calling foldl1 (+) which then returns another function, which you apply to xs. So since the function returned by foldl1 (+) is actually the same one as addList, you can just shorten it to addList = foldl1 (+).

Answer 2

The explanation from sepp2k is correct, I just want to point out (pun intended) that this application of currying has a name: It's called "point-free style". Here is a good explanation, including the pros and cons: http://www.haskell.org/haskellwiki/Pointfree

Answer 3

Besides currying, as sepp2k pointed out, here we use the so called eta reduction. It's one of the reduction rules of lambda calculus which is the basis of Haskell. It says that \x -> f x is equivalent to f when x does not appear in f.

Lets apply it to your case. I guess you are comfortable with a definition like addList xs = foldl1 (+) xs. We can rewrite this as addList = \xs -> foldl1 (+) xs and now applying the eta reduction rule we get addList = foldl1 (+).

This rule is based on the idea that two functions are equal if they give equal results when applied to the same arguments. The two functions here are f and g = \x -> f x where f : a -> b and we want to show that for all c : a, f c = g c. To prove it take an arbitrary c : a and apply it to g: g c = (\x -> f x) c = f c, the last equality is by another rule called beta reduction which says that function application is evaluated by substitution.