BoolRing.hs

{-# LANGUAGE CPP #-}
module Algebra.Heyting.BoolRing
  ( BoolRing (..)
  , Semiring (..)
  , (<+>)
  ) where

import           Prelude

#if __GLASGOW_HASKELL__ < 808
import           Data.Monoid (Monoid (..))
#endif
#if __GLASGOW_HASKELL__ < 804
import           Data.Semigroup (Semigroup (..))
#endif

import           Algebra.Lattice (bottom, top, (/\), (\/))
import           Data.Semiring (Semiring (..), (<+>))

import           Algebra.Heyting

-- |
-- Newtype wraper which captures Boolean ring structure, which holds for every
-- Heyting algebra.  A Boolean ring is a ring which satisfies:
--
-- prop> a <.> a = a
--
-- Some other properties:
--
-- prop> a <+> a = mempty                  -- thus it is a ring of characteristic 2
-- prop> a <.> b = b <.> a                 -- hence it is a commutative ring
-- prop> a <+> (b <+> c) = (a <+> b) <+> c -- multiplicative associativity
newtype BoolRing a = BoolRing { getBoolRing :: a }

-- | Sum is [symmetric differnce](https://en.wikipedia.org/wiki/Symmetric_difference).
instance Heyting a => Semigroup (BoolRing a) where
  (BoolRing a) <> (BoolRing b) = BoolRing $ (neg a /\ b) \/ (a /\ neg b)

-- | In a Boolean ring @a + a = 0@, hence @negate = id@.
instance Heyting a => Monoid (BoolRing a) where
  mempty = BoolRing bottom

#if __GLASGOW_HASKELL__ <= 804
  mappend = (<>)
#endif

-- |  Multiplication is given by @'/\'@
instance Heyting a => Semiring (BoolRing a) where
  BoolRing a <.> BoolRing b = BoolRing (a \/ b)
  one = BoolRing top