The Monoid class
edit
1. Warning: very slow proofs ahead.
The two more common monoids for Bool are those under conjunction ("and" i.e. (&&)) and disjunction ("or" i.e. (||)). They are the ones in Data.Monoid:
newtype All = All { getAll :: Bool }
instance Monoid All where
mempty = All True
mappend (All p) (All q) = All (p && q)
-- Laws:
mempty <> p = p -- left identity
True && p = p
-- For p = True:
True && True = True
True = True -- OK
-- For p = False:
True && False = False
False = False -- Q.E.D
p <> mempty = p -- right identity
p && True = p
-- For p = True:
True && True = True
True = True -- OK
-- For p = False:
False && True = False
False = False -- OK
-- Q.E.D
(p <> q) <> r = p <> (q <> r) -- associativity
(p && q) && r = p && (q && r)
-- For r = False:
(p && q) && False = p && (q && False)
False = p && False
False = False -- OK
-- For r = True:
(p && q) && True = p && (q && True)
p && q = p && q -- right identity
-- Q.E.D (no need to check all possibilities of p and q)
Note that, since (&&) is commutative (that is, p && q = q && p), if the left identity law holds right identity will hold too, and vice-versa. That means we only needed to prove one of the identity laws. We will use this shortcut in the following answers.
newtype Any = Any { getAny :: Bool }
instance Monoid Any where
mempty = Any False
mappend (Any p) (Any q) = Any (p || q)
-- Laws:
mempty <> p = p -- left identity
False || p = p
-- For p = True:
False || True = True
True = True -- OK
-- For p = False:
False || False = False
False = False -- OK
--Q.E.D
-- (||) is commutative, so since left identity holds
-- right identity holds as well.
(p <> q) <> r = p <> (q <> r) -- associativity
(p || q) || r = p || (q || r)
-- For r = False:
(p || q) || False = p || (q || False)
p || q = p || q -- OK (left identity)
-- For r = True:
(p || q) || True = p || (q || True)
True = p || True -- right identity
True = True -- OK
-- Q.E.D
Exclusive disjunction ("either-or", "XOR") and material equivalence ("if-and-only-if", logical bicondicional) also form monoids.
-- Exclusive disjunction
xor :: Bool -> Bool -> Bool
xor True q = not q
xor _ q = q
-- Note that xor is the same as (/=) for Bool.
newtype OnlyOne = OnlyOne { getOnlyOne :: Bool }
instance Monoid OnlyOne where
mempty = OnlyOne False
mappend (OnlyOne p) (OnlyOne q) = OnlyOne (xor p q)
-- Laws:
mempty <> p = p -- left identity
xor False p = p
-- For p = True:
xor False True = True
True = True -- OK
-- For p = False:
xor False False = False
False = False -- OK
-- Q.E.D
-- xor, like (/=), is commutative, so since left identity holds
-- right identity holds as well.
(p <> q) <> r = p <> (q <> r) -- associativity
xor (xor p q) r = xor p (xor q r)
-- For r = False:
xor (xor p q) False = xor p (xor q False)
xor p q = xor p q -- OK
-- For r = True:
xor (xor p q) True = xor p (xor q True)
not (xor p q) = xor p (not q)
-- * For q = False:
not (xor p False) = xor p (not False)
not p = xor p True
not p = not p -- OK
-- * For q = True
not (xor p True) = xor p (not True)
not (not p) = xor p False
p = p -- OK
-- Q.E.D
-- Material equivalence
eqv :: Bool -> Bool -> Bool
eqv True q = q
eqv _ q = not q
-- Note that eqv is the same as (==) for Bool,
-- as well as equivalent to ((not .) . xor).
newtype AllOrNone = AllOrNone { getAllOrNone :: Bool }
instance Monoid AllOrNone where
mempty = AllOrNone True
mappend (AllOrNone p) (AllOrNone q) = AllOrNone (eqv p q)
-- Laws (we will do this one a bit faster):
mempty <> p = p -- left identity
eqv True p = p
p = p -- Q.E.D (see definition)
-- eqv, like (==), is commutative, so since left identity holds
-- right identity holds as well.
(p <> q) <> r = p <> (q <> r) -- associativity
eqv (eqv p q) r = eqv p (eqv q r)
-- For r = False:
eqv (eqv p q) False = eqv p (eqv q False)
not (eqv p q) = eqv p (not q)
-- * For q = False:
not (eqv p False) = eqv p (not False)
not (not p) = eqv p True
p = p -- OK
-- * For q = True
not (eqv p True) = eqv p (not True)
not p = eqv p False
not p = not p -- OK
-- For r = True:
eqv (eqv p q) True = eqv p (eqv q True)
eqv p q = eqv p q -- OK
-- Q.E.D