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)"... _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe