On Fri, 04 May 2007 14:42:53 +0300 Ilya Tsindlekht <[EMAIL PROTECTED]> 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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
