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 } }
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
