{-# LANGUAGE NoRebindableSyntax #-}

-- | Free ring — the initial encoding of 'Ring'.
module NumHask.Free.Ring
  ( Ring (..),
    zero,
    one,
    plus,
    negate,
    minus,
    times,
    embed,
    lift,
    normalize,
    eval,
    foldRing,
    fromAdditive,
    fromMultiplicative,
    fromSubtractive,
  )
where

import NumHask.Algebra.Additive qualified as NHA
import NumHask.Algebra.Multiplicative qualified as NHM
import NumHask.Algebra.Ring qualified as NHR
import NumHask.Free.Additive qualified as HA
import NumHask.Free.Multiplicative qualified as HM
import NumHask.Free.Subtractive qualified as HS
import Prelude (Eq, Show, otherwise, (==))

-- | Free ring over a carrier type.
--
-- The initial encoding of 'NumHask.Algebra.Ring.Ring'.
-- Combines additive and multiplicative structure with the
-- antipode.  Distributivity is enforced by 'eval', not by
-- the term structure — 'Times' over 'Plus' is not reduced
-- automatically.  Use 'eval' to project into a lawful ring.
data Ring a
  = Zero
  | One
  | Plus (Ring a) (Ring a)
  | Negate (Ring a)
  | Times (Ring a) (Ring a)
  | Embed a
  deriving (Ring a -> Ring a -> Bool
(Ring a -> Ring a -> Bool)
-> (Ring a -> Ring a -> Bool) -> Eq (Ring a)
forall a. Eq a => Ring a -> Ring a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Ring a -> Ring a -> Bool
== :: Ring a -> Ring a -> Bool
$c/= :: forall a. Eq a => Ring a -> Ring a -> Bool
/= :: Ring a -> Ring a -> Bool
Eq, Int -> Ring a -> ShowS
[Ring a] -> ShowS
Ring a -> String
(Int -> Ring a -> ShowS)
-> (Ring a -> String) -> ([Ring a] -> ShowS) -> Show (Ring a)
forall a. Show a => Int -> Ring a -> ShowS
forall a. Show a => [Ring a] -> ShowS
forall a. Show a => Ring a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Ring a -> ShowS
showsPrec :: Int -> Ring a -> ShowS
$cshow :: forall a. Show a => Ring a -> String
show :: Ring a -> String
$cshowList :: forall a. Show a => [Ring a] -> ShowS
showList :: [Ring a] -> ShowS
Show)

-- | Additive identity.
zero :: Ring a
zero :: forall a. Ring a
zero = Ring a
forall a. Ring a
Zero

-- | Multiplicative identity.
one :: Ring a
one :: forall a. Ring a
one = Ring a
forall a. Ring a
One

-- | Addition with identity absorption.
plus :: Ring a -> Ring a -> Ring a
plus :: forall a. Ring a -> Ring a -> Ring a
plus Ring a
Zero Ring a
b = Ring a
b
plus Ring a
a Ring a
Zero = Ring a
a
plus Ring a
a Ring a
b = Ring a -> Ring a -> Ring a
forall a. Ring a -> Ring a -> Ring a
Plus Ring a
a Ring a
b

-- | Antipode with involution cancellation.
negate :: Ring a -> Ring a
negate :: forall a. Ring a -> Ring a
negate Ring a
Zero = Ring a
forall a. Ring a
Zero
negate (Negate Ring a
a) = Ring a
a
negate Ring a
a = Ring a -> Ring a
forall a. Ring a -> Ring a
Negate Ring a
a

-- | Subtraction as addition of the antipode.
minus :: Ring a -> Ring a -> Ring a
minus :: forall a. Ring a -> Ring a -> Ring a
minus Ring a
a Ring a
b = Ring a -> Ring a -> Ring a
forall a. Ring a -> Ring a -> Ring a
plus Ring a
a (Ring a -> Ring a
forall a. Ring a -> Ring a
negate Ring a
b)

-- | Multiplication with identity absorption.
times :: Ring a -> Ring a -> Ring a
times :: forall a. Ring a -> Ring a -> Ring a
times Ring a
One Ring a
b = Ring a
b
times Ring a
a Ring a
One = Ring a
a
times Ring a
a Ring a
b = Ring a -> Ring a -> Ring a
forall a. Ring a -> Ring a -> Ring a
Times Ring a
a Ring a
b

-- | Embed a carrier value as an atomic generator.
embed :: a -> Ring a
embed :: forall a. a -> Ring a
embed = a -> Ring a
forall a. a -> Ring a
Embed

-- $setup
-- >>> import Prelude (fromInteger)

-- | Lift a carrier value, absorbing additive and multiplicative identities.
--
-- >>> lift 0
-- Zero
-- >>> lift 1
-- One
lift :: (Eq a, NHR.Ring a) => a -> Ring a
lift :: forall a. (Eq a, Ring a) => a -> Ring a
lift a
a
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Additive a => a
NHA.zero = Ring a
forall a. Ring a
Zero
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Multiplicative a => a
NHM.one = Ring a
forall a. Ring a
One
  | Bool
otherwise = a -> Ring a
forall a. a -> Ring a
Embed a
a

-- | Normalize a term with respect to ring laws: identity absorption and
-- antipode involution. Distributivity is left to 'eval'.
--
-- >>> normalize (embed 0)
-- Zero
normalize :: (Eq a, NHR.Ring a) => Ring a -> Ring a
normalize :: forall a. (Eq a, Ring a) => Ring a -> Ring a
normalize Ring a
Zero = Ring a
forall a. Ring a
Zero
normalize Ring a
One = Ring a
forall a. Ring a
One
normalize (Embed a
a)
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Additive a => a
NHA.zero = Ring a
forall a. Ring a
Zero
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Multiplicative a => a
NHM.one = Ring a
forall a. Ring a
One
  | Bool
otherwise = a -> Ring a
forall a. a -> Ring a
Embed a
a
normalize (Plus Ring a
a Ring a
b) = Ring a -> Ring a -> Ring a
forall a. Ring a -> Ring a -> Ring a
plus (Ring a -> Ring a
forall a. (Eq a, Ring a) => Ring a -> Ring a
normalize Ring a
a) (Ring a -> Ring a
forall a. (Eq a, Ring a) => Ring a -> Ring a
normalize Ring a
b)
normalize (Negate Ring a
a) = Ring a -> Ring a
forall a. Ring a -> Ring a
negate (Ring a -> Ring a
forall a. (Eq a, Ring a) => Ring a -> Ring a
normalize Ring a
a)
normalize (Times Ring a
a Ring a
b) = Ring a -> Ring a -> Ring a
forall a. Ring a -> Ring a -> Ring a
times (Ring a -> Ring a
forall a. (Eq a, Ring a) => Ring a -> Ring a
normalize Ring a
a) (Ring a -> Ring a
forall a. (Eq a, Ring a) => Ring a -> Ring a
normalize Ring a
b)

-- | Evaluate a term into any 'NumHask.Algebra.Ring.Ring'.
--
-- This is the unique homomorphism out of the free ring.
eval :: (NHR.Ring a) => Ring a -> a
eval :: forall a. Ring a => Ring a -> a
eval Ring a
Zero = a
forall a. Additive a => a
NHA.zero
eval Ring a
One = a
forall a. Multiplicative a => a
NHM.one
eval (Plus Ring a
a Ring a
b) = Ring a -> a
forall a. Ring a => Ring a -> a
eval Ring a
a a -> a -> a
forall a. Additive a => a -> a -> a
NHA.+ Ring a -> a
forall a. Ring a => Ring a -> a
eval Ring a
b
eval (Negate Ring a
a) = a -> a
forall a. Subtractive a => a -> a
NHA.negate (Ring a -> a
forall a. Ring a => Ring a -> a
eval Ring a
a)
eval (Times Ring a
a Ring a
b) = Ring a -> a
forall a. Ring a => Ring a -> a
eval Ring a
a a -> a -> a
forall a. Multiplicative a => a -> a -> a
NHM.* Ring a -> a
forall a. Ring a => Ring a -> a
eval Ring a
b
eval (Embed a
a) = a
a

-- | Universal property: fold with a target ring.
foldRing ::
  b ->
  b ->
  (b -> b -> b) ->
  (b -> b) ->
  (b -> b -> b) ->
  (a -> b) ->
  Ring a ->
  b
foldRing :: forall b a.
b
-> b
-> (b -> b -> b)
-> (b -> b)
-> (b -> b -> b)
-> (a -> b)
-> Ring a
-> b
foldRing b
z b
o b -> b -> b
p b -> b
n b -> b -> b
t a -> b
f = Ring a -> b
go
  where
    go :: Ring a -> b
go Ring a
Zero = b
z
    go Ring a
One = b
o
    go (Plus Ring a
a Ring a
b) = b -> b -> b
p (Ring a -> b
go Ring a
a) (Ring a -> b
go Ring a
b)
    go (Negate Ring a
a) = b -> b
n (Ring a -> b
go Ring a
a)
    go (Times Ring a
a Ring a
b) = b -> b -> b
t (Ring a -> b
go Ring a
a) (Ring a -> b
go Ring a
b)
    go (Embed a
a) = a -> b
f a
a

-- | Inject an additive term into the free ring.
fromAdditive :: HA.Additive a -> Ring a
fromAdditive :: forall a. Additive a -> Ring a
fromAdditive Additive a
HA.Zero = Ring a
forall a. Ring a
Zero
fromAdditive (HA.Plus Additive a
a Additive a
b) = Ring a -> Ring a -> Ring a
forall a. Ring a -> Ring a -> Ring a
Plus (Additive a -> Ring a
forall a. Additive a -> Ring a
fromAdditive Additive a
a) (Additive a -> Ring a
forall a. Additive a -> Ring a
fromAdditive Additive a
b)
fromAdditive (HA.Embed a
a) = a -> Ring a
forall a. a -> Ring a
Embed a
a

-- | Inject a multiplicative term into the free ring.
fromMultiplicative :: HM.Multiplicative a -> Ring a
fromMultiplicative :: forall a. Multiplicative a -> Ring a
fromMultiplicative Multiplicative a
HM.One = Ring a
forall a. Ring a
One
fromMultiplicative (HM.Times Multiplicative a
a Multiplicative a
b) = Ring a -> Ring a -> Ring a
forall a. Ring a -> Ring a -> Ring a
Times (Multiplicative a -> Ring a
forall a. Multiplicative a -> Ring a
fromMultiplicative Multiplicative a
a) (Multiplicative a -> Ring a
forall a. Multiplicative a -> Ring a
fromMultiplicative Multiplicative a
b)
fromMultiplicative (HM.Embed a
a) = a -> Ring a
forall a. a -> Ring a
Embed a
a

-- | Inject a subtractive term into the free ring.
fromSubtractive :: HS.Subtractive a -> Ring a
fromSubtractive :: forall a. Subtractive a -> Ring a
fromSubtractive Subtractive a
HS.Zero = Ring a
forall a. Ring a
Zero
fromSubtractive (HS.Plus Subtractive a
a Subtractive a
b) = Ring a -> Ring a -> Ring a
forall a. Ring a -> Ring a -> Ring a
Plus (Subtractive a -> Ring a
forall a. Subtractive a -> Ring a
fromSubtractive Subtractive a
a) (Subtractive a -> Ring a
forall a. Subtractive a -> Ring a
fromSubtractive Subtractive a
b)
fromSubtractive (HS.Negate Subtractive a
a) = Ring a -> Ring a
forall a. Ring a -> Ring a
Negate (Subtractive a -> Ring a
forall a. Subtractive a -> Ring a
fromSubtractive Subtractive a
a)
fromSubtractive (HS.Embed a
a) = a -> Ring a
forall a. a -> Ring a
Embed a
a