Tomasz Zielonka 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)
>
>
>     (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
```