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

[Tomasz Zielonka]

On Fri, Sep 01, 2006 at 01:13:14AM +0200, Benjamin Franksen wrote:
> So getting the value out of the monad is not a pure function (extract ::
> Monad m => m a -> a). I think I stated that, already, in my previous post.

The only generic way of "extracting" values from a monadic value is
the bind operator. The lack of extract function is a feature :-)
But now I know that you are not really claiming such a function exists.

> 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.

> and that this implies that the computation represented by the first
> argument must somehow be 'run' (in some environment) in order to
> produce such a value.

Not sure what to do with this one. Certainly, for some monads the
environment can be empty, eg. for Identity or []. For the IO monad the
lack of the "run" function is a feature (Let's pretend that
unsafePerformIO doesn't exist - in fact, there is no such function in
Haskell 98), but you can say that the RTS runs the "main" IO
computation.

Informally, it seems obvious that you have to be able to run your
monadic computations somehow - otherwise you wouldn't be writing them
;-) I am not sure you can prove it though.

> -- And, of course, whether this is actually true in the first place.
> Would you say that your examples above are counter-examples to this
> statement (imprecise as it is, unfortunately)?

Well, no, they were counter-examples for the existence of the extract
function. As you say, I misunderstood you intent.

Best regards
Tomasz