[Haskell-cafe] A free monad theorem?

[Tomasz Zielonka]

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
Tomasz