ideas-1.0: src/Common/Algebra/Group.hs

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-----------------------------------------------------------------------------
-- Copyright 2011, Open Universiteit Nederland. This file is distributed
-- under the terms of the GNU General Public License. For more information,
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-----------------------------------------------------------------------------
module Common.Algebra.Group
   ( -- * Monoids
     module Data.Monoid, (<>), associative, leftIdentity
   , rightIdentity, identityLaws, monoidLaws, commutativeMonoidLaws
   , idempotent
     -- * Groups
   , Group(..), (<>-), leftInverse, rightInverse, doubleInverse
   , inverseIdentity, inverseDistrFlipped, inverseLaws, groupLaws
   , appendInverseLaws
     -- * Abelian groups
   , commutative, inverseDistr, abelianGroupLaws
     -- * Monoids with a zero element
   , MonoidZero(..), leftZero, rightZero, zeroLaws, monoidZeroLaws
   , WithZero, fromWithZero
     -- * Generalized laws
   , associativeFor, commutativeFor, idempotentFor
   , leftDistributiveFor, rightDistributiveFor
   ) where

import Common.Algebra.Law
import Control.Applicative (Applicative)
import Control.Monad (liftM2)
import Data.Foldable (Foldable)
import Data.Monoid
import Data.Traversable (Traversable)

--------------------------------------------------------
-- Monoids

infixl 6 <>

(<>) :: Monoid a => a -> a -> a
(<>) = mappend

associative :: Monoid a => Law a
associative = associativeFor (<>)

leftIdentity :: Monoid a => Law a
leftIdentity = law "left-identity" $ \a -> mempty <> a :==: a

rightIdentity :: Monoid a => Law a
rightIdentity = law "right-identity" $ \a -> a <> mempty :==: a

identityLaws :: Monoid a => [Law a]
identityLaws = [leftIdentity, rightIdentity]

monoidLaws :: Monoid a => [Law a]
monoidLaws = associative : identityLaws

commutativeMonoidLaws :: Monoid a => [Law a]
commutativeMonoidLaws = monoidLaws ++ [commutative]

-- | Not all monoids are idempotent (see: idempotentFor)
idempotent :: Monoid a => Law a
idempotent = idempotentFor (<>)

--------------------------------------------------------
-- Groups

-- | Minimal complete definition: inverse or appendInverse
class Monoid a => Group a where
   inverse   :: a -> a
   appendInv :: a -> a -> a
   -- default definitions
   inverse = (mempty <>-)
   appendInv a b = a <> inverse b

infixl 6 <>-

(<>-) :: Group a => a -> a -> a
(<>-) = appendInv

leftInverse :: Group a => Law a
leftInverse = law "left-inverse" $ \a -> inverse a <> a :==: mempty

rightInverse :: Group a => Law a
rightInverse = law "right-inverse" $ \a -> a <> inverse a :==: mempty

doubleInverse :: Group a => Law a
doubleInverse = law "double-inverse" $ \a -> inverse (inverse a) :==: a

inverseIdentity :: Group a => Law a
inverseIdentity = law "inverse-identity" $ inverse mempty :==: mempty

inverseDistrFlipped :: Group a => Law a
inverseDistrFlipped = law "inverse-distr-flipped" $ \a b ->
   inverse (a <> b) :==: inverse b <> inverse a

inverseLaws :: Group a => [Law a]
inverseLaws = [leftInverse, rightInverse]

groupLaws :: Group a => [Law a]
groupLaws = monoidLaws ++ inverseLaws ++
   [doubleInverse, inverseIdentity, inverseDistrFlipped]

appendInverseLaws :: Group a => [Law a]
appendInverseLaws =
   [ make 1 $ \a b   ->           a <>- b :==: a <> inverse b
   , make 2 $ \a     ->           a <>- a :==: mempty
   , make 3 $ \a     ->      a <>- mempty :==: a
   , make 4 $ \a     ->      mempty <>- a :==: inverse a
   , make 5 $ \a b c ->    a <>- (b <> c) :==: (a <>- b) <>- c
   , make 6 $ \a b c ->   a <>- (b <>- c) :==: (a <>- b) <> c
   , make 7 $ \a b c ->    a <> (b <>- c) :==: (a <> b) <>- c
   , make 8 $ \a b   ->   a <>- inverse b :==: a <> b
   , make 9 $ \a b   -> inverse (a <>- b) :==: inverse a <> b
   ]
 where
    make n = law ("append-inverse-law" ++ show (n :: Int))

--------------------------------------------------------
-- Abelian groups

commutative :: Monoid a => Law a
commutative = commutativeFor (<>)

inverseDistr :: Group a => Law a
inverseDistr = law "inverse-distr" $ \a b ->
    inverse (a <> b) :==: (inverse a <> inverse b)

abelianGroupLaws :: Group a => [Law a]
abelianGroupLaws = groupLaws ++ [commutative, inverseDistr]

--------------------------------------------------------
-- Monoids with a zero element
-- This element could be the additive identity from a (semi-)ring for
-- the multiplicative monoid

class Monoid a => MonoidZero a where
   mzero :: a

leftZero :: MonoidZero a => Law a
leftZero = law "left-zero" $ \a -> mzero <> a :==: mzero

rightZero:: MonoidZero a => Law a
rightZero = law "right-zero" $ \a -> a <> mzero :==: mzero

zeroLaws :: MonoidZero a => [Law a]
zeroLaws = [leftZero, rightZero]

monoidZeroLaws :: MonoidZero a => [Law a]
monoidZeroLaws = monoidLaws ++ zeroLaws

-- Type that adds a zero element
newtype WithZero a = WZ { fromWithZero :: Maybe a }
   deriving (Eq, Ord, Functor, Foldable, Traversable, Applicative)

instance Monoid a => Monoid (WithZero a) where
   mempty = WZ (Just mempty)
   mappend x y = WZ (liftM2 mappend (fromWithZero x) (fromWithZero y))

instance Monoid a => MonoidZero (WithZero a) where
   mzero = WZ Nothing

--------------------------------------------------------
-- Generalized laws

associativeFor :: (a -> a -> a) -> Law a
associativeFor (?) = law "associative" $ \a b c ->
   a ? (b ? c) :==: (a ? b) ? c

commutativeFor :: (a -> a -> a) -> Law a
commutativeFor (?) = law "commutative" $ \a b -> a ? b :==: b ? a

idempotentFor :: (a -> a -> a) -> Law a
idempotentFor (?) = law "idempotent" $ \a -> a ? a :==: a

leftDistributiveFor :: (a -> a -> a) -> (a -> a -> a) -> Law a
leftDistributiveFor (<*>) (<+>) = law "left-distributive" $ \a b c ->
   a <*> (b <+> c) :==: (a <*> b) <+> (a <*> c)

rightDistributiveFor :: (a -> a -> a) -> (a -> a -> a) -> Law a
rightDistributiveFor (<*>) (<+>) = law "right-distributive" $ \a b c ->
   (a <+> b) <*> c :==: (a <*> c) <+> (b <*> c)