Haskell/Solutions/Monoids

The Monoid class 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 Semigroup All where (All p) <> (All q) = All (p && q) instance Monoid All where mempty = All True -- 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 Semigroup Any where (Any p) <> (Any q) = Any (p || q) instance Monoid Any where mempty = Any False -- 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 Semigroup OnlyOne where (OnlyOne p) <> (OnlyOne q) = OnlyOne (xor p q) instance Monoid OnlyOne where mempty = OnlyOne False -- 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 Semigroup AllOrNone where (AllOrNone p) <> (AllOrNone q) = AllOrNone (eqv p q) instance Monoid AllOrNone where mempty = AllOrNone True -- 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