Haskell Hierarchical Libraries (collections package)ContentsIndex
Data.Collections.Properties
PortabilityMPTC, FD, undecidable instances
Stabilityexperimental
Maintainerjeanphilippe.bernardy; google mail.
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 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.

For convenience, this module provides an instance of Arbitrary (Maybe a).

Synopsis
foldable_properties :: forall c a . (Arbitrary c, Arbitrary a, Show a, Show c, Eq c, Eq a, Foldable c a) => c -> [(Property, String)]
collection_properties :: forall c i o . (Arbitrary c, Arbitrary i, Arbitrary o, Show i, Show o, Show c, Eq c, Eq o, Ord i, Collection c i o) => c -> [(Property, String)]
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) => m -> [(Property, String)]
map_coll_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) (k, v)) => m -> [(Property, String)]
set_coll_properties :: forall m k . (Arbitrary m, Arbitrary k, Show k, Show m, Eq m, Eq k, Map m k (), Collection m k k) => m -> [(Property, String)]
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)]
sequence_properties :: forall s a . (Arbitrary s, Arbitrary a, Show s, Show a, Eq s, Eq a, Sequence s a) => s -> [(Property, String)]
indexed_properties :: forall m k v . (Arbitrary m, Arbitrary k, Arbitrary v, Show k, Show v, Show m, Eq m, Eq v, Indexed m k v) => m -> [(Property, String)]
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)]
Documentation
foldable_properties :: forall c a . (Arbitrary c, Arbitrary a, Show a, Show c, Eq c, Eq a, Foldable c a) => c -> [(Property, String)]

foldable_properties returns the following properties:

size
  size c == foldr (const (+1)) 0 c
null
  null c <==> all (const False) c
collection_properties :: forall c i o . (Arbitrary c, Arbitrary i, Arbitrary o, Show i, Show o, Show c, Eq c, Eq o, Ord i, Collection c i o) => c -> [(Property, String)]

collection_properties returns the following properties:

null_empty
  null empty
size_empty
  size empty == 0
singleton1
  size (singleton a) == 1
singleton2
  singleton a == insert a empty
isSingleton
  isSingleton (singleton a)
insert1
  observe a `elem` (insert a c)
insert2
  observe a /= a' ==> (a' `elem` c <==> a' `elem` (insert a c))
insertMany
  insertMany l c == Foldable.foldr insert c l
insertManySorted
  insertManySorted l c == Foldable.foldr insert c l
     where l = List.sort l0
filter1
  all f (filter f c)
filter2
  foldr (:) [] (filter p c) == foldr comb [] c
     where comb a = if p a then (:) a else id
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) => m -> [(Property, String)]

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
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 (\x y -> Nothing) m1 m2
subset
  isSubset m1 m2 <==> isSubmapBy (\x y -> True) m1 m2
mempty
  lookup k mempty == Nothing
mappend
  mappend m1 m2 == union m1 m2
map_coll_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) (k, v)) => m -> [(Property, String)]

map_coll_properties returns the following properties:

mempty
  mempty == empty
insert
  insert (k,v) m == insertWith (\x _ -> x) k v m
foldable
  case lookup k m of 
     Nothing -> all ((/= k) . fst) (toList m)
     Just v' -> count ((== k) . fst) (toList m) == 1
size
  sizeExcept (alter f k m) == sizeExcept m
    where sizeExcept m = size m - maybe 0 (const 1) (lookup k m)
set_coll_properties :: forall m k . (Arbitrary m, Arbitrary k, Show k, Show m, Eq m, Eq k, Map m k (), Collection m k k) => m -> [(Property, String)]

set_coll_properties returns the following properties:

mempty
  mempty == empty
insert
  insert k m == insertWith (\x _->x) k () m
foldable1
  member k m <==> any (== k) m
foldable2
  member k m ==>  count (== k) m == 1
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)]

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)]

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
indexed_properties :: forall m k v . (Arbitrary m, Arbitrary k, Arbitrary v, Show k, Show v, Show m, Eq m, Eq v, Indexed m k v) => m -> [(Property, String)]

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)]

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
Produced by Haddock version 0.7