[Haskell-cafe] Re: QuickCheck [Architecturally flawed]

[Ryan Ingram]

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
<andrewcoppin at btinternet.com> wrote:
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>