Re: [Haskell-cafe] Monadic correctness

17 Oct 2009

      Am Samstag 17 Oktober 2009 22:24:08 schrieb Andrew Coppin:
...
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
Are you sure that's really the type you want for runFoo ?
By the definition below, runFoo :: Foo x -> M -> IO x would be the natural type.
...
...
...
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
So,

(Foo f) >>= return
    ~> Foo $ \m -> do
            x <- f m
            let Foo g = return x
            g m
    ~> (since g is (\_ -> return x))
       Foo $ \m -> do
            x <- f m
            (\_ -> return x) m
    ~> Foo $ \m -> do
            x <- f m
            return x
    ~> (monad laws for IO)
       Foo $ \m -> f m
    ~> Foo f

That's number 1.

return a >>= f
    ~> Foo $ \m -> do
            x <- (\_ -> return a) m
            let Foo g = f x
            g m
    ~> Foo $ \m -> do
            x <- return a
            let Foo g = f x
            g m
    ~> Foo $ \m -> do
            let Foo g = f a
            g m
    ~> Foo $ \m -> unFoo (f a) m
    ~> Foo (unFoo $ f a)
    ~> f a

where I've used unFoo :: Foo x -> M -> IO x; unFoo (Foo f) = f,
that's number 2.

(Foo f >>= g) >>= h
    ~> Foo $ \m -> do
            y <- unFoo (Foo f >>= g) m
            let Foo h1 = h y
            h1 m
    ~> Foo $ \m -> do
            y <- (unFoo . Foo $ \m1 -> do
                    x <- f m1
                    let Foo g1 = g x
                    g1 m1) m
            let Foo h1 = h y
            h1 m
    ~> Foo $ \m -> do
            y <- do
                    x <- f m
                    let Foo g1 = g x
                    g1 m
            let Foo h1 = h y
            h1 m
    ~> Foo $ \m -> do
            y <- f m >>= \x -> unFoo (g x) m
            unFoo (h y) m
    ~> Foo $ \m ->
            (f m >>= \x -> unFoo (g x) m) >>= \y -> unFoo (h y) m
    ~> Foo $ \m ->
            f m >>= \x -> (unFoo (g x) m >>= \y -> unFoo (h y) m)

And

Foo f >>= (\z -> g z >>= h)
    ~> Foo $ \m -> do
            x <- f m
            let Foo k = (\z -> g z >>= h) x
            k m
    ~> Foo $ \m -> do
            x <- f m
            unFoo (g x >>= h) m
    ~> Foo $ \m ->
            f m >>= \x -> unFoo (g x >>= h) m
    ~> Foo $ \m ->
            f m >>= \x -> (\m1 -> (unFoo (g x) m1) >>= \y -> unFoo (h y) m1) m
    ~> Foo $ \m ->
            f m >>= \x -> (unFoo (g x) m >>= \y -> unFoo (h y) m)

That's number 3.
...
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)"...

Re: [Haskell-cafe] Monadic correctness

Daniel Fischer