On Fri, Sep 01, 2006 at 01:13:14AM +0200, Benjamin Franksen wrote:
So getting the value out of the monad is not a pure function (extract :: Monad m => m a -> a). I think I stated that, already, in my previous post.
The only generic way of "extracting" values from a monadic value is the bind operator. The lack of extract function is a feature :-) But now I know that you are not really claiming such a function exists.
The real question (the one that bugs me, anyway) is if one can give a precise meaning to the informal argument that if the definition of bind is to be non-trivial then its second argument must be applied to some non-trivial value at one point (but not, of course, in all cases, nor necessarily only once)
How about using monad laws, specifically: (return x) >>= f == f x We assume that >>= never uses it's second argument, so: (return x) >>= f == (return x) >>= g Combining it with the above monad law we get: f x == (return x) >>= f == (return x) >>= g == g x so f x = g x for arbitrary f and g. Let's substitute return for f and undefined for g: return x = undefined x so return x = undefined Now that seems like a very trivial (and dysfunctional) monad.
and that this implies that the computation represented by the first argument must somehow be 'run' (in some environment) in order to produce such a value.
Not sure what to do with this one. Certainly, for some monads the environment can be empty, eg. for Identity or []. For the IO monad the lack of the "run" function is a feature (Let's pretend that unsafePerformIO doesn't exist - in fact, there is no such function in Haskell 98), but you can say that the RTS runs the "main" IO computation. Informally, it seems obvious that you have to be able to run your monadic computations somehow - otherwise you wouldn't be writing them ;-) I am not sure you can prove it though.
-- And, of course, whether this is actually true in the first place. Would you say that your examples above are counter-examples to this statement (imprecise as it is, unfortunately)?
Well, no, they were counter-examples for the existence of the extract function. As you say, I misunderstood you intent. Best regards Tomasz