[Haskell-cafe] Monad definition question

[Robin Green]

On Fri, 04 May 2007 14:42:53 +0300
Ilya Tsindlekht <eilya497 at 013.net> wrote:

> 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'

How could it be otherwise? How are you going to distinguish between f
and f' if they are indistinguishable functions, in Haskell?

> 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?

Yes - if _|_ is considered to be a value.

> (What bothers
> me is that the problem whether two lambda-expressions define the same
> map is clearly undecidable.)

Yes. But this is a fundamental mathematical issue which isn't at all
specific to Haskell, of course. It suggests using some sort of
intensional type theory, so that you have to explicitly prove lambda
expressions to be equal.

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

I suggest you look into Observational Type Theory.
-- 
Robin