module Noether.Algebra.Single.Magma where
import qualified Prelude as P
import Noether.Lemmata.Prelude
import Noether.Lemmata.TypeFu
import Noether.Algebra.Tags
data MagmaE
= MagmaPrim
| MagmaNum
| MagmaNamed Symbol MagmaE
| MagmaTagged Type MagmaE
class MagmaK (op :: k) a (s :: MagmaE) where
binaryOpK :: Proxy op -> Proxy s -> a -> a -> a
instance P.Num a => MagmaK Add a MagmaNum where
binaryOpK _ _ = (P.+)
instance P.Num a => MagmaK Mul a MagmaNum where
binaryOpK _ _ = (P.*)
instance MagmaK And P.Bool MagmaPrim where
binaryOpK _ _ = (P.&&)
instance MagmaK Or P.Bool MagmaPrim where
binaryOpK _ _ = (P.||)
instance MagmaK op a s => MagmaK op a (MagmaNamed sym s) where
binaryOpK o _ = binaryOpK o (Proxy @(MagmaNamed sym s))
instance MagmaK op a s => MagmaK op (i -> a) (MagmaTagged FunctionLift s) where
binaryOpK o _ f g = \x -> f x `binop` g x
where binop = binaryOpK o (Proxy @s)
type Magma op a = MagmaK op a (MagmaS op a)
type family MagmaS (op :: k) (a :: Type) = (r :: MagmaE)