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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
