[Haskell-cafe] Re: A free monad theorem?

[Tomasz Zielonka]

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