{-# LANGUAGE NoRebindableSyntax #-}

-- | Free abelian group — the initial encoding of 'Subtractive'.
module NumHask.Free.Subtractive
  ( Subtractive (..),
    zero,
    plus,
    negate,
    minus,
    embed,
    lift,
    normalize,
    eval,
    foldSubtractive,
  )
where

import NumHask.Algebra.Additive qualified as NH
import Prelude (Eq, Show, otherwise, (==))

-- | Free abelian group over a carrier type.
--
-- The initial encoding of 'NumHask.Algebra.Subtractive.Subtractive'.
-- Extends the free commutative monoid with an antipode.
data Subtractive a
  = Zero
  | Plus (Subtractive a) (Subtractive a)
  | Negate (Subtractive a)
  | Embed a
  deriving (Subtractive a -> Subtractive a -> Bool
(Subtractive a -> Subtractive a -> Bool)
-> (Subtractive a -> Subtractive a -> Bool) -> Eq (Subtractive a)
forall a. Eq a => Subtractive a -> Subtractive a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Subtractive a -> Subtractive a -> Bool
== :: Subtractive a -> Subtractive a -> Bool
$c/= :: forall a. Eq a => Subtractive a -> Subtractive a -> Bool
/= :: Subtractive a -> Subtractive a -> Bool
Eq, Int -> Subtractive a -> ShowS
[Subtractive a] -> ShowS
Subtractive a -> String
(Int -> Subtractive a -> ShowS)
-> (Subtractive a -> String)
-> ([Subtractive a] -> ShowS)
-> Show (Subtractive a)
forall a. Show a => Int -> Subtractive a -> ShowS
forall a. Show a => [Subtractive a] -> ShowS
forall a. Show a => Subtractive a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Subtractive a -> ShowS
showsPrec :: Int -> Subtractive a -> ShowS
$cshow :: forall a. Show a => Subtractive a -> String
show :: Subtractive a -> String
$cshowList :: forall a. Show a => [Subtractive a] -> ShowS
showList :: [Subtractive a] -> ShowS
Show)

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

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

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

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

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

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

-- | Lift a carrier value, absorbing the additive identity.
--
-- >>> lift 0
-- Zero
lift :: (Eq a, NH.Subtractive a) => a -> Subtractive a
lift :: forall a. (Eq a, Subtractive a) => a -> Subtractive a
lift a
a
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Additive a => a
NH.zero = Subtractive a
forall a. Subtractive a
Zero
  | Bool
otherwise = a -> Subtractive a
forall a. a -> Subtractive a
Embed a
a

-- | Normalize a term with respect to abelian-group laws: identity
-- absorption, antipode involution, and additive-inverse cancellation.
--
-- >>> normalize (plus (embed 3) (negate (embed 3)))
-- Zero
normalize :: (Eq a, NH.Subtractive a) => Subtractive a -> Subtractive a
normalize :: forall a. (Eq a, Subtractive a) => Subtractive a -> Subtractive a
normalize Subtractive a
Zero = Subtractive a
forall a. Subtractive a
Zero
normalize (Embed a
a)
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Additive a => a
NH.zero = Subtractive a
forall a. Subtractive a
Zero
  | Bool
otherwise = a -> Subtractive a
forall a. a -> Subtractive a
Embed a
a
normalize (Negate Subtractive a
a) = Subtractive a -> Subtractive a
forall a. Subtractive a -> Subtractive a
negate (Subtractive a -> Subtractive a
forall a. (Eq a, Subtractive a) => Subtractive a -> Subtractive a
normalize Subtractive a
a)
normalize (Plus Subtractive a
a Subtractive a
b) =
  case (Subtractive a -> Subtractive a
forall a. (Eq a, Subtractive a) => Subtractive a -> Subtractive a
normalize Subtractive a
a, Subtractive a -> Subtractive a
forall a. (Eq a, Subtractive a) => Subtractive a -> Subtractive a
normalize Subtractive a
b) of
    (Subtractive a
Zero, Subtractive a
x) -> Subtractive a
x
    (Subtractive a
x, Subtractive a
Zero) -> Subtractive a
x
    (Subtractive a
x, Negate Subtractive a
y)
      | Subtractive a
x Subtractive a -> Subtractive a -> Bool
forall a. Eq a => a -> a -> Bool
== Subtractive a
y -> Subtractive a
forall a. Subtractive a
Zero
      | Bool
otherwise -> Subtractive a -> Subtractive a -> Subtractive a
forall a. Subtractive a -> Subtractive a -> Subtractive a
Plus Subtractive a
x (Subtractive a -> Subtractive a
forall a. Subtractive a -> Subtractive a
Negate Subtractive a
y)
    (Negate Subtractive a
x, Subtractive a
y)
      | Subtractive a
x Subtractive a -> Subtractive a -> Bool
forall a. Eq a => a -> a -> Bool
== Subtractive a
y -> Subtractive a
forall a. Subtractive a
Zero
      | Bool
otherwise -> Subtractive a -> Subtractive a -> Subtractive a
forall a. Subtractive a -> Subtractive a -> Subtractive a
Plus (Subtractive a -> Subtractive a
forall a. Subtractive a -> Subtractive a
Negate Subtractive a
x) Subtractive a
y
    (Subtractive a
x, Subtractive a
y) -> Subtractive a -> Subtractive a -> Subtractive a
forall a. Subtractive a -> Subtractive a -> Subtractive a
Plus Subtractive a
x Subtractive a
y

-- | Evaluate a term into any 'NumHask.Algebra.Additive.Subtractive'.
--
-- This is the unique homomorphism out of the free abelian group.
eval :: (NH.Subtractive a) => Subtractive a -> a
eval :: forall a. Subtractive a => Subtractive a -> a
eval Subtractive a
Zero = a
forall a. Additive a => a
NH.zero
eval (Plus Subtractive a
a Subtractive a
b) = Subtractive a -> a
forall a. Subtractive a => Subtractive a -> a
eval Subtractive a
a a -> a -> a
forall a. Additive a => a -> a -> a
NH.+ Subtractive a -> a
forall a. Subtractive a => Subtractive a -> a
eval Subtractive a
b
eval (Negate Subtractive a
a) = a -> a
forall a. Subtractive a => a -> a
NH.negate (Subtractive a -> a
forall a. Subtractive a => Subtractive a -> a
eval Subtractive a
a)
eval (Embed a
a) = a
a

-- | Universal property: fold with a target abelian group.
foldSubtractive :: b -> (b -> b -> b) -> (b -> b) -> (a -> b) -> Subtractive a -> b
foldSubtractive :: forall b a.
b -> (b -> b -> b) -> (b -> b) -> (a -> b) -> Subtractive a -> b
foldSubtractive b
z b -> b -> b
p b -> b
n a -> b
f = Subtractive a -> b
go
  where
    go :: Subtractive a -> b
go Subtractive a
Zero = b
z
    go (Plus Subtractive a
a Subtractive a
b) = b -> b -> b
p (Subtractive a -> b
go Subtractive a
a) (Subtractive a -> b
go Subtractive a
b)
    go (Negate Subtractive a
a) = b -> b
n (Subtractive a -> b
go Subtractive a
a)
    go (Embed a
a) = a -> b
f a
a