[Haskell-cafe] Re: A free monad theorem?
Robert Dockins
robdockins at fastmail.fm
Thu Aug 31 20:02:50 EDT 2006
> 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
More information about the Haskell-Cafe
mailing list