module Pandora.Paradigm.Primary.Algebraic.Product where import Pandora.Core.Functor (type (:=)) import Pandora.Pattern.Category ((#)) import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-))) import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult)) import Pandora.Pattern.Functor.Extendable (Extendable ((<<=))) import Pandora.Pattern.Object.Setoid (Setoid ((==))) import Pandora.Pattern.Object.Semigroup (Semigroup ((+))) import Pandora.Pattern.Object.Monoid (Monoid (zero)) import Pandora.Pattern.Object.Ringoid (Ringoid ((*))) import Pandora.Pattern.Object.Quasiring (Quasiring (one)) import Pandora.Pattern.Object.Semilattice (Infimum ((/\)), Supremum ((\/))) import Pandora.Pattern.Object.Lattice (Lattice) import Pandora.Pattern.Object.Group (Group (invert)) import Pandora.Paradigm.Primary.Algebraic.Exponential (type (<--), type (-->)) import Pandora.Pattern.Morphism.Flip (Flip (Flip)) import Pandora.Pattern.Morphism.Straight (Straight (Straight)) import Pandora.Paradigm.Controlflow.Effect.Interpreted ((!)) infixr 1 :*: data (:*:) s a = s :*: a instance Covariant (->) (->) ((:*:) s) where a -> b f <-|- :: (a -> b) -> (s :*: a) -> s :*: b <-|- ~(s s :*: a x) = s s s -> b -> s :*: b forall s a. s -> a -> s :*: a :*: a -> b f a x instance Covariant (->) (->) (Flip (:*:) a) where a -> b f <-|- :: (a -> b) -> Flip (:*:) a a -> Flip (:*:) a b <-|- (Flip (a x :*: a y)) = (b :*: a) -> Flip (:*:) a b forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip ((b :*: a) -> Flip (:*:) a b) -> (b :*: a) -> Flip (:*:) a b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) ! a -> b f a x b -> a -> b :*: a forall s a. s -> a -> s :*: a :*: a y instance Extendable (->) ((:*:) s) where (s :*: a) -> b f <<= :: ((s :*: a) -> b) -> (s :*: a) -> s :*: b <<= ~(s s :*: a x) = s s s -> b -> s :*: b forall s a. s -> a -> s :*: a :*: (s :*: a) -> b f (s s s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: a x) instance (Setoid s, Setoid a) => Setoid (s :*: a) where ~(s sx :*: a x) == :: (s :*: a) -> (s :*: a) -> Boolean == ~(s sy :*: a y) = (s sx s -> s -> Boolean forall a. Setoid a => a -> a -> Boolean == s sy) Boolean -> Boolean -> Boolean forall a. Ringoid a => a -> a -> a * (a x a -> a -> Boolean forall a. Setoid a => a -> a -> Boolean == a y) instance (Semigroup s, Semigroup a) => Semigroup (s :*: a) where ~(s sx :*: a x) + :: (s :*: a) -> (s :*: a) -> s :*: a + ~(s sy :*: a y) = s sx s -> s -> s forall a. Semigroup a => a -> a -> a + s sy s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: a x a -> a -> a forall a. Semigroup a => a -> a -> a + a y instance (Monoid s, Monoid a) => Monoid (s :*: a) where zero :: s :*: a zero = s forall a. Monoid a => a zero s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: a forall a. Monoid a => a zero instance (Ringoid s, Ringoid a) => Ringoid (s :*: a) where ~(s sx :*: a x) * :: (s :*: a) -> (s :*: a) -> s :*: a * ~(s sy :*: a y) = s sx s -> s -> s forall a. Ringoid a => a -> a -> a * s sy s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: a x a -> a -> a forall a. Ringoid a => a -> a -> a * a y instance (Quasiring s, Quasiring a) => Quasiring (s :*: a) where one :: s :*: a one = s forall a. Quasiring a => a one s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: a forall a. Quasiring a => a one instance (Infimum s, Infimum a) => Infimum (s :*: a) where ~(s sx :*: a x) /\ :: (s :*: a) -> (s :*: a) -> s :*: a /\ ~(s sy :*: a y) = s sx s -> s -> s forall a. Infimum a => a -> a -> a /\ s sy s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: a x a -> a -> a forall a. Infimum a => a -> a -> a /\ a y instance (Supremum s, Supremum a) => Supremum (s :*: a) where ~(s sx :*: a x) \/ :: (s :*: a) -> (s :*: a) -> s :*: a \/ ~(s sy :*: a y) = s sx s -> s -> s forall a. Supremum a => a -> a -> a \/ s sy s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: a x a -> a -> a forall a. Supremum a => a -> a -> a \/ a y instance (Lattice s, Lattice a) => Lattice (s :*: a) where instance (Group s, Group a) => Group (s :*: a) where invert :: (s :*: a) -> s :*: a invert ~(s s :*: a x) = s -> s forall a. Group a => a -> a invert (s -> s) -> s -> s forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # s s s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: a -> a forall a. Group a => a -> a invert (a -> a) -> a -> a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # a x delta :: a -> a :*: a delta :: a -> a :*: a delta a x = a x a -> a -> a :*: a forall s a. s -> a -> s :*: a :*: a x swap :: a :*: b -> b :*: a swap :: (a :*: b) -> b :*: a swap ~(a x :*: b y) = b y b -> a -> b :*: a forall s a. s -> a -> s :*: a :*: a x attached :: a :*: b -> a attached :: (a :*: b) -> a attached ~(a x :*: b _) = a x