[Haskell-cafe] Monadic correctness

[Daniel Fischer]

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)"...