Type-signature vs. function equation in Haskell

I'm new to Haskell and to functional programming. I'm reading through Real World Haskell, and I've realized I'm confused by a few examples.

Specifically this is in Chapter 9, in the section "A Domain specific language for predicates", the examples which have the w x y z parameters.

I've boiled it down to this:

Why does this code compile?

f :: Int -> (Int -> Int)
f x y = x+y

main = do
  let q = f 4 5
  putStr  (show (q))

According to the type signature, f is clearly accepting 1 parameter and returning a function. However, it seems I can write the function equation so it will accept two parameters and return an int. Why is this possible? Does this mean the type signature is ignored?

Is this currying? Is this some kind of closure? If I understand this http://www.haskell.org/haskellwiki/Currying correctly, then it seems to be somewhat in reverse to currying as defined there - my f function is taking multiple arguments instead of a single one!

Also, can anyone answering please provide a link to some sort of Haskell documentation where this ability is stated (if possible at all).

EDIT:

After thinking about this for some time, what you two seem to be implying is that:

1) This syntax is syntact开发者_StackOverflow中文版ic sugar, f will always have a single parameter, no matter how many parameters are written in the equation

2) Upon application of f, the function body will (always?) be transformed into a stub (in effect, the returned function), where x is fixed to the parameter given (4), and y is a parameter.

3) Then this new function is applied to 5 which replaces y, and then the + function is evaluated.

What I was really interested in was, where exactly does it say something like "in the function equation, if you write more than one parameter, it's really syntactic sugar, and the following actually happens..." as I wrote above. Or is that so obvious to everyone except me?

Edit II:

The real eye-opener answer was in @luqui comment below, unfortunately I don't think I can mark a comment as an answer.

It is the fact that f x y = ... is actually syntactic sugar for: f = \x -> \y -> ...

And for me, everything else everyone below said follows from this.

I found a sort of source for this in the Gentle Introduction to Haskell, here: http://haskell.cs.yale.edu/tutorial/functions.html in section 3.1, called Lambda Abstractions.

In fact, the equations:

inc x = x+1 add x y = x+y

are really shorthand for:

inc = \x -> x+1 add = \x y -> x+y

While it doesn't use the phrase "syntactic sugar", it uses the more, uh, mathematically oriented word "shorthand", but as a programmer I read this as "sugar" :-)

---

It is currying. As the type signature says, f takes only one parameter. That would be 4. It then returns a function, which is immediately applied to 5. In fact, these two type signatures:

Int -> Int -> Int

and

Int -> (Int -> Int)

are equivalent in Haskell.

EDIT: this link about Partial Application, which I found inside the page you provided, explains this.

EDIT 2: You asked where the currying behavior of Haskell is defined. I don't know if this is what you're looking for: the Haskell 98 Revised Report, in section 3.3 Curried Applications and Lambda Abstractions, says:

Function application is written e1 e2. Application associates to the left, so the parentheses may be omitted in (f x) y.

---

The -> operator is right-associative, i.e. t -> t -> t is the same as t -> (t -> t).

If you re-write

f x y = x+y

in the equivalent form

f x = \y -> x + y

this conncetion should become obvious.

---

This is definitely a bit of currying. While I can't immediately find where in the documentation it explicitly states this behavior, all we have to do is check out our math a little about currying.

As we know, a function with the signature Int ->(Int -> Int) takes an Int, and returns a function that takes an Int and returns an Int. And we could just provide both of the Ints it needs to get that final int, like in your example:

f :: Int -> (Int -> Int)
f x y = x+y

And if we provide just the first argument, we get back a function that needs another argument. The bread and butter of currying.

Simply put, currying is right-associative. In other words, Int -> (Int -> Int) is the same as Int->Int->Int, just we added parenthesis to make it more obvious that:

f 3

Isn't missing an argument, but actually returns a function of type Int->Int.

It's kind of like back in math when you learn the associative property of addition.

3 + 2 + 1 = (3 + 2) + 1 = 3 + (2 + 1)

The result is the same, regardless of how we put our parentheses.

---

It's not really syntax sugar, it's just how function application works in Haskell.

Consider:

f :: Int -> Int -> Int -> Int 
f x y z = x + y + z

g = f 4
h = g 4 5

f 4 4 5 -- 13
g 4 5   -- 13
g 6     -- 13

You can play with this in ghci to confirm. g is a partial application of function f - its type is g :: Int -> Int -> Int.

You can also write:

((f 4) 4) 5  -- 13 

In this case (f 4) returns a partially applied function that takes two additional arguments, ((f 4) 4) returns a partially applied function that takes one argument, and the whole expression reduces to 13.

---

After thinking some more about this, I think the full explanation should be something along the lines of:

An Haskell function can only accept a single argument and return one parameter. Haskell allows us to pretend that several arguments are passed, but this form is treated as a series of nested lambda functions.

f x y = x + y

is treated as

(1) f = \x -> \y -> x + y

This treatment is true for lambda functions as well \x y -> x + y is treated as \x -> \y -> x + y

This allows us to treat type declaration as left-associative, that is: f :: Int -> Int -> Int is actually f :: (Int -> (Int -> Int)) which fits exactly to (1) above: f has no arguments, but is returning a function which accepts Int. This function in turn returns a function which accepts another Int, and returns an Int.

This means that if we want to return a function from a function, we don't have to do anything special, since that's Haskell's "default" mode.

This also means that given the type declaration f :: Int -> Int -> Int We can write f's implementatin ("equation") with 0, 1 or 2 parameters. If one or two parameter are specified, the compiler will generate the necessary lambdas to comply with the form f :: (Int -> (Int -> Int))

f = \x -> \y -> x + y

f x = \y -> x + y  -- \x -> is generated

f x y = x + y -- \x -> \y is generated

But in each of these cases, the function application appearing to accept two parameters will compile successfully, since it will always be translated to the first form, e.g.

f 4 5 --> (\x -> (\y -> x + y) 5 ) 4

Where the inner function application will return the curried form (x + 5)

This enables partial function application, where we can give f just one parameter and get back a partial function.

Also, changing the precedence in the function type:

f'' :: (Int -> Int) -> Int

changes the meaning - we accept a function getting an Int and returning one as the single parameter, and return an Int.
Assuming we've defined this function somewhere, then calling this function with Integer parameters, e.g.

f'' 4 5

will not compile.

Edit:

Also, even if the last arguments are in parenthesis, or are a type declaration, this holds.

E.g., in the following, the last pair of parenthesis is optional, since if they weren't there the compiler would put them anyway to get to the "lambda'd" form.

t4 :: (Int -> Int) -> (Int -> Int)
t4 f i = f i + i

Can be applied thus:

t4 (\x -> x*10) 5

Also, given:

type MyIntInt = Int -> Int

Then:

t5 :: MyIntInt -> MyIntInt

Is equivalent to t4, but confusing, since the meaning of MyIntInt is different in both places. The first one is the type of the first parameter.
The second one is "expanded" into Int -> Int (probably because of the right-associativity of the operator), which means that t5 can appear to accept 0 to 2 parameters in the function equation and function application (while actually always accepting 0 and returning embedded lambdas, as I've detailed above).

E.g. we can write t5 just like t4:

t5 f i = f i + i