Haskell/解决方案/幺半群

`Monoid` 类

1. 警告：前方非常缓慢的证明。

对于 Bool，两个最常见的幺半群是那些在合取（“与”即 (&&)）和析取（“或”即 (||)）下的幺半群。它们是 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)

请注意，由于 (&&) 是可交换的（即 p && q = q && p），如果左单位律成立，右单位律也会成立，反之亦然。这意味着我们只需要证明其中一个单位律。在以下答案中，我们将使用此捷径。

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

异或（“或非”，“XOR”）和实质等价（“当且仅当”，“逻辑双条件”）也形成幺半群。

-- 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

Monoid 类

`Monoid` 类