nick8325 / quickcheck

Automatic testing of Haskell programs.
Other
711 stars 119 forks source link

RFC: New method, generate values in (==) equivalence class (for quotient types) #214

Open Icelandjack opened 6 years ago

Icelandjack commented 6 years ago

Sometimes we want to generate structurally different but equal elements, for set we may want a generator for Set [1,2,3], Set [3,2,1], ..

This is an idea to add equivArbitrary (please propose a better name, approach etc) to the Arbitrary class with a default definition for arbitrary = join equivArbitrary:

class Arbitrary a where
  arbitrary :: Gen a
  arbitrary = join equivArbitrary

  equivArbitrary :: Gen (Gen a)
  equivArbitrary = do
    a <- arbitrary
    pure (pure a)

  {-# Minimal arbitrary | equivArbitrary #-}
  ..

Set: Outer-most Gen initializes the model (eg Set [1,2,3]) that the inner-most Gen gets to shuffle (Set [1,3,2], Set [3,2,1] ..):

newtype Set a = Set [a] deriving newtype Show

instance Ord a => Eq (Set a) where
  (==) :: Set a -> Set a -> Bool
  Set as == Set bs = sort as == sort bs

-- >> equivSet <- toIO (equivArbitrary @(Set Int))
-- >> equivSet
-- [-16,7,1,13]
-- >> equivSet
-- [13,-16,7,1]
-- >> equivSet
-- [13,1,-16,7]
instance Arbitrary a => Arbitrary (Set a) where
  equivArbitrary :: Gen (Gen (Set a))
  equivArbitrary = do
    as <- arbitrary
    pure $ do
      shuffle'd <- shuffle as
      pure (Set shuffle'd)

toIO :: Gen (Gen a) -> IO (IO a)
toIO = generate . fmap generate

This allows us to construct the example in 4.4 Testing for Invariance (Random Testing of Purely Functional Abstract Datatypes) in a backwards compatible way for every Arbitrary type without defining a new class:

-- (Equiv a) values contain two (a)-values (x :=: y) such that (x == y)
data Equiv a = a :=: a

-- >> equivSet <- toIO (equivArbitrary @(Equiv (Set Int)))
-- >> equivSet
-- [19,11,-25,-20,-8] :=: [-20,19,11,-25,-8]
-- >> equivSet
-- [19,11,-8,-20,-25] :=: [-20,-8,11,19,-25]
-- >> equivSet
-- [19,-25,-8,-20,11] :=: [11,-25,19,-8,-20]
instance Arbitrary a => Arbitrary (Equiv a) where
  equivArbitrary :: Gen (Gen (Equiv a))
  equivArbitrary = do
    gen <- equivArbitrary
    pure (liftA2 (:=:) gen gen)
property $ \x (q :=: q') -> enqueue x q == enqueue x q'
property $ \  (q :=: q') -> isEmpty   q == isEmpty   q' ..
ggreif commented 6 years ago

Sometimes you say equivArbitrary and other times equiArbitrary.

Icelandjack commented 6 years ago

fixed

Lysxia commented 6 years ago

Is it better to extend Arbitrary instead of creating a different class for this?