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

[Benjamin Franksen]

Chris Kuklewicz wrote:
> 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). I would like to argue that this is because bind is
>> polymorphic in a, which makes it impossible to construct values of type
>> a 'out of thin air' (besides bottom). Thus, however bind is defined, the
>> only place where it can obtain a 'real' value of type a is from its first
>> argument. Although one might think that this implies the existence of
>> some function
>> 
>>         extract :: Monad m => m a -> a
>> 
>> it is obvious that this is too limiting, as the IO monad plainly shows.
>> Even monads that can be implemented in Haskell itself (the vast majority,
>> it seems) usually need some additional (monad-specific) argument to
>> their 'extract' (or 'run') function. However, even a value of type IO
>> a /does/ produce a value of type a, only the 'value producing
>> computation' is not a (pure) function. But how can all this be made more
>> precise with less handwaiving?
> 
> You can cheat a bit and write your own IO a -> a using GHC:
> 
> {-
> Taken from the shootout  at
>
http://shootout.alioth.debian.org/gp4/benchmark.php?test=knucleotide&lang=ghc&id=2
> -}
> 
> import GHC.Exts -- for realWorld# value
> import GHC.IOBase -- for IO constructor
> 
> {-# INLINE inlinePerformIO #-}
> inlinePerformIO :: IO a -> a
> inlinePerformIO (IO m) = case m realWorld# of (# _, r #) -> r
> 
> -- Now you can write things like this, which need IO action to define pure
> -- functions:
> 
> data Seq = Seq !Int !(Ptr Base)
> 
> instance Eq Seq where
>   (==)  (Seq (I# size1) (Ptr ptr1)) (Seq _ (Ptr ptr2)) = inlinePerformIO $
>   IO
> (\s -> eqmem size1 ptr1 ptr2 s)
> {-# INLINE eqmem #-}
> eqmem remainingSize ptr1 ptr2 s = if remainingSize ==# 0# then (# s , True
> #)
>    else case readInt8OffAddr# ptr1 0# s of { (# s, i8a #) ->
>         case readInt8OffAddr# ptr2 0# s of { (# s, i8b #) ->
>                if i8a /=# i8b then (# s, False #)
>                else eqmem (remainingSize -# 1#) (plusAddr# ptr1 1#)
>                (plusAddr#
> ptr2 1#) s } }

Would you (or someone else) care to explain what this exercise in advanced
ghc hacking has to do with my question? I don't exclude the remote
possibility that there is some connection but I don't get it.

Ben