{-# LANGUAGE NoRebindableSyntax #-}

-- | Free commutative monoid — the initial encoding of 'Additive'.
module NumHask.Free.Additive
  ( Additive (..),
    zero,
    plus,
    embed,
    lift,
    normalize,
    eval,
    foldAdditive,
    flatten,
  )
where

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

-- | Free commutative monoid over a carrier type.
--
-- The initial encoding of 'NumHask.Algebra.Additive.Additive'.
-- Terms are built from 'zero', 'plus', and 'embed'.
--
-- Use smart constructors 'zero' and 'plus' for identity-normalised
-- terms. 'eval' projects into any target monoid satisfying the
-- 'NumHask.Algebra.Additive.Additive' laws.
data Additive a
  = Zero
  | Plus (Additive a) (Additive a)
  | Embed a
  deriving (Additive a -> Additive a -> Bool
(Additive a -> Additive a -> Bool)
-> (Additive a -> Additive a -> Bool) -> Eq (Additive a)
forall a. Eq a => Additive a -> Additive a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Additive a -> Additive a -> Bool
== :: Additive a -> Additive a -> Bool
$c/= :: forall a. Eq a => Additive a -> Additive a -> Bool
/= :: Additive a -> Additive a -> Bool
Eq, Int -> Additive a -> ShowS
[Additive a] -> ShowS
Additive a -> String
(Int -> Additive a -> ShowS)
-> (Additive a -> String)
-> ([Additive a] -> ShowS)
-> Show (Additive a)
forall a. Show a => Int -> Additive a -> ShowS
forall a. Show a => [Additive a] -> ShowS
forall a. Show a => Additive a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Additive a -> ShowS
showsPrec :: Int -> Additive a -> ShowS
$cshow :: forall a. Show a => Additive a -> String
show :: Additive a -> String
$cshowList :: forall a. Show a => [Additive a] -> ShowS
showList :: [Additive a] -> ShowS
Show)

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

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

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

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

-- | Normalize a term with respect to additive-monoid laws.
--
-- >>> normalize (embed 0)
-- Zero
normalize :: (Eq a, NH.Additive a) => Additive a -> Additive a
normalize :: forall a. (Eq a, Additive a) => Additive a -> Additive a
normalize Additive a
Zero = Additive a
forall a. Additive 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 = Additive a
forall a. Additive a
Zero
  | Bool
otherwise = a -> Additive a
forall a. a -> Additive a
Embed a
a
normalize (Plus Additive a
a Additive a
b) = Additive a -> Additive a -> Additive a
forall a. Additive a -> Additive a -> Additive a
plus (Additive a -> Additive a
forall a. (Eq a, Additive a) => Additive a -> Additive a
normalize Additive a
a) (Additive a -> Additive a
forall a. (Eq a, Additive a) => Additive a -> Additive a
normalize Additive a
b)

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

-- | Evaluate a term into any 'NumHask.Algebra.Additive.Additive'.
--
-- This is the unique homomorphism out of the free commutative monoid.
--
-- >>> eval (plus (embed 1) (embed 2))
-- 3
eval :: (NH.Additive a) => Additive a -> a
eval :: forall a. Additive a => Additive a -> a
eval Additive a
Zero = a
forall a. Additive a => a
NH.zero
eval (Plus Additive a
a Additive a
b) = Additive a -> a
forall a. Additive a => Additive a -> a
eval Additive a
a a -> a -> a
forall a. Additive a => a -> a -> a
NH.+ Additive a -> a
forall a. Additive a => Additive a -> a
eval Additive a
b
eval (Embed a
a) = a
a

-- | Universal property: fold with a target monoid.
--
-- > foldAdditive z p f . embed == f
-- > foldAdditive z p f zero   == z
-- > foldAdditive z p f (plus a b) == p (foldAdditive z p f a) (foldAdditive z p f b)
foldAdditive :: b -> (b -> b -> b) -> (a -> b) -> Additive a -> b
foldAdditive :: forall b a. b -> (b -> b -> b) -> (a -> b) -> Additive a -> b
foldAdditive b
z b -> b -> b
p a -> b
f = Additive a -> b
go
  where
    go :: Additive a -> b
go Additive a
Zero = b
z
    go (Plus Additive a
a Additive a
b) = b -> b -> b
p (Additive a -> b
go Additive a
a) (Additive a -> b
go Additive a
b)
    go (Embed a
a) = a -> b
f a
a

-- | Flatten a term to a list of embedded generators, discarding
-- identities.  This is the bag-of-generators view of the free
-- commutative monoid; commutativity is not enforced structurally.
flatten :: Additive a -> [a]
flatten :: forall a. Additive a -> [a]
flatten = [a] -> ([a] -> [a] -> [a]) -> (a -> [a]) -> Additive a -> [a]
forall b a. b -> (b -> b -> b) -> (a -> b) -> Additive a -> b
foldAdditive [] [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(P.++) (a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [])