Type-signature vs. function equation in Haskell

Question

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 syntactic 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" :-)

Answer 1

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.