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
Andrew Coppin wrote:
After many hours of effort, I came up with these:
data Writer x instance Monad Writer run_writer :: Writer () -> ByteString write1 :: Bool -> Writer () write8 :: Word8 -> Writer () write16 :: Word16 -> Writer () write32 :: Word32 -> Writer () write64 :: Word64 -> Writer () writeN :: Word8 -> Word32 -> Writer ()
data Reader x instance Monad Reader run_reader :: Reader x -> ByteString -> x is_EOF :: Reader Bool read1 :: Reader Bool read8 :: Reader Word8 read16 :: Reader Word16 read32 :: Reader Word32 read64 :: Reader Word64 readN :: Word8 -> Reader Word32
How would you write QuickCheck properties for these?
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?
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?
In the end, what I opted to do was define various properties where I take some arbitrary data, write it with the Writer monad, then read it back with the Reader monad and confirm that the data stays identical. (This actually fails for writeN, which writes the N least-significant bits of the supplied data, so you need to apply some masking before doing equity. Or, equivilently, reject some test values...)
Looking at the QuickCheck paper, it seems I should probably have done some checking that the size of the output is correct. I didn't actually bother because it's really easy to get right, whereas strickiness with bit-shifts and indexing is all too easy to screw up.
What I finally did was try writing/reading with each primitive (to check that actually works properly), and then again with a random number of individual bits packed on each side to give random alignment (to check that the index adjustments actually work right). It's easy to make the code work correctly with a certain alignment, but fail spectacularly otherwise. It's packed at *both* ends because it's also quite easy to make it write out the correct bit pattern, but leave the bit pointer with the wrong value, causing subsequent writes to screw up.
How would you approach this one? All hints welcomed.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe