[Haskell-cafe] A free monad theorem?

[Chris Kuklewicz]

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