[Haskell-cafe] Monadic correctness
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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monadic correctness
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. Cheers, Edward ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monadic correctness
On Sat, Oct 17, 2009 at 3:21 PM, Andrew Coppin andrewcop...@btinternet.com wrote: 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. Anything which satisfies the monad laws is a monad. In other words, do you have: return a = f = f a m = return = m (m = f) = g = m = (\a - f a = g) When I bother, I usually just work out the proofs by hand. -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monadic correctness
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)... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monadic correctness
On Sat, Oct 17, 2009 at 3:24 PM, Andrew Coppin andrewcop...@btinternet.com wrote: 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) In this case it is trivial, Foo = ReaderT M IO which is a monad. If you want, you can verify for yourself that this is a monad. It isn't, however, uncommon for custom monads to be (equivalent to) stacks of monad transformers. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monadic correctness
Derek Elkins wrote: On Sat, Oct 17, 2009 at 3:24 PM, Andrew Coppin andrewcop...@btinternet.com wrote: I'm reasonably confident it works, but not 100% sure... newtype Foo x = Foo (M - IO x) In this case it is trivial, Foo = ReaderT M IO which is a monad. Ah yes, of course... I keep forgetting that the Reader monad doesn't do what it sounds like it does! Oh well. ;-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monadic correctness
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
Re: [Haskell-cafe] Monadic correctness
Daniel Fischer wrote: 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. M is a type containing a bunch of IORefs. runFoo generates M, feeds M to Foo x, and then does magical stuff with M afterwards. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
