{- |
Define common properties that can be used e.g. for automated tests.
Cf. to "Test.QuickCheck.Utils".
-}
module Algebra.Laws where


commutative :: Eq a => (b -> b -> a) -> b -> b -> Bool
commutative :: (b -> b -> a) -> b -> b -> Bool
commutative b -> b -> a
op b
x b
y  =  b
x b -> b -> a
`op` b
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== b
y b -> b -> a
`op` b
x

associative :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool
associative :: (a -> a -> a) -> a -> a -> a -> Bool
associative a -> a -> a
op a
x a
y a
z  =  (a
x a -> a -> a
`op` a
y) a -> a -> a
`op` a
z a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x a -> a -> a
`op` (a
y a -> a -> a
`op` a
z)

leftIdentity :: Eq a => (b -> a -> a) -> b -> a -> Bool
leftIdentity :: (b -> a -> a) -> b -> a -> Bool
leftIdentity b -> a -> a
op b
y a
x  =  b
y b -> a -> a
`op` a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x

rightIdentity :: Eq a => (a -> b -> a) -> b -> a -> Bool
rightIdentity :: (a -> b -> a) -> b -> a -> Bool
rightIdentity a -> b -> a
op b
y a
x  =  a
x a -> b -> a
`op` b
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x

identity :: Eq a => (a -> a -> a) -> a -> a -> Bool
identity :: (a -> a -> a) -> a -> a -> Bool
identity a -> a -> a
op a
x a
y  =  (a -> a -> a) -> a -> a -> Bool
forall a b. Eq a => (b -> a -> a) -> b -> a -> Bool
leftIdentity a -> a -> a
op a
x a
y Bool -> Bool -> Bool
&&  (a -> a -> a) -> a -> a -> Bool
forall a b. Eq a => (a -> b -> a) -> b -> a -> Bool
rightIdentity a -> a -> a
op a
x a
y

leftZero :: Eq a => (a -> a -> a) -> a -> a -> Bool
leftZero :: (a -> a -> a) -> a -> a -> Bool
leftZero  =  (a -> a -> Bool) -> a -> a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> a -> Bool) -> a -> a -> Bool)
-> ((a -> a -> a) -> a -> a -> Bool)
-> (a -> a -> a)
-> a
-> a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> a) -> a -> a -> Bool
forall a b. Eq a => (a -> b -> a) -> b -> a -> Bool
rightIdentity

rightZero :: Eq a => (a -> a -> a) -> a -> a -> Bool
rightZero :: (a -> a -> a) -> a -> a -> Bool
rightZero  =  (a -> a -> Bool) -> a -> a -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a -> a -> Bool) -> a -> a -> Bool)
-> ((a -> a -> a) -> a -> a -> Bool)
-> (a -> a -> a)
-> a
-> a
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a -> a) -> a -> a -> Bool
forall a b. Eq a => (b -> a -> a) -> b -> a -> Bool
leftIdentity

zero :: Eq a => (a -> a -> a) -> a -> a -> Bool
zero :: (a -> a -> a) -> a -> a -> Bool
zero a -> a -> a
op a
x a
y  =  (a -> a -> a) -> a -> a -> Bool
forall a. Eq a => (a -> a -> a) -> a -> a -> Bool
leftZero a -> a -> a
op a
x a
y  Bool -> Bool -> Bool
&&  (a -> a -> a) -> a -> a -> Bool
forall a. Eq a => (a -> a -> a) -> a -> a -> Bool
rightZero a -> a -> a
op a
x a
y

leftInverse :: Eq a => (b -> b -> a) -> (b -> b) -> a -> b -> Bool
leftInverse :: (b -> b -> a) -> (b -> b) -> a -> b -> Bool
leftInverse b -> b -> a
op b -> b
inv a
y b
x  =  b -> b
inv b
x b -> b -> a
`op` b
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y

rightInverse :: Eq a => (b -> b -> a) -> (b -> b) -> a -> b -> Bool
rightInverse :: (b -> b -> a) -> (b -> b) -> a -> b -> Bool
rightInverse b -> b -> a
op b -> b
inv a
y b
x  =  b
x b -> b -> a
`op` b -> b
inv b
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y

inverse :: Eq a => (b -> b -> a) -> (b -> b) -> a -> b -> Bool
inverse :: (b -> b -> a) -> (b -> b) -> a -> b -> Bool
inverse b -> b -> a
op b -> b
inv a
y b
x  =  (b -> b -> a) -> (b -> b) -> a -> b -> Bool
forall a b. Eq a => (b -> b -> a) -> (b -> b) -> a -> b -> Bool
leftInverse b -> b -> a
op b -> b
inv a
y b
x Bool -> Bool -> Bool
&& (b -> b -> a) -> (b -> b) -> a -> b -> Bool
forall a b. Eq a => (b -> b -> a) -> (b -> b) -> a -> b -> Bool
rightInverse b -> b -> a
op b -> b
inv a
y b
x

leftDistributive :: Eq a => (a -> b -> a) -> (a -> a -> a) -> b -> a -> a -> Bool
leftDistributive :: (a -> b -> a) -> (a -> a -> a) -> b -> a -> a -> Bool
leftDistributive ( # ) a -> a -> a
op b
x a
y a
z  =  (a
y a -> a -> a
`op` a
z) a -> b -> a
# b
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (a
y a -> b -> a
# b
x) a -> a -> a
`op` (a
z a -> b -> a
# b
x)

rightDistributive :: Eq a => (b -> a -> a) -> (a -> a -> a) -> b -> a -> a -> Bool
rightDistributive :: (b -> a -> a) -> (a -> a -> a) -> b -> a -> a -> Bool
rightDistributive ( # ) a -> a -> a
op b
x a
y a
z  =  b
x b -> a -> a
# (a
y a -> a -> a
`op` a
z) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (b
x b -> a -> a
# a
y) a -> a -> a
`op` (b
x b -> a -> a
# a
z)

homomorphism :: Eq a =>
   (b -> a) -> (b -> b -> b) -> (a -> a -> a) -> b -> b -> Bool
homomorphism :: (b -> a) -> (b -> b -> b) -> (a -> a -> a) -> b -> b -> Bool
homomorphism b -> a
f b -> b -> b
op0 a -> a -> a
op1 b
x b
y  =  b -> a
f (b
x b -> b -> b
`op0` b
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== b -> a
f b
x a -> a -> a
`op1` b -> a
f b
y

rightCascade :: Eq a =>
   (b -> b -> b) -> (a -> b -> a) -> a -> b -> b -> Bool
rightCascade :: (b -> b -> b) -> (a -> b -> a) -> a -> b -> b -> Bool
rightCascade ( # ) a -> b -> a
op a
x b
i b
j  =  (a
x a -> b -> a
`op` b
i) a -> b -> a
`op` b
j a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x a -> b -> a
`op` (b
ib -> b -> b
#b
j)

leftCascade :: Eq a =>
   (b -> b -> b) -> (b -> a -> a) -> a -> b -> b -> Bool
leftCascade :: (b -> b -> b) -> (b -> a -> a) -> a -> b -> b -> Bool
leftCascade ( # ) b -> a -> a
op a
x b
i b
j  =  b
j b -> a -> a
`op` (b
i b -> a -> a
`op` a
x) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== (b
jb -> b -> b
#b
i) b -> a -> a
`op` a
x