[Haskell-cafe] A free monad theorem?
Chris Kuklewicz
haskell at list.mightyreason.com
Thu Aug 31 13:47:55 EDT 2006
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 } }
More information about the Haskell-Cafe
mailing list