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