[Haskell-cafe] Monad definition question

[Ilya Tsindlekht]

Does the definition of monad silently assume that if f and f' are equal
in the sense that they return the same value for any argument o correct
type then m >>= f = m >>= f'

More specifically, the definition says x >>= return = x. How does one
justify from this that x >>= (return . id) = x?

Are values of type a -> b in general assumed to be maps from the set of
values of type a into the set ov values of type b? (What bothers me is
that the problem whether two lambda-expressions define the same map is
clearly undecidable.)

More generally, is some kind of logic without equality more appropriate
for formalisation of Haskell then the usual kind(s) of logic with
equality?