Fixed Point Combinator

[Nick Kallen]

http://www.deene.ufu.br/clean/monads.htm defines a way to find the factorial
of a number using a fixed point combinator. I'm having a little bit of
trouble with this because it's only covered sparsely in the document, and I
have no previous experience with such combinators.
    The combinator is defined as,

Y f= f (Y f)

And the factorial is defined as,

Y (\ loop n m -> (if (n<1) m (loop (n-1) (n*m) )))

I first stared at this in amazement wondering what the significance of loop
was. In fact, loop isn't defined--so I didn't know what was going on.
    I've come up with some ideas, but  I need help to fully understand this
stuff.

Certainly:
    loop can be replaced with anything (e.g., "foo") --it needn't be
defined.

And probably:
    the reason loop is there is that the function can't return (n - 1) (n
*m)--it's type is Int Int or rather undefined--and a function can't return
something of -that- type. Thus some function is used--applied to (n - 1) (n
* m) as in loop (n - 1) (n * m).

I was thinking that one could consider loop almost like a type constructor.
For a function, it's pretty damn useless; it has no definition and is never
used. But what exactly is the type of loop? Is it loop :: a b -> c?
    Now, assuming loop is a function, the only reason it doesn't need to be
defined is that it never actually gets used or applied to any arguments
(because of laziness). If all of my above reasoning is correct, the type
system must infer that loop is never used and thus needn't be defined. Is
this the case?

I realize that I've answered many of my own questions, but I'm hoping
someone can tell me with certainty that I'm correct--or incorrect as the
case may be--and provide the correct answers if I have erred..

-Nick