[gregfjohnson]

A nice way to think about eta-reduction is that it asserts something about the types of expressions in lambda calculus, namely that every expression is in fact a function.

If an expression M can appear in the left position of the function application operation, this implies that M is a function.

By way of analogy, if I have a formula x == x+0, this implies that x is a number.

Or, s == s + '' would imply that s is a string.

So, if M == lambda x. M(x), this is saying that M is a function.