{-# 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 { BoolRing a -> a
getBoolRing :: a }

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

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

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

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