[Haskell-cafe] Re: A free monad theorem?
tomasz.zielonka at gmail.com
Fri Sep 1 06:38:13 EDT 2006
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
> f x = g x
> for arbitrary f and g. Let's substitute return for f and
> undefined for g:
> return x = undefined x
> 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.
More information about the Haskell-Cafe