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

[Benjamin Franksen]

Tomasz Zielonka wrote:
> 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?

True, however if the instance for Maybe would have been defined
without /ever/ applying the second argument to anything, then wouldn't this
necessarily be a trivial monad (however one would need to define 'trivial'
here)?

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

Yes, I should have said: Any non-trivial definition of bind has to apply its
second argument at least in _some_ cases and _at least_ once to something
non-bottom.

> 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)}

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?

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