[Haskell-cafe] Monadic correctness

Andrew Coppin andrewcoppin at btinternet.com
Sat Oct 17 16:24:08 EDT 2009


Edward Z. Yang wrote:
> Excerpts from Andrew Coppin's message of Sat Oct 17 15:21:28 -0400 2009:
>   
>> Suppose we have
>>
>>    newtype Foo x
>>    instance Monad Foo
>>    runFoo :: Foo x -> IO x
>>
>> What sort of things can I do to check that I actually implemented this 
>> correctly? I mean, ignoring what makes Foo special for a moment, how can 
>> I check that it works correctly as a monad.
>>     
>
> A proper monad obeys the monad laws:
>
> http://www.haskell.org/haskellwiki/Monad_Laws
>
> You can probably cook up some quickcheck properties to test for these,
> but really you should be able to convince yourself by inspection  that
> your monad follows these laws.
>   

I'm reasonably confident it works, but not 100% sure...

newtype Foo x = Foo (M -> IO x)

instance Monad Foo where
  return x = Foo (\_ -> return x)

  (Foo f1) >>= fn = Foo $ \m -> do
    x <- f1m
    let Foo f2 = fn x
    f2 m

runFoo (Foo f) = do
   let m = ...
   f m

I can do something like "runFoo (return 1)" and check that it yields 1. 
(If it doesn't, my implementation is *completely* broken!) But I'm not 
sure how to proceed further. I need to assure myself of 3 things:

1. runFoo correctly runs the monad and retrives its result.
2. return does that it's supposed to.
3. (>>=) works correctly.

Doing "runFoo (return 1)" seems to cover #1 and #2, but I'm not so sure 
about #3... I guess I could maybe try "runFoo (return 1 >>= return)"...



More information about the Haskell-Cafe mailing list