{-# LANGUAGE ScopedTypeVariables #-} {-| Module: Test.Semiring Description: Some functions for generating tests for 'Semiring's. License: MIT Maintainer: mail@doisinkidney.com Stability: experimental This module provides functions which can be quickly converted into or -like properties. The functions are of the form: > a -> Either String String where the left case is failure of the test, and the right case is success. For smallcheck, this function can be used directly as a property: > smallCheck 10 (plusId :: UnaryLaws Integer) (the typealias is provided as well) For QuickCheck, you might want to provide an instance like this: > instance Testable (Either String String) where > property = either (`counterexample` False) (const (property True)) And then testing is as simple as: > quickCheck (plusAssoc :: TernaryLaws Integer) There are also functions provided to test multiple laws at once. Putting all of this together, writing a test for all the semiring laws for, say, 'Integer' looks like this: > quickCheck (unaryLaws :: UnaryLaws Integer) > quickCheck (binaryLaws :: BinaryLaws Integer) > quickCheck (ternaryLaws :: TernaryLaws Integer) -} module Test.Semiring ( -- * Type Aliases UnaryLaws ,BinaryLaws ,TernaryLaws , -- * Semiring Laws -- ** Unary plusId ,mulId ,annihilateL ,annihilateR ,unaryLaws , -- ** Binary plusComm ,binaryLaws , -- ** Ternary plusAssoc ,mulAssoc ,mulDistribL ,mulDistribR ,ternaryLaws , -- * Near-semiring laws -- ** Unary nearUnaryLaws , -- ** Ternary nearTernaryLaws , -- * StarSemiring Laws -- ** Unary starLaw ,plusLaw ,starLaws , -- * DetectableZero Laws -- ** Unary zeroLaw ,zeroIsZero ,zeroLaws , -- * Ordering Laws -- ** Ternary ordMulLaw ,ordAddLaw ,ordLaws) where import Data.Semiring (Semiring(..), StarSemiring(..), DetectableZero(..)) -- | Typealias for unary laws. Can be used like so: -- -- > smallCheck 10 (unaryLaws :: UnaryLaws Int) type UnaryLaws a = a -> Either String String -- | Typealias for binary laws. Can be used like so: -- -- > smallCheck 8 (binaryLaws :: BinaryLaws Int) type BinaryLaws a = a -> a -> Either String String -- | Typealias for ternary laws. Can be used like so: -- -- > smallCheck 6 (ternaryLaws :: TernaryLaws Int) type TernaryLaws a = a -> a -> a -> Either String String -- | Plus is associative. -- -- @(x '<+>' y) '<+>' z = x '<+>' (y '<+>' z)@ plusAssoc :: (Eq a, Semiring a, Show a) => a -> a -> a -> Either String String plusAssoc x y z = if res then Right s else Left s where res = lp == rp l = x <+> y r = y <+> z lp = l <+> z rp = x <+> r s = unlines [ "<+> is " ++ (if res then "" else "not ") ++ "associative." , " Law:" , " (x <+> y) <+> z = x <+> (y <+> z)" , " x = " ++ show x , " y = " ++ show y , " z = " ++ show z , " x <+> y = " ++ show l , " y <+> z = " ++ show r , " (x <+> y) <+> z = " ++ show lp , " x <+> (y <+> z) = " ++ show rp] -- | Multiplication is associative. -- -- @(x '<.>' y) '<.>' z = x '<.>' (y '<.>' z)@ mulAssoc :: (Eq a, Semiring a, Show a) => a -> a -> a -> Either String String mulAssoc x y z = if res then Right s else Left s where res = lp == rp l = x <.> y r = y <.> z lp = l <.> z rp = x <.> r s = unlines [ "<+> is " ++ (if res then "" else "not ") ++ "associative." , " Law:" , " (x <.> y) <.> z = x <.> (y <.> z)" , " x = " ++ show x , " y = " ++ show y , " z = " ++ show z , " x <.> y = " ++ show l , " y <.> z = " ++ show r , " (x <.> y) <.> z = " ++ show lp , " x <.> (y <.> z) = " ++ show rp] -- | Plus is commutative. -- -- @x '<+>' y = y '<+>' x@ plusComm :: (Eq a, Semiring a, Show a) => a -> a -> Either String String plusComm x y = if res then Right s else Left s where res = l == r l = x <+> y r = y <+> x s = unlines [ "<+> is " ++ (if res then "" else "not ") ++ "commutative." , " Law:" , " x <+> y = y <+> x" , " x = " ++ show x , " y = " ++ show y , " x <+> y = " ++ show l , " y <+> x = " ++ show r] -- | Multiplication distributes left. -- -- @x '<.>' (y '<+>' z) = x '<.>' y '<+>' x '<.>' z@ mulDistribL :: (Eq a, Semiring a, Show a) => a -> a -> a -> Either String String mulDistribL x y z = if res then Right s else Left s where res = l == r l = x <.> (y <+> z) r = x <.> y <+> x <.> z s = unlines [ "<.> does " ++ (if res then "" else "not ") ++ "distribute left over <+>." , " Law:" , " x <.> (y <+> z) = x <.> y <+> x <.> z" , " x = " ++ show x , " y = " ++ show y , " z = " ++ show z , " x <.> (y <+> z) = " ++ show l , " x <.> y <+> x <.> z = " ++ show r] -- | Multiplication distributes right. -- -- @(x '<+>' y) '<.>' z = x '<.>' z '<+>' y '<.>' z@ mulDistribR :: (Eq a, Semiring a, Show a) => a -> a -> a -> Either String String mulDistribR x y z = if res then Right s else Left s where res = l == r l = (x <+> y) <.> z r = x <.> z <+> y <.> z s = unlines [ "<.> does " ++ (if res then "" else "not ") ++ "distribute right over <+>." , " Law:" , " (x <+> y) <.> z = x <.> z <+> y <.> z" , " x = " ++ show x , " y = " ++ show y , " z = " ++ show z , " (x <+> y) <.> z = " ++ show l , " x <.> z <+> y <.> z = " ++ show r] -- | Additive identity. -- -- @x '<+>' 'zero' = 'zero' '<+>' x = x@ plusId :: (Eq a, Semiring a, Show a) => a -> Either String String plusId (x :: a) = if res then Right s else Left s where res = l == x && r == x l = x <+> zero r = zero <+> x s = unlines [ "zero is" ++ (if res then "" else " not") ++ " the identity of <+>." , " Law:" , " x <+> zero = zero <+> x = x" , " x = " ++ show x , " zero = " ++ show (zero :: a) , " x <+> zero = " ++ show l , " zero <+> x = " ++ show r] -- | Multiplicative identity. -- -- @x '<.>' 'one' = 'one' '<.>' x = x@ mulId :: (Eq a, Semiring a, Show a) => a -> Either String String mulId (x :: a) = if res then Right s else Left s where res = l == x && r == x l = x <.> one r = one <.> x s = unlines [ "one is" ++ (if res then "" else " not") ++ " the identity of <+>." , " Law:" , " x <.> one = one <.> x = x" , " x = " ++ show x , " one = " ++ show (one :: a) , " x <.> one = " ++ show l , " one <.> x = " ++ show r] -- | Right annihilation of '<.>' by 'zero'. -- -- @'zero' '<.>' x = 'zero'@ annihilateR :: (Eq a, Semiring a, Show a) => a -> Either String String annihilateR (x :: a) = if res then Right s else Left s where res = r == zero r = zero <.> x s = unlines [ "zero does " ++ (if res then "" else "not ") ++ "annihilate right with <.>." , " Law:" , " zero <.> x = zero" , " x = " ++ show x , " zero = " ++ show (zero :: a) , " zero <.> x = " ++ show r] -- | Left annihilation of '<.>' by 'zero'. -- -- @x '<.>' 'zero' = 'zero'@ annihilateL :: (Eq a, Semiring a, Show a) => a -> Either String String annihilateL (x :: a) = if res then Right s else Left s where res = l == zero l = x <.> zero s = unlines [ "zero does " ++ (if res then "" else "not ") ++ "annihilate left with <.>." , " Law:" , " x <.> zero = zero" , " x = " ++ show x , " zero = " ++ show (zero :: a) , " x <.> zero = " ++ show l] -- | A test for all three unary laws for 'Semiring's ('plusId', 'mulId', -- 'annihilateL', and 'annihilateR'). unaryLaws :: (Eq a, Semiring a, Show a) => a -> Either String String unaryLaws x = fmap unlines (sequence [plusId x, mulId x, annihilateL x, annihilateR x]) -- | A test for the unary laws for near-'Semiring's ('plusId', 'mulId', and -- 'annihilateR'). nearUnaryLaws :: (Eq a, Semiring a, Show a) => a -> Either String String nearUnaryLaws x = fmap unlines (sequence [plusId x, mulId x, annihilateR x]) -- | A test for all of the ternary laws for near-'Semiring's ('plusAssoc', -- 'mulAssoc', 'mulDistribR'). nearTernaryLaws :: (Eq a, Semiring a, Show a) => a -> a -> a -> Either String String nearTernaryLaws x y z = fmap unlines (sequence [plusAssoc x y z, mulAssoc x y z, mulDistribR x y z]) -- | A test for all of the binary laws for 'Semiring's (just 'plusComm'). binaryLaws :: (Eq a, Semiring a, Show a) => a -> a -> Either String String binaryLaws = plusComm -- | A test for all of the ternary laws for 'Semiring's ('plusAssoc', 'mulAssoc', -- 'mulDistribL', 'mulDistribR'). ternaryLaws :: (Eq a, Semiring a, Show a) => a -> a -> a -> Either String String ternaryLaws x y z = fmap unlines (sequence [ plusAssoc x y z , mulAssoc x y z , mulDistribR x y z , mulDistribL x y z]) -- | The star law for 'StarSemiring's. -- -- @'star' x = 'one' '<+>' x '<.>' 'star' x = 'one' '<+>' 'star' x '<.>' x@ starLaw :: (Eq a, StarSemiring a, Show a) => a -> Either String String starLaw (x :: a) = if res then Right s else Left s where res = l == st && r == st l = one <+> x <.> star x r = one <+> star x <.> x st = star x s = unlines [ "star law" ++ (if res then "" else " not") ++ " followed." , " Law:" , " star x = one <+> x <.> star x = one <+> star x <.> x" , " x = " ++ show x , " one = " ++ show (one :: a) , " star x = " ++ show st , " one <+> x <.> star x = " ++ show l , " one <+> star x <.> x = " ++ show r] -- | The plus law for 'StarSemiring's. -- -- @'plus' x = x '<.>' 'star' x@ plusLaw :: (Eq a, StarSemiring a, Show a) => a -> Either String String plusLaw (x :: a) = if res then Right s else Left s where res = r == st r = x <.> star x st = plus x s = unlines [ "plus law" ++ (if res then "" else " not") ++ " followed." , " Law:" , " plus x = x <.> star x" , " x = " ++ show x , " star x = " ++ show st , " x <.> star x = " ++ show r] -- | The laws for 'StarSemiring's ('starLaw', 'plusLaw'). starLaws :: (Eq a, StarSemiring a, Show a) => a -> Either String String starLaws x = fmap unlines (sequence [starLaw x, plusLaw x]) -- | Addition law for ordered 'Semiring's. -- -- @x '<=' y => x '<+>' z '<=' y '<+>' z '&&' z '<+>' x '<=' z '<+>' y@ ordAddLaw :: (Ord a, Semiring a, Show a) => a -> a -> a -> Either String String ordAddLaw (x :: a) (y :: a) (z :: a) = if res then Right s else Left s where cnd = x <= y lhs = x <+> z <= y <+> z rhs = z <+> x <= z <+> y res = not cnd || lhs && rhs s = unlines [ "additive ordering law" ++ (if res then "" else " not") ++ " followed." , " Law:" , " x <= y => x <+> z <= y <+> z && z <+> x <= z <+> y" , " x = " ++ show x , " y = " ++ show y , " z = " ++ show z] -- | Multiplication law for ordered 'Semiring's. -- -- @x '<=' y => x '<.>' z '<=' y '<.>' z '&&' z '<.>' x '<=' z '<.>' y@ ordMulLaw :: (Ord a, Semiring a, Show a) => a -> a -> a -> Either String String ordMulLaw (x :: a) (y :: a) (z :: a) = if res then Right s else Left s where cnd = x <= y && zero <= z lhs = x <.> z <= y <.> z rhs = z <.> x <= z <.> y res = not cnd || lhs && rhs s = unlines [ "ordering law" ++ (if res then "" else " not") ++ " followed." , " Law:" , " x <= y => x <.> z <= y <.> z && z <.> x <= z <.> y" , " x = " ++ show x , " y = " ++ show y , " z = " ++ show z] -- | Laws for ordered 'Semiring's ('ordMulLaw', 'ordAddLaw'). ordLaws :: (Ord a, Semiring a, Show a) => a -> a -> a -> Either String String ordLaws x y z = fmap unlines (sequence [ordAddLaw x y z, ordMulLaw x y z]) -- | Law for result of 'isZero' operation. -- -- @x '==' 'zero' = 'zero' '==' x = 'isZero' x@ zeroLaw :: (Eq a, DetectableZero a, Show a) => a -> Either String String zeroLaw (x :: a) = if res then Right s else Left s where lhs_1 = x == zero lhs_2 = zero == x rhs = isZero x res = lhs_1 == rhs && lhs_2 == rhs s = unlines [ "zero law" ++ (if res then "" else " not") ++ " followed." , " Law:" , " x == zero = zero == x = isZero x" , " x = " ++ show x , " x == zero = " ++ show lhs_1 , " zero == x = " ++ show lhs_2 , " isZero x = " ++ show rhs] -- | Zero is zero law. -- -- @'isZero' 'zero' = 'True'@ zeroIsZero :: (DetectableZero a, Show a) => f a -> Either String String zeroIsZero (_ :: f a) = if res then Right s else Left s where z = zero :: a res = isZero z s = unlines [ "zero is zero law" ++ (if res then "" else " not") ++ " followed." , " Law:" , " isZero zero = True" , " zero = " ++ show z , " isZero zero = " ++ show res] -- | The laws for 'DetectableZero' 'Semiring's ('zeroLaw', 'zeroIsZero'). zeroLaws :: (DetectableZero a, Show a, Eq a) => a -> Either String String zeroLaws x = zeroLaw x *> zeroIsZero [x]