On Fri, Sep 01, 2006 at 07:22:02AM +0200, Tomasz Zielonka wrote:
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.
I just realized that I haven't addressed your exact problem, but maybe you'll be able to use a similar reasoning to prove your theorem. What (I think) I proved is that: if >>= never uses its second argument, then the monad is dysfunctional (maybe not even a monad at all). Again, informally, it is obvious. Best regards Tomasz