[Haskell-cafe] Re: A free monad theorem?
Benjamin Franksen
benjamin.franksen at bessy.de
Thu Aug 31 15:15:20 EDT 2006
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
More information about the Haskell-Cafe
mailing list