From 3c71853163bbc8f57b3aaf0a22d1505951641158 Mon Sep 17 00:00:00 2001 From: Recursion Ninja Date: Fri, 11 Jul 2025 15:37:19 -0400 Subject: [PATCH] Adding type-class law properties for data-types exported from Database.LSMTree --- lsm-tree.cabal | 2 + test/Main.hs | 2 + test/Test/Database/LSMTree.hs | 216 +++++- test/Test/Database/LSMTree/Internal/Config.hs | 199 +++++ test/Test/Util/TypeClassLaws.hs | 681 ++++++++++++++++++ 5 files changed, 1091 insertions(+), 9 deletions(-) create mode 100644 test/Test/Database/LSMTree/Internal/Config.hs create mode 100644 test/Test/Util/TypeClassLaws.hs diff --git a/lsm-tree.cabal b/lsm-tree.cabal index bd3b3b68f..b34979aee 100644 --- a/lsm-tree.cabal +++ b/lsm-tree.cabal @@ -689,6 +689,7 @@ test-suite lsm-tree-test Test.Database.LSMTree.Internal.BlobFile.FS Test.Database.LSMTree.Internal.BloomFilter Test.Database.LSMTree.Internal.Chunk + Test.Database.LSMTree.Internal.Config Test.Database.LSMTree.Internal.CRC32C Test.Database.LSMTree.Internal.Entry Test.Database.LSMTree.Internal.Index.Compact @@ -734,6 +735,7 @@ test-suite lsm-tree-test Test.Util.QC Test.Util.QLS Test.Util.RawPage + Test.Util.TypeClassLaws Test.Util.TypeFamilyWrappers build-depends: diff --git a/test/Main.hs b/test/Main.hs index 6369428a1..21f54b384 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -12,6 +12,7 @@ import qualified Test.Database.LSMTree.Internal.Arena import qualified Test.Database.LSMTree.Internal.BlobFile.FS import qualified Test.Database.LSMTree.Internal.BloomFilter import qualified Test.Database.LSMTree.Internal.Chunk +import qualified Test.Database.LSMTree.Internal.Config import qualified Test.Database.LSMTree.Internal.CRC32C import qualified Test.Database.LSMTree.Internal.Entry import qualified Test.Database.LSMTree.Internal.Index.Compact @@ -61,6 +62,7 @@ main = do , Test.Database.LSMTree.Internal.BlobFile.FS.tests , Test.Database.LSMTree.Internal.BloomFilter.tests , Test.Database.LSMTree.Internal.Chunk.tests + , Test.Database.LSMTree.Internal.Config.tests , Test.Database.LSMTree.Internal.CRC32C.tests , Test.Database.LSMTree.Internal.Entry.tests , Test.Database.LSMTree.Internal.Index.Compact.tests diff --git a/test/Test/Database/LSMTree.hs b/test/Test/Database/LSMTree.hs index f382a4ddf..ced073d90 100644 --- a/test/Test/Database/LSMTree.hs +++ b/test/Test/Database/LSMTree.hs @@ -1,14 +1,23 @@ -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} module Test.Database.LSMTree (tests) where import Control.Exception import Control.Tracer +import Data.Foldable import Data.Function (on) import Data.IORef -import Data.Monoid +import Data.Monoid (Sum (..)) +import Data.String (fromString) import Data.Typeable (Typeable) import qualified Data.Vector as V import qualified Data.Vector.Algorithms as VA @@ -19,15 +28,17 @@ import Database.LSMTree.Extras (showRangesOf) import Database.LSMTree.Extras.Generators () import qualified System.FS.API as FS import qualified System.FS.BlockIO.API as FS -import Test.QuickCheck -import Test.Tasty +import Test.Database.LSMTree.Internal.Config () +import Test.Tasty (TestTree, testGroup) import Test.Tasty.QuickCheck import Test.Util.FS +import Test.Util.TypeClassLaws + tests :: TestTree -tests = testGroup "Test.Database.LSMTree" [ - testGroup "Session" [ - -- openSession +tests = testGroup "Test.Database.LSMTree" + [ testGroup "Session" + [ -- openSession testProperty "prop_openSession_newSession" prop_openSession_newSession , testProperty "prop_openSession_restoreSession" prop_openSession_restoreSession -- happy path @@ -41,6 +52,16 @@ tests = testGroup "Test.Database.LSMTree" [ -- salt , testProperty "prop_goodAndBadSessionSalt" prop_goodAndBadSessionSalt ] + , laws_Entry + , laws_LookupResult + , laws_Range + , laws_RawBytes + , laws_SnapshotName + , laws_SnapshotLabel + , laws_TableConfigOverride + , laws_UnionCredits + , laws_UnionDebt + , laws_Update ] {------------------------------------------------------------------------------- @@ -312,3 +333,180 @@ prop_goodAndBadSessionSalt (Positive (Small bufferSize)) ins = conf = defaultTableConfig { confWriteBufferAlloc = AllocNumEntries bufferSize } + +{------------------------------------------------------------------------------- + Type-class Laws +-------------------------------------------------------------------------------} + +-- | +-- This alias exists for brevity in type signatures +type W = Word + +-- Entry + +instance (Arbitrary k, Arbitrary v, Arbitrary b) => Arbitrary (Entry k v b) where + + arbitrary = oneof + [ Entry <$> arbitrary <*> arbitrary + , EntryWithBlob <$> arbitrary <*> arbitrary <*> arbitrary + ] + + shrink (Entry k v) = [ Entry k' v' | k' <- shrink k, v' <- shrink v ] + shrink (EntryWithBlob k v b) = + [ EntryWithBlob k' v' b' | k' <- shrink k, v' <- shrink v, b' <- shrink b ] + +laws_Entry :: TestTree +laws_Entry = testGroup "Entry" + -- Basic control structures + [ functorLaws @(Entry W W) + , bifunctorLaws @(Entry W) + , foldableLaws @(Entry W W) + , traversableLaws @(Entry W W) + -- Data structures + , equalityLaws @(Entry W W W) + , normalFormDataLaws @(Entry W W W) + , showProperties @(Entry W W W) + ] + +-- LookupResult + +instance (Arbitrary v, Arbitrary b) => Arbitrary (LookupResult v b) where + + arbitrary = oneof + [ pure NotFound + , Found <$> arbitrary + , FoundWithBlob <$> arbitrary <*> arbitrary + ] + + shrink NotFound = [] + shrink (Found v) = NotFound : [Found v' | v' <- shrink v] + shrink (FoundWithBlob v b) = fold + [ [NotFound, Found v] + , [FoundWithBlob v' b | v' <- shrink v] + , [FoundWithBlob v b' | b' <- shrink b] + ] + +laws_LookupResult :: TestTree +laws_LookupResult = testGroup "LookupResult" + -- Basic control structures + [ functorLaws @(LookupResult W) + , bifunctorLaws @(LookupResult) + , foldableLaws @(LookupResult W) + , traversableLaws @(LookupResult W) + -- Data structures + , equalityLaws @(LookupResult W W) + , normalFormDataLaws @(LookupResult W W) + , showProperties @(LookupResult W W) + ] + +-- Range + +laws_Range :: TestTree +laws_Range = testGroup "Range" + [ functorLaws @(Range) + , equalityLaws @(Range W) + , normalFormDataLaws @(Range W) + , showProperties @(Range W) + ] + +-- RawBytes + +laws_RawBytes :: TestTree +laws_RawBytes = testGroup "RawBytes" + [ equalityLaws @(RawBytes) + , orderingLaws @(RawBytes) + , semigroupLaws @(RawBytes) + , monoidLaws @(RawBytes) + , normalFormDataLaws @(RawBytes) + , showProperties @(RawBytes) + ] + +-- SnapshotName + +instance Arbitrary SnapshotName where + + arbitrary = toSnapshotName . getPrintableString <$> + (arbitrary `suchThat` (isValidSnapshotName . getPrintableString)) + + shrink = fmap toSnapshotName . filter isValidSnapshotName . + fmap getPrintableString . shrink . PrintableString . show + +laws_SnapshotName :: TestTree +laws_SnapshotName = testGroup "SnapshotName" + [ equalityLaws @(SnapshotName) + , orderingLaws @(SnapshotName) + , showProperties @(SnapshotName) + ] + +-- SnapshotLabel + +instance Arbitrary SnapshotLabel where + + arbitrary = fromString . getPrintableString <$> + (arbitrary `suchThat` (isValidSnapshotName . getPrintableString)) + + shrink = fmap fromString. filter isValidSnapshotName . + fmap getPrintableString . shrink . PrintableString . show + +laws_SnapshotLabel :: TestTree +laws_SnapshotLabel = testGroup "SnapshotLabel" + [ equalityLaws @(SnapshotLabel) + , normalFormDataLaws @(SnapshotLabel) + , showProperties @(SnapshotLabel) + ] + +-- TableConfigOverride + +instance Arbitrary TableConfigOverride where + + arbitrary = TableConfigOverride <$> arbitrary <*> arbitrary + + shrink (TableConfigOverride x y) = + [ TableConfigOverride x' y' | x' <- shrink x, y' <- shrink y ] + +laws_TableConfigOverride :: TestTree +laws_TableConfigOverride = testGroup "TableConfigOverride" + [ equalityLaws @(SnapshotLabel) + , showProperties @(SnapshotLabel) + ] + +-- UnionCredits + +instance Arbitrary UnionCredits where + + arbitrary = UnionCredits . getNonNegative <$> arbitrary + + shrink (UnionCredits x) = UnionCredits . getNonNegative <$> shrink (NonNegative x) + +laws_UnionCredits :: TestTree +laws_UnionCredits = testGroup "UnionCredits" + [ equalityLaws @(UnionCredits) + , orderingLaws @(UnionCredits) + , numLaws @(UnionCredits) + , showProperties @(UnionCredits) + ] + +-- UnionDebt + +instance Arbitrary UnionDebt where + + arbitrary = UnionDebt . getNonNegative <$> arbitrary + + shrink (UnionDebt x) = UnionDebt . getNonNegative <$> shrink (NonNegative x) + +laws_UnionDebt :: TestTree +laws_UnionDebt = testGroup "UnionDebt" + [ equalityLaws @(UnionDebt) + , orderingLaws @(UnionDebt) + , numLaws @(UnionDebt) + , showProperties @(UnionDebt) + ] + +-- Update + +laws_Update :: TestTree +laws_Update = testGroup "Update" + [ equalityLaws @(Update W W) + , normalFormDataLaws @(Update W W) + , showProperties @(Update W W) + ] diff --git a/test/Test/Database/LSMTree/Internal/Config.hs b/test/Test/Database/LSMTree/Internal/Config.hs new file mode 100644 index 000000000..0b0411370 --- /dev/null +++ b/test/Test/Database/LSMTree/Internal/Config.hs @@ -0,0 +1,199 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + +module Test.Database.LSMTree.Internal.Config (tests) where + +import Database.LSMTree.Internal.Config +import Test.QuickCheck.Modifiers +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck +import Test.Util.TypeClassLaws + + +tests :: TestTree +tests = testGroup "Test.Database.LSMTree.Internal.Config" + [ laws_BloomFilterAlloc + , laws_DiskCachePolicy + , laws_FencePointerIndexType + , laws_LevelNo + , laws_MergeBatchSize + , laws_MergePolicy + , laws_MergeSchedule + , laws_SizeRatio + , laws_TableConfig + , laws_WriteBufferAlloc + ] + +laws_BloomFilterAlloc :: TestTree +laws_BloomFilterAlloc = testGroup "BloomFilterAlloc" + [ equalityLaws @(BloomFilterAlloc) + , normalFormDataLaws @(BloomFilterAlloc) + , showProperties @(BloomFilterAlloc) + ] + +laws_DiskCachePolicy :: TestTree +laws_DiskCachePolicy = testGroup "DiskCachePolicy" + [ equalityLaws @(DiskCachePolicy) + , normalFormDataLaws @(DiskCachePolicy) + , showProperties @(DiskCachePolicy) + ] + +laws_FencePointerIndexType :: TestTree +laws_FencePointerIndexType = testGroup "FencePointerIndexType" + [ equalityLaws @(FencePointerIndexType) + , normalFormDataLaws @(FencePointerIndexType) + , showProperties @(FencePointerIndexType) + ] + +laws_LevelNo :: TestTree +laws_LevelNo = testGroup "LevelNo" + [ enumLaws @(LevelNo) + , equalityLaws @(LevelNo) + , orderingLaws @(LevelNo) + , normalFormDataLaws @(LevelNo) + , showProperties @(LevelNo) + ] + +laws_MergeBatchSize :: TestTree +laws_MergeBatchSize = testGroup "MergeBatchSize" + [ equalityLaws @(MergeBatchSize) + , orderingLaws @(MergeBatchSize) + , normalFormDataLaws @(MergeBatchSize) + , showProperties @(MergeBatchSize) + ] + +laws_MergePolicy :: TestTree +laws_MergePolicy = testGroup "MergePolicy" + [ normalFormDataLaws @(MergePolicy) + , showProperties @(MergePolicy) + ] + +laws_MergeSchedule :: TestTree +laws_MergeSchedule = testGroup "MergeSchedule" + [ equalityLaws @(MergeSchedule) + , normalFormDataLaws @(MergeSchedule) + , showProperties @(MergeSchedule) + ] + +laws_SizeRatio :: TestTree +laws_SizeRatio = testGroup "SizeRatio" + [ normalFormDataLaws @(SizeRatio) + , showProperties @(SizeRatio) + ] + +laws_TableConfig :: TestTree +laws_TableConfig = testGroup "TableConfig" + [ equalityLaws @(TableConfig) + , normalFormDataLaws @(TableConfig) + , showProperties @(TableConfig) + ] + +laws_WriteBufferAlloc :: TestTree +laws_WriteBufferAlloc = testGroup "WriteBufferAlloc" + [ equalityLaws @(WriteBufferAlloc) + , normalFormDataLaws @(WriteBufferAlloc) + , showProperties @(WriteBufferAlloc) + ] + +isValidBloomFilterFixedValue :: Double -> Bool +isValidBloomFilterFixedValue x = 2 <= x && x <= 24 + +isValidBloomFilterRequestValue :: Double -> Bool +isValidBloomFilterRequestValue x = 0 < x && x < 1 + +instance Arbitrary BloomFilterAlloc where + + arbitrary = oneof + [ fmap AllocFixed $ + arbitrary `suchThat` isValidBloomFilterFixedValue + , fmap AllocRequestFPR $ + arbitrary `suchThat` isValidBloomFilterRequestValue + ] + + shrink (AllocFixed x) = fmap AllocFixed . + filter isValidBloomFilterFixedValue $ shrink x + shrink (AllocRequestFPR x) = fmap AllocRequestFPR . + filter isValidBloomFilterRequestValue $ shrink x + +instance Arbitrary DiskCachePolicy where + + arbitrary = oneof + [ pure DiskCacheAll + , pure DiskCacheNone + , DiskCacheLevelOneTo . getPositive <$> arbitrary + ] + + shrink (DiskCacheLevelOneTo x) = + [ DiskCacheLevelOneTo x' | Positive x' <- shrink $ Positive x ] + shrink _ = [] + +instance Arbitrary FencePointerIndexType where + + arbitrary = oneof $ pure <$> [ OrdinaryIndex, CompactIndex ] + + shrink _ = [] + +instance Arbitrary LevelNo where + + arbitrary = LevelNo . getNonNegative <$> arbitrary + + shrink (LevelNo x) = + LevelNo . getNonNegative <$> shrink (NonNegative x) + +instance Arbitrary MergeBatchSize where + + arbitrary = MergeBatchSize . getPositive <$> arbitrary + + shrink (MergeBatchSize x) = + MergeBatchSize . getPositive <$> shrink (Positive x) + +instance Arbitrary MergePolicy where + + arbitrary = pure LazyLevelling + + shrink = const [] + +instance Arbitrary MergeSchedule where + + arbitrary = oneof $ pure <$> [ OneShot, Incremental ] + + shrink = const [] + +instance Arbitrary SizeRatio where + + arbitrary = pure Four + + shrink = const [] + +instance Arbitrary TableConfig where + + arbitrary = TableConfig + <$> arbitrary + <*> arbitrary + <*> arbitrary + <*> arbitrary + <*> arbitrary + <*> arbitrary + <*> arbitrary + <*> arbitrary + + shrink (TableConfig a b c d e f g h) = + [ TableConfig a' b' c' d' e' f' g' h' + | (a',b',c',d',e',f',g',h') <- shrink (a,b,c,d,e,f,g,h) + ] + +instance Arbitrary WriteBufferAlloc where + + arbitrary = AllocNumEntries . getPositive <$> arbitrary + + shrink (AllocNumEntries x) = + AllocNumEntries . getPositive <$> shrink (Positive x) + diff --git a/test/Test/Util/TypeClassLaws.hs b/test/Test/Util/TypeClassLaws.hs new file mode 100644 index 000000000..99b2fce85 --- /dev/null +++ b/test/Test/Util/TypeClassLaws.hs @@ -0,0 +1,681 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} + +-- Testing type-class laws necissarily requires +-- definitions which HLint finds superfluous +{- HLINT ignore "Use first" -} +{- HLINT ignore "Use second" -} +{- HLINT ignore "Redundant bimap" -} +{- HLINT ignore "Use bimap" -} +{- HLINT ignore "Monad law, right identity" -} +{- HLINT ignore "Monad law, left identity" -} +{- HLINT ignore "Use >=>" -} +{- HLINT ignore "Use =<<" -} +{- HLINT ignore "Monoid law, left identity" -} +{- HLINT ignore "Monoid law, right identity" -} +{- HLINT ignore "Redundant toList" -} +{- HLINT ignore "Use null" -} + +-- | +-- Exports generalized, property-based type-class laws for usage in other +-- test-suite modules. +module Test.Util.TypeClassLaws + ( -- * Type Class Laws + -- ** Basic control structures + functorLaws + , bifunctorLaws + , applicativeLaws + , monadLaws + , monadFailLaws + -- ** Refined control structures + , altLaws + , applyLaws + , bindLaws + -- ** Ordered container structures + , foldableLaws + , traversableLaws + -- ** Numeric-like + , boundedLaws + , enumLaws + , numLaws + -- ** Group-like + , semigroupLaws + , monoidLaws + -- ** Orderable + , equalityLaws + , orderingLaws + -- ** Other + , normalFormDataLaws + , showProperties + ) where + +import Control.Applicative (Alternative (..)) +import Control.DeepSeq +import Control.Monad (join) +import Data.Bifunctor +import Data.Foldable +import Data.Functor.Compose +import Data.Functor.Identity +import Data.Semigroup +import Test.QuickCheck.Function +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck hiding ((=/=)) + +-- | +-- This alias exists for brevity in type signatures +type W = Word + +functorLaws + :: forall f. + ( Arbitrary (f W) + , Eq (f W) + , Functor f + , Show (f W) + ) + => TestTree +functorLaws = testGroup "Functor Laws" + [ testLaw functorIdentity "Identity" "fmap id === id" + , testLaw functorComposition "Composition" "fmap (f . g) === fmap f . fmap g" + ] + where + functorIdentity :: f W -> Property + functorIdentity x = + fmap id x === x + + functorComposition :: f W -> Fun W W -> Fun W W -> Property + functorComposition x (apply -> f) (apply -> g) = + fmap (g . f) x === (fmap g . fmap f $ x) + +bifunctorLaws + :: forall f. + ( Arbitrary (f W W) + , Eq (f W W) + , Bifunctor f + , Show (f W W) + ) + => TestTree +bifunctorLaws = testGroup "Bifunctor Laws" + [ testLaw bifunctorIdentity "Identity" "bimap id id === id" + , testLaw bifunctorComposition "Composition" "bimap f g === first f . second g" + ] + where + bifunctorIdentity :: f W W -> Property + bifunctorIdentity x = + bimap id id x === x + + bifunctorComposition :: f W W -> Fun W W -> Fun W W -> Property + bifunctorComposition x (apply -> f) (apply -> g) = + bimap f g x === (first f . second g) x + +applicativeLaws + :: forall f. + ( Applicative f + , Arbitrary (f W) + , Arbitrary (f (Fun W W)) + , Eq (f W) + , Show (f W) + , Show (f (Fun W W)) + ) + => TestTree +applicativeLaws = testGroup "Applicative Laws" + [ testLaw applicativeIdentity "Identity" "pure id <*> v === v" + , testLaw applicativeComposition "Composition" "pure (.) <*> u <*> v <*> w === u <*> (v <*> w)" + , testLaw applicativeHomomorphism "Homomorphism" "pure f <*> pure x = pure (f x)" + , testLaw applicativeInterchange "Interchange" "u <*> pure y === pure ($ y) <*> u" + ] + where + applicativeIdentity :: f W -> Property + applicativeIdentity x = + (pure id <*> x) === x + + applicativeComposition :: f (Fun W W) -> f (Fun W W) -> f W -> Property + applicativeComposition (fmap apply -> x) (fmap apply -> y) z = + (pure (.) <*> x <*> y <*> z) === (x <*> (y <*> z)) + + applicativeInterchange :: f (Fun W W) -> W -> Property + applicativeInterchange (fmap apply -> x) y = + (x <*> pure y) === (pure ($ y) <*> x) + + applicativeHomomorphism :: Fun W W -> W -> Property + applicativeHomomorphism (apply -> f) x = + (pure f <*> pure x) === (pure (f x) :: f W) + +applyLaws + :: forall f. + ( Applicative f + , Arbitrary (f W) + , Arbitrary (f (Fun W W)) + , Eq (f W) + , Eq (f (f W)) + , Show (f W) + , Show (f (f W)) + , Show (f (Fun W W)) + ) + => TestTree +applyLaws = testGroup "Apply Laws" + [ testLaw composition "Composition" "(.) <$> u <*> v <*> w = u <*> (v <*> w)" + , testLaw leftInterchange "Left Interchange" "x <*> (f <$> y) = (. f) <$> x <*> y" + , testLaw rightInterchange "Right Interchange" "f <$> (x <*> y) = (f .) <$> x <*> y" + , testLaw leftNullification "Left Nullification" "(mf <$> m) *> (nf <$> n) = nf <$> (m *> n)" + , testLaw rightNullification "Right Nullification" "(mf <$> m) <* (nf <$> n) = mf <$> (m <* n)" + ] + where + composition :: f (Fun W W) -> f (Fun W W) -> f W -> Property + composition (fmap apply -> x) (fmap apply -> y) z = + ((.) <$> x <*> y <*> z) === (x <*> (y <*> z)) + + leftInterchange :: Fun W W -> f (Fun W W) -> f W -> Property + leftInterchange (apply -> f) (fmap apply -> x) y = + (x <*> (f <$> y)) === ((. f) <$> x <*> y) + + rightInterchange :: Fun W (f W) -> f (Fun W W) -> f W -> Property + rightInterchange (apply -> f) (fmap apply -> x) y = + (f <$> (x <*> y)) === ((f .) <$> x <*> y) + + leftNullification :: Fun W W -> Fun W W -> f W -> f W -> Property + leftNullification (apply -> f) (apply -> g) m n = + ((f <$> m) *> (g <$> n)) === (g <$> (m *> n)) + + rightNullification :: Fun W W -> Fun W W -> f W -> f W -> Property + rightNullification (apply -> f) (apply -> g) m n = + ((f <$> m) <* (g <$> n)) === (f <$> (m <* n)) + +monadLaws + :: forall m. + ( Arbitrary (m W) + , Eq (m W) + , Monad m + , Show (m W) + ) + => TestTree +monadLaws = testGroup "Monad Laws" + [ testLaw monadLeftIdentity "Left Identity" "return a >>= k === k a" + , testLaw monadRightIdentity "Right Identity" "m >>= return === m" + , testLaw monadAssociativity "Associativity" "m >>= (x -> k x >>= h) === (m >>= k) >>= h" + ] + where + monadRightIdentity :: m W -> Property + monadRightIdentity x = + (x >>= pure) === x + + monadLeftIdentity :: W -> Fun W (m W) -> Property + monadLeftIdentity x (apply -> f) = + (pure x >>= f) === f x + + monadAssociativity :: m W -> Fun W (m W) -> Fun W (m W) -> Property + monadAssociativity x (apply -> f) (apply -> g) = + ((x >>= f) >>= g) === (x >>= (\x' -> f x' >>= g)) + +monadFailLaws + :: forall m. + ( Arbitrary (m W) + , Eq (m W) + , MonadFail m + , Show (m W) + ) + => TestTree +monadFailLaws = testGroup "MonadFail Laws" + [ testLaw leftNullification "Left Nullification" "fail s >>= f === fail s" + ] + where + leftNullification :: Fun W (m W) -> String -> Property + leftNullification (apply -> f) s = + (fail s >>= f) === (fail s :: m W) + +altLaws + :: forall f. + ( Alternative f + , Arbitrary (f W) + , Eq (f W) + , Show (f W) + ) + => TestTree +altLaws = testGroup "Alt Laws" + [ testLaw altAssociativity "Associativity" "x <|> (y <|> z) === (x <|> y) <|> z" + , testLaw altLeftCatch "Left Catch" "pure x <|> y = pure x" + , testLaw altLeftDistributivity1 "Left Distributivity I" "f <$> (x <|> y) === (f <$> x) <|> (f <$> y)" +-- These laws do not hold for our 'Either-like' data type. +-- This is okay (apparently) since the 'Left Catch' law holds. +-- , "Left Distributivity II" "(x <|> y) <*> z === (x <*> z) <|> (y <*> z)" +-- , "Right Distributivity" "(m <|> n) >>- f === (m >>- f) <|> (m >>- f)" + ] + where + altAssociativity :: f W -> f W -> f W -> Property + altAssociativity x y z = + ((x <|> y) <|> z) === (x <|> (y <|> z)) + + altLeftCatch :: W -> f W -> Property + altLeftCatch x y = + (pure x <|> y) === pure x + + altLeftDistributivity1 :: Fun W W -> f W -> f W -> Property + altLeftDistributivity1 (apply -> f) x y = + (f <$> (x <|> y)) === ((f <$> x) <|> (f <$> y)) + +bindLaws + :: forall m. + ( Arbitrary (m W) + , Arbitrary (m (m W)) + , Arbitrary (m (m (m W))) + , Arbitrary (m (Fun W W)) + , Monad m + , Eq (m W) + , Show (m W) + , Show (m (m W)) + , Show (m (m (m W))) + , Show (m (Fun W W)) + ) + => TestTree +bindLaws = testGroup "Bind Laws" + [ testLaw defJoin "Definition of join" "join === (>>= id)" + , testLaw defBind "Definition of bind" "m >>= f === join (fmap f m)" + , testLaw defApply "Definition of apply" "f <*> x === f >>= (<$> x)" + , testLaw associativity1 "Associativity I" "(m >>= f) >>= g === m >>= (\\x -> f x >>= g)" + , testLaw associativity2 "Associativity II" "join . join === join . mmap join" + ] + where + defJoin :: m (m W) -> Property + defJoin x = + join x === (>>= id) x + + defBind :: Fun W (m W) -> m W -> Property + defBind (apply -> f) x = + (x >>= f) === join (fmap f x) + + defApply :: m (Fun W W) -> m W -> Property + defApply (fmap apply -> f) x = + (f <*> x) === (f >>= (<$> x)) + + associativity1 :: Fun W (m W) -> Fun W (m W) -> m W -> Property + associativity1 (apply -> f) (apply -> g) x = + ((x >>= f) >>= g) === (x >>= (\a -> f a >>= g)) + + associativity2 :: m (m (m W)) -> Property + associativity2 x = + (join . join) x === (join . fmap join) x + +boundedLaws + :: forall a. + ( Arbitrary a + , Bounded a + , Enum a + , Eq a + , Show a + ) + => TestTree +boundedLaws = testGroup "Bounded Laws" + [ testLaw iso_succ "Isomorphism (succ)" "x /= maxBound ==> fromEnum (succ x) === fromEnum x + 1" + , testLaw iso_pred "Isomorphism (pred)" "x /= minBound ==> fromEnum (pred x) === fromEnum x - 1" + ] + where + iso_succ :: a -> Property + iso_succ x = + x /= maxBound ==> fromEnum (succ x) === fromEnum x + 1 + + iso_pred :: a -> Property + iso_pred x = + x /= minBound ==> fromEnum (pred x) === fromEnum x - 1 + +enumLaws + :: forall a. + ( Arbitrary a + , Enum a + , Eq a + , Show a + ) + => TestTree +enumLaws = testGroup "Enum Laws" + [ testLaw iso_id "Isomorphism (id)" "(toEnum . fromEnum) x === x" + , testLaw iso_int "Isomorphism (Int)" "(fromEnum . toEnum) x === x" + ] + where + iso_id :: a -> Property + iso_id x = + (toEnum . fromEnum) x === x + + iso_int :: Int -> Property + iso_int x = + (fromEnum . (toEnum :: Int -> a)) x === x + +numLaws + :: forall a. + ( Arbitrary a + , Eq a + , Num a + , Show a + ) + => TestTree +numLaws = testGroup "Num Laws" + [ testLaw associativity_plus "associativity (+)" "x + (y + z) === (x + y) + z" + , testLaw identity_L_plus "identity (L) (+)" "0 + x === x" + , testLaw identity_R_plus "identity (R) (+)" "x + 0 === x" + , testLaw associativity_times "associativity (*)" "x * (y * z) === (x * y) * z" + , testLaw identity_L_times "identity (L) (*)" "1 * x === x" + , testLaw identity_R_times "identity (R) (*)" "x * 1 === x" + ] + where + associativity_plus :: a -> a -> a -> Property + associativity_plus x y z = + x + (y + z) === (x + y) + z + + identity_L_plus :: a -> Property + identity_L_plus x = + 0 + x === x + + identity_R_plus :: a -> Property + identity_R_plus x = + x + 0 === x + + associativity_times :: a -> a -> a -> Property + associativity_times x y z = + x * (y * z) === (x * y) * z + + identity_L_times :: a -> Property + identity_L_times x = + 1 * x === x + + identity_R_times :: a -> Property + identity_R_times x = + x * 1 === x + +-- | Note: do not use this for data-types with a single inhabitant. +-- The preconditions of @x /= y@ will never be satisfied, +-- causing the tests to fail. +equalityLaws + :: forall a. + ( Arbitrary a + , Eq a + , Show a + ) + => TestTree +equalityLaws = testGroup "Equality Laws" + [ testLaw negation "Negation" "x /= y ==> not (x == y)" + , testLaw symmetry "Symmetry" "x /= y ==> y /= x" + , testLaw transitivity "Transitivity" "x == y && y == z ==> x == z" + , testLaw refexivity "Reflexivity" "x == x" + ] + where + negation :: a -> a -> Property + negation x y = + x /= y ==> not (x == y) + + symmetry :: a -> a -> Property + symmetry x y = + x /= y ==> y =/= x + + transitivity :: a -> a -> a -> Property + transitivity x y z = + not (x == y && y == z) .||. x == z + + refexivity :: a -> Property + refexivity x = + x === x + +normalFormDataLaws + :: forall a. + ( Arbitrary a + , NFData a + , Show a + ) + => TestTree +normalFormDataLaws = testGroup "NFData Laws" + [ testLaw finiteReduction "Finiteness" "rnf x =/= _|_" + ] + where + finiteReduction :: a -> Property + finiteReduction x = + rnf x === () + +orderingLaws + :: forall a. + ( Arbitrary a + , Ord a + , Show a + ) + => TestTree +orderingLaws = testGroup "Ordering Laws" + [ testLaw symmetry "Symmetry" "x >= y ==> y <= x" + , testLaw transitivity1 "Transitive I" "x < y && y < z ==> x < z" + , testLaw transitivity2 "Transitive II" "x > y && y > z ==> x > z" + ] + where + symmetry :: a -> a -> Bool + symmetry lhs rhs = + case (lhs `compare` rhs, rhs `compare` lhs) of + (EQ, EQ) -> True + (GT, LT) -> True + (LT, GT) -> True + _ -> False + + transitivity1 :: a -> a -> a -> Property + transitivity1 x y z = + (x < y && y < z) ==> x < z + + transitivity2 :: a -> a -> a -> Property + transitivity2 x y z = + (x > y && y > z) ==> x > z + +semigroupLaws + :: forall a. + ( Arbitrary a + , Eq a + , Semigroup a + , Show a + ) + => TestTree +semigroupLaws = testGroup "Semigroup Laws" + [ testLaw semigroupAssociativity "Associativity" "x <> (y <> z) === (x <> y) <> z" + ] + where + semigroupAssociativity :: a -> a -> a -> Property + semigroupAssociativity x y z = + (x <> (y <> z)) === ((x <> y) <> z) + +monoidLaws + :: forall a. + ( Arbitrary a + , Eq a + , Monoid a + , Show a + ) + => TestTree +monoidLaws = testGroup "Monoid Laws" + [ testLaw identity_L "identity left" "mempty <> x === x" + , testLaw identity_R "identity right" "x <> mempty === x" + ] + where + identity_L :: a -> Property + identity_L x = + mempty <> x === x + + identity_R :: a -> Property + identity_R x = + x <> mempty === x + +showProperties + :: forall a. + ( Arbitrary a + , Show a + ) + => TestTree +showProperties = testGroup "Show Laws" + [ testLaw finiteString "Finiteness" "rnf (show x) =/= _|_" + , testLaw nonNullString "Non-null" "not . null . show" + ] + where + finiteString :: a -> Property + finiteString x = + (rnf . show) x === () + + nonNullString :: a -> Bool + nonNullString = + not . null . show + +foldableLaws + :: forall f. + ( Arbitrary (f W) + , Foldable f + , Show (f W) + ) + => TestTree +foldableLaws = testGroup "Foldable Laws" + [ testLaw testFoldlFoldMap "Dual Endomorphism" + "foldl' f z t === appEndo (getDual (foldMap (Dual . Endo . flip f) t)) z" + , testLaw testFoldrFoldMap "Fold-map Endomorphism" + "foldr f z t === appEndo (foldMap (Endo . f) t ) z" + , testLaw testFoldr "Fold-right List Equivelency" + "foldr f z === foldr f z . toList" + , testLaw testFoldl "Fold-right List Equivelency" + "foldl' f z === foldl' f z . toList" + , testLaw testFoldr1 "Non-empty Fold-right List Equivelency" + "foldr1 f === foldr1 f . toList" + , testLaw testFoldl1 "Non-empty Fold-left List Equivelency" + "foldl1 f === foldl1 f . toList" + , testLaw testNull "Zero-length Nullability Implication" + "null === (0 ==) . length" + , testLaw testLength "Length List Equivelency" + "length === length . toList" + , testLaw testInclusionConsistency "Inclusion Consistency" + "elem e =/= notElem e" + , testLaw testMax "Max Fold-map Equivelency" + "maximum === getMax . foldMap Max" + , testLaw testMin "Min Fold-map Equivelency" + "minimum === getMin . foldMap Min" + , testLaw testSum "Sum Fold-map Equivelency" + "sum === getSum . foldMap Sum" + , testLaw testProduct "Product Fold-map Equivelency" + "product === getProduct . foldMap Product" + , testLaw testFirst "First Fold-map Equivelency" + "head . toList === getFirst . foldMap First" + , testLaw testLast "Last Fold-map Equivelency" + "last . toList === getLast . foldMap Last" + , testLaw testAll "All Fold-map Equivelency" + "all f === getAll . foldMap (All . f)" + , testLaw testAny "Any Fold-map Equivelency" + "any f === getAny . foldMap (Any . f)" + ] + where + testFoldrFoldMap :: Fun (W, W) W -> W -> f W -> Property + testFoldrFoldMap (applyFun2 -> f) z x = + foldr f z x === appEndo (foldMap (Endo . f) x) z + + testFoldlFoldMap :: Fun (W, W) W -> W -> f W -> Property + testFoldlFoldMap (applyFun2 -> f) z x = + foldl' f z x === appEndo (getDual (foldMap (Dual . Endo . flip f) x)) z + + testFoldr :: Fun (W, W) W -> W -> f W -> Property + testFoldr (applyFun2 -> f) z x = + foldr f z x === (foldr f z . toList) x + + testFoldl :: Fun (W, W) W -> W -> f W -> Property + testFoldl (applyFun2 -> f) z x = + foldl' f z x === (foldl' f z . toList) x + + testFoldr1 :: Fun (W, W) W -> f W -> Property + testFoldr1 (applyFun2 -> f) x = + (not . null) x ==> foldr1 f x === (foldr1 f . toList) x + + testFoldl1 :: Fun (W, W) W -> f W -> Property + testFoldl1 (applyFun2 -> f) x = + (not . null) x ==> foldl1 f x === (foldl1 f . toList) x + + testNull :: f W -> Property + testNull x = + null x === ((0 ==) . length) x + + testLength :: f W -> Property + testLength x = + length x === (length . toList) x + + testInclusionConsistency :: (W, f W) -> Property + testInclusionConsistency (e, x) = + elem e x =/= notElem e x + + testMax :: f W -> Property + testMax x = + (not . null) x ==> + maximum x === (getMax . foldMap Max) x + + testMin :: f W -> Property + testMin x = + (not . null) x ==> + minimum x === (getMin . foldMap Min) x + + testSum :: f W -> Property + testSum x = + sum x === (getSum . foldMap Sum) x + + testProduct :: f W -> Property + testProduct x = + product x === (getProduct . foldMap Product) x + + testFirst :: f W -> Property + testFirst x = + (not . null) x ==> + (Just . head . toList) x === (fmap getFirst . foldMap (Just . First)) x + + testLast :: f W -> Property + testLast x = + (not . null) x ==> + (Just . last . toList) x === (fmap getLast . foldMap (Just . Last)) x + + testAll :: Fun W Bool -> f W -> Property + testAll (apply -> f) x = + all f x === (getAll . foldMap (All . f)) x + + testAny :: Fun W Bool -> f W -> Property + testAny (apply -> f) x = + any f x === (getAny . foldMap (Any . f)) x + +traversableLaws + :: forall f. + ( Arbitrary (f W) + , Eq (f Bool) + , Eq (f W) + , Traversable f + , Show (f W) + , Show (f Bool) + ) + => TestTree +traversableLaws = testGroup "Traversable Laws" + [ testLaw naturality "Naturality" "t . traverse f === traverse (t . f)" + , testLaw identity "Identity" "traverse Identity === Identity" + , testLaw composition "Composition" "traverse (Compose . fmap g . f) === Compose . fmap (traverse g) . traverse f" + , testLaw equality "Definition Equality" "traverse === mapM" + ] + where + naturality :: Fun W [W] -> f W -> Property + naturality (apply -> f) x = + (headMay . traverse f) x === traverse (headMay . f) x + where + headMay [] = Nothing + headMay (a:_) = Just a + + identity :: f W -> Property + identity x = + traverse Identity x === Identity x + + composition :: Fun W (Either W Bool) -> Fun Bool (Maybe W) -> f W -> Property + composition (apply -> f) (apply -> g) x = + traverse (Compose . fmap g . f) x === (Compose . fmap (traverse g) . traverse f) x + + equality :: Fun W (Maybe Bool) -> f W -> Property + equality (apply -> f) x = + traverse f x === mapM f x + +testLaw :: Testable a => a -> String -> String -> TestTree +testLaw f lawName lawExpression = testGroup lawName [testProperty lawExpression f ] + +-- | Like '/=', but prints a counterexample when it fails. +infix 4 =/= +(=/=) :: (Eq a, Show a) => a -> a -> Property +(=/=) x y = counterexample (show x <> " == " <> show y) (x /= y)