[Haskell-cafe] A free monad theorem?

Tomasz Zielonka tomasz.zielonka at gmail.com
Thu Aug 31 16:16:38 EDT 2006

On Thu, Aug 31, 2006 at 07:23:55PM +0200, Benjamin Franksen wrote:
> I'd like to know if the following reasoning can be made more precise:
> As we all know, the monadic bind operation has type:
>         bind :: Monad m => m a -> (a -> m b) -> m b
> My intuition says that in order to apply the second argument to some
> non-trivial (i.e. non-bottom) value of type a, the bind operator needs to
> be able to somehow 'extract' a value (of type a) from the first argument
> (of type m a).

The bind operator doesn't have to neccesarily apply the second argument
to anything. What if m is Maybe, and the first arguments is Nothing?

And if the bind operator "wants" to apply the second argument to
something, it doesn't have to do it only once - consider the [] monad.

Other examples:

    get :: State s s        -- from Control.Monad.State
        there is no way you can extract an 's' value from "get" alone -
        you have to supply the state to the whole computation

    Cont (const ()) :: Cont () a        -- from Control.Monad.Cont

        whatever you do, you won't be able to extract an 'a' typed
        value, non-bottom from this computation. Cont is defined as:

            newtype Cont r a = Cont {runCont :: (a -> r) -> r)}

Best regards

More information about the Haskell-Cafe mailing list