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

[Benjamin Franksen]

Andrea Rossato wrote:
> Il Fri, Sep 01, 2006 at 07:22:02AM +0200, Tomasz Zielonka ebbe a scrivere:
>> On Fri, Sep 01, 2006 at 01:13:14AM +0200, Benjamin Franksen wrote:
>> > 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.
>> 
>> The only generic way of "extracting" values from a monadic value is
>> the bind operator. The lack of extract function is a feature :-)
>> But now I know that you are not really claiming such a function exists.
> 
> I do not understand this discussion, but I'd like to.
> 
> Can you please tell me what you are talking about in terms of this
> example?

Sure. Your definition of bind (>>=):

> newtype M a = TypeConstructor {unpack::(a, String)}
>     deriving (Show)
> 
> instance Monad M where
>     return a = (TypeConstructor (a,""))
>     (>>=) m f = TypeConstructor (a1,b++b1)
>                 where (a,b) = unpack m
>                       (a1,b1) = unpack (f a)

applies f to something that it has extracted from m, via deconstructor
unpack, namely a. Thus, your bind implementation must know how to produce
an a from its first argument m. In this case it doesn't even have to use
an 'environment', since the value a is really packed together with the
monadic value m. In fact for this monad you /do/ have an 'extract'
function:

        extract = fst . unpack

However, there are monads like IO for which it is not possible to define
such a function (and for IO this is indeed the whole point). However, in
order to 'run' (i.e. finally actually use) a monadic value that involves an
application of bind, the latter would have to supply some argument to its
second argument (which is a function), so there must be some way to 'get an
a out of' the first argument m. I struggle to make this 'somehow get an a
out of the m' more precise.

Cheers
Ben