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

[Robert Dockins]

> 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.
> I'd even say that the monadic values alone can be completely meaningless.
> They often have a meaning only relative to some environment, thus are
> (usually) _effectful_ computations. But we already knew that, didn't we?

It may help to remember that, in the mathematical context where monads where 
born (AKA category theory), a monad is generally defined as a functor with a 
join and a unit (satisfying some laws that I would have to look up).  The 
unit should be familiar (it's spelled 'return' in haskell), but join may not 
be.  Its type is

join :: Monad m => m (m a) -> m a

which is a lot like extract, except with one more "monad layer" wrapped around 
it.  IIRC the relevant identity here is:

x >>= f === join (fmap f x)

and with f specialzed to id:

join (fmap id x) === x >>= id
join x           === x >>= id

I'm not sure why (>>=) is taken as basic in Haskell.  At any rate, my point is 
that I think your questions might be better framed in terms of the behavior 
of 'fmap'.

> 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), 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. -- 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)?

> Ben




-- 
Rob Dockins

Talk softly and drive a Sherman tank.
Laugh hard, it's a long way to the bank.
       -- TMBG