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?
On Fri, 04 May 2007 14:42:53 +0300
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'
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
participants (2)
-
Ilya Tsindlekht -
Robin Green