collections-api-1.0.0.0: API for collection data structures.

PortabilityMPTC, FD, undecidable instances
Stabilityexperimental
Maintainerjeanphilippe.bernardy; google mail.

Data.Collections.Properties

Description

The purpose of this module is twofold:

  1. Check instances of the classes in the collection framework.
  2. Give those classes more formal semantics.

Therefore, this acts as a contract between the collections users and implementers.

Each function in this module returns a list of (property_name, propterty) for a given class (or set of classes). Each function is parameterized on the type of the collection to check, so a value witnessing the type must be passed. This value is guaranteed not to be evaluated, so it can always be undefined.

These properties allow to verify, with a high degree of confidence, that instances of the classes defined in Data.Collections satisfy the prescribed properties.

You will note that properties depend on the Eq class. This means that

  • properties are verified up to Eq equivalence.
  • Infinite structures and other bottoms are not testable with this module.

Synopsis

Documentation

unfoldable_properties :: forall c a. (Arbitrary c, Arbitrary a, Ord a, Show a, Show c, Eq c, Eq a, Unfoldable c a) => c -> [(Property, String)]Source

unfoldable_properties returns the following properties:

singleton
  singleton a == insert a empty
insertMany
  insertMany l c == Foldable.foldr insert c l
insertManySorted
  insertManySorted l c == Foldable.foldr insert c l
     where l = List.sort l0

foldable_properties :: forall c a. (Arbitrary c, Arbitrary a, Show a, Show c, Eq c, Eq a, Foldable c a) => c -> [(Property, String)]Source

foldable_properties returns the following properties:

size
  size c == foldr (const (+1)) 0 c
null
  null c <==> all (const False) c
isSingleton
  isSingleton c <==> size c == 1
eq_elem
  c1 == c2 ==> elem x c1 == elem x c2 -- note that the order of folding is not enforced, and that the converse is not true

collection_properties :: forall c i. (CoArbitrary i, Arbitrary c, Arbitrary i, Show i, Show c, Eq c, Eq i, Collection c i) => c -> [(Property, String)]Source

collection_properties returns the following properties:

collection
  foldr insert empty c == c
empty
  null empty
insert1
  a `elem` (insert a c)                                 -- insert puts the element in the collection
insert2
  a /= a' ==> (a' `elem` c <==  a' `elem` (insert a c)) -- insert does not insert other elements
insert3
  let c' = insert a c in x `elem` c && y `elem` c ==> x `elem` c' || y `elem` c' -- insert alters at most one element
filter
  (a `elem` filter f c) <==> ((a `elem` c) && f a)

map_properties :: forall m k v. (CoArbitrary v, CoArbitrary k, Arbitrary m, Arbitrary k, Arbitrary v, Show k, Show v, Show m, Eq m, Eq v, Map m k v) => m -> [(Property, String)]Source

map_properties returns the following properties:

alter
  lookup k (alter f k m) == f (lookup k m)
mapWithKey
  lookup k (mapWithKey f m) == fmap (f k) (lookup k m)
unionWith
  lookup k (unionWith f m1 m2) == case (lookup k m1, lookup k m2) of
     (Nothing,Nothing) -> Nothing
     (Just x, Nothing) -> Just x
     (Nothing,Just x)  -> Just x
     (Just x, Just y)  -> Just (f x y)
intersectionWith
  lookup k (intersectionWith f m1 m2) == case (lookup k m1, lookup k m2) of
     (Just x, Just y) -> Just (f x y)
     _ -> Nothing
differenceWith
  lookup k (differenceWith f m1 m2) == case (lookup k m1, lookup k m2) of
     (Just x, Nothing) -> Just x
     (Just x, Just y)  -> f x y
     (Nothing, _)      -> Nothing
isSubmapBy
  isSubmapBy f m1 m2 <==> differenceWith (\x y->if f x y then Nothing else Just v) m1 m2 == mempty
isProperSubmapBy
  isProperSubmapBy f m1 m2 <==> isSubmapBy f m1 m2 && m1 /= m2
insertWith
  insertWith f k a m == alter (\x -> Just $ case x of {Nothing->a;Just a' -> f a a'}) k m
fromFoldableWith
  fromFoldableWith f l == foldr (uncurry (insertWith f)) mempty l
delete
  delete k m == alter (const Nothing) k m
member
  member k m <==> isJust (lookup k m)
union
  union m1 m2 == unionWith const m1 m2
intersection
  intersection m1 m2 == intersectionWith const m1 m2 
difference
  difference m1 m2 == differenceWith (\_ _ -> Nothing) m1 m2
subset
  isSubset m1 m2 <==> isSubmapBy (\_ _ -> True) m1 m2
properSubset
  isProperSubset m1 m2 <==> isProperSubmapBy (\_ _ -> True) m1 m2
mempty
  lookup k mempty == Nothing
mappend
  mappend m1 m2 == union m1 m2
eq_lookup
  c1 == c2 ==> lookup x c1 == lookup x c2 -- should really be: c1 == c2 <==> forall x. lookup x c1 == lookup x c2

map_unfold_properties :: forall m k v. (Arbitrary m, Arbitrary k, Arbitrary v, Show k, Show v, Show m, Eq m, Eq v, Eq k, Map m k v, Collection m (k, v)) => m -> [(Property, String)]Source

map_unfold_properties returns the following properties:

mempty
  mempty == empty
insert
  insert (k,v) m == insertWith (\x _ -> x) k v m

set_unfold_properties :: forall m k. (Arbitrary m, Arbitrary k, Show k, Show m, Eq m, Eq k, Map m k (), Unfoldable m k) => m -> [(Property, String)]Source

set_unfold_properties returns the following properties:

mempty
  mempty == empty
insert
  insert k m == insertWith (\x _->x) k () m

map_fold_properties :: forall m k v. (CoArbitrary v, Arbitrary m, Arbitrary k, Arbitrary v, Show k, Show v, Show m, Eq m, Eq v, Eq k, Map m k v, Collection m (k, v)) => m -> [(Property, String)]Source

map_fold_properties returns the following properties:

foldable
  maybeToList (lookup k m) == map snd (List.filter ((== k) . fst) (toList m))
size
  sizeExcept (alter f k m) == sizeExcept m
    where sizeExcept m = size m - maybe 0 (const 1) (lookup k m)

set_fold_properties :: forall m k. (Arbitrary m, Arbitrary k, Show k, Show m, Eq m, Eq k, Map m k (), Foldable m k) => m -> [(Property, String)]Source

set_fold_properties returns the following properties:

foldable
  maybeToList (lookup k m) == map (const ()) (List.filter (== k) (toList m))
size
  sizeExcept (alter f k m) == sizeExcept m
    where sizeExcept m = size m - maybe 0 (const 1) (lookup k m)

indexed_map_properties :: forall m k v. (Arbitrary m, Arbitrary k, Arbitrary v, Show k, Show v, Show m, Eq m, Eq v, Map m k v, Indexed m k v) => m -> [(Property, String)]Source

indexed_map_properties returns the following properties:

domain
  k `inDomain` m <==> k `member` m
index
  case lookup k m of {Just x -> x == index k m; _ -> True}

sequence_properties :: forall s a. (Arbitrary s, Arbitrary a, Show s, Show a, Eq s, Eq a, Sequence s a) => s -> [(Property, String)]Source

sequence_properties returns the following properties:

fold0
  foldMap f empty == mempty
fold1
  foldMap f (x <| s) == f x `mappend` foldMap f s
fold2
  foldMap f (s |> x) == foldMap f s `mappend` f x
fold3
  foldMap f (s >< t) == foldMap f s `mappend` foldMap f t
front0
  front empty == Nothing
front1
  front (x <| s) == Just (x,s)
front2
  front (s |> x) == case front s of {Nothing -> Just (x, empty); Just (x',s') -> Just (x', s' |> x)}
front3
  front (s >< t) == case front s of {Nothing -> front t;         Just (x',s') -> Just (x', s' >< t)}
back0
  back empty == Nothing
back1
  back (s |> x) == Just (s,x)
back2
  back (x <| s) == case back s of {Nothing -> Just (empty, x); Just (s',x') -> Just (x <| s', x')}
back3
  back (t >< s) == case back s of {Nothing -> back t;          Just (s',x') -> Just (t >< s', x')}
drop1
          drop 0     s == s
drop2
  n>0 ==> drop (n+1) s == case front (drop n s) of Nothing -> empty; Just (_,s') -> s'
take1
          take 0     s == empty
take2
  n>0 ==> take (n+1) s == case front s of Nothing -> empty; Just (x,s') -> x <| take n s'
reverse
  foldMap f (reverse s) == getDual (foldMap (Dual . f) s)
mempty
  mempty == empty
eq_fold
  s1 == s2 ==> foldMap f s1 == foldMap f s2

indexed_properties :: forall m k v. (CoArbitrary v, Arbitrary m, Arbitrary k, Arbitrary v, Show k, Show v, Show m, Eq m, Eq v, Indexed m k v) => m -> [(Property, String)]Source

indexed_properties returns the following properties:

adjust
  k `inDomain` m ==> index k (adjust f k m) == f (index k m)

indexed_sequence_properties :: forall s a. (Arbitrary s, Arbitrary a, Show s, Show a, Eq s, Eq a, Sequence s a, Indexed s Int a) => s -> [(Property, String)]Source

indexed_sequence_properties returns the following properties:

domain
  k `inDomain` s <==> k >= 0 && k < size s
left1
  k `inDomain` s ==> index (k+1)      (x <| s) == index k s
left2
                       index 0          (x <| s) == x
right1
  k `inDomain` s ==> index k          (s |> x) == index k s
right2
                     index (size s)   (s |> x) == x
append1
  k `inDomain` t ==> index (k+size s) (s >< t) == index k t
append2
  k `inDomain` s ==> index k          (s >< t) == index k s