
Ryan Ingram wrote:
I think you can use the duality of Writer/Reader to help you here; you have the law that, for suitable "dual" computations r and w,
run_reader r (run_writer (w x)) == x
Then you can build up a list of rules specifying which computations are dual; read64 is dual to write64, for example. You can then have some laws like:
if r1 is dual to w1, and r2 is dual to w2, then r1 >>= \x -> r2 >>= \y -> (x,y) is dual to \(x,y) -> w1 x >> w2 y
if r1 is dual to w1, and r2 is dual to w2, then read1 >>= \b -> case b of True -> liftM Left r1 ; False -> liftM Right r2 is dual to \x -> case x of Left l -> w1 l; Right r -> w2 r
You can then use these to build up more complicated reader/writer duals and verify that the main "identity" law holds.
It's a little bit tricky; QuickCheck is not good at dealing with polymorphic data, but you could generalize this to a simple term ADT: data SimpleTerm = Leaf Word8 Word32 | Pair SimpleTerm SimpleTerm | Switch (Either SimpleTerm SimpleTerm) deriving Eq
and make a suitable "arbitrary" instance for SimpleTerm to test your reader/writer. Leaf would test readN/writeN, or you can make custom leaves to test the other operations.
-- ryan
On Fri, Jul 11, 2008 at 11:10 AM, Andrew Coppin
wrote: For starters, what would be a good set of properties to confirm that any monad is actually working correctly? More particularly, how about a state monad? It's easy to screw up the implementation and pass the wrong state around. How would you catch that?
See http://www.cs.chalmers.se/~rjmh/Papers/QuickCheckST.ps on QuickCheck tests for monadic properties. The basic idea is to write a Gen action to generate a list of actions in your target monad.
Secondly, the monads themselves. I started writing things like "if X has the lowest bit set then the lowest bit of the final byte of the output should be set"... but then all I'm really doing is reimplementing the algorithm as a property rather than a monad! If a property fails, is the program wrong or is the property wrong This is a fundamental issue with the way that QuickCheck, or any other automatic test generator, works. QuickCheck tests are a formal specification of the properties of your program, so they have the same fundamental complexity as your program. See http://en.wikipedia.org/wiki/Kolmogorov_complexity for more on this. The only exception is when a complicated algorithm produces a simple result, such as sorting or square roots. There are two ways of dealing with this:
1: Write abbreviated properties that only specify part of your program's behaviour, and trust to single-case tests and code inspection for the rest. For instance a test for "reverse" done this way might test that reverse "abcd" = "dcba" and otherwise just check that the input and output strings were the same length. 2: Accept that your tests are going to be as long as the program itself. When a test fails, just figure out which is at fault (you have to do this for any testing method anyway). You still gain reliability because you have implemented the algorithm in two different ways, so hopefully a defect in one will not have a matching defect in the other. I say "hopefully" because the history of N-version programming suggests that such errors are not independent, even when the versions are developed by different teams.