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 (multiply_)) import Pandora.Pattern.Functor.Extractable (Extractable (extract)) import Pandora.Pattern.Functor.Extendable (Extendable ((<<=))) import Pandora.Pattern.Functor.Comonad (Comonad) import Pandora.Pattern.Functor.Bivariant (Bivariant ((<->))) 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.Transformer.Flip (Flip (Flip)) import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>)) infixr 0 :*: data (:*:) s a = s :*: a instance Covariant ((:*:) s) (->) (->) where a -> b f -<$>- :: (a -> b) -> (s :*: a) -> s :*: b -<$>- s :*: a x = (s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a x s -> b -> s :*: b forall s a. s -> a -> s :*: a :*: a -> b f (a -> b) -> a -> b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: 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 :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ a -> b f a x b -> a -> b :*: a forall s a. s -> a -> s :*: a :*: a y instance Extractable ((:*:) a) (->) where extract :: (a :*: a) -> a extract ~(a _ :*: a y) = a y instance Extendable ((:*:) s) (->) where (s :*: a) -> b f <<= :: ((s :*: a) -> b) -> (s :*: a) -> s :*: b <<= s :*: a x = (s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a x s -> b -> s :*: b forall s a. s -> a -> s :*: a :*: (s :*: a) -> b f ((s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a x s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: a x) instance Comonad ((:*:) s) (->) where instance Bivariant (:*:) (->) (->) (->) where a -> b f <-> :: (a -> b) -> (c -> d) -> (a :*: c) -> b :*: d <-> c -> d g = \ ~(a s :*: c x) -> a -> b f a s b -> d -> b :*: d forall s a. s -> a -> s :*: a :*: c -> d g c x instance (Setoid s, Setoid a) => Setoid (s :*: a) where s :*: a x == :: (s :*: a) -> (s :*: a) -> Boolean == s :*: a y = ((s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a x s -> s -> Boolean forall a. Setoid a => a -> a -> Boolean == (s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a y) Boolean -> Boolean -> Boolean forall a. Ringoid a => a -> a -> a * ((s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: a x a -> a -> Boolean forall a. Setoid a => a -> a -> Boolean == (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: a y) instance (Semigroup s, Semigroup a) => Semigroup (s :*: a) where s :*: a x + :: (s :*: a) -> (s :*: a) -> s :*: a + s :*: a y = (s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a x s -> s -> s forall a. Semigroup a => a -> a -> a + (s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a y s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: a x a -> a -> a forall a. Semigroup a => a -> a -> a + (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: 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 :*: a x * :: (s :*: a) -> (s :*: a) -> s :*: a * s :*: a y = (s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a x s -> s -> s forall a. Ringoid a => a -> a -> a * (s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a y s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: a x a -> a -> a forall a. Ringoid a => a -> a -> a * (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: 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 :*: a x /\ :: (s :*: a) -> (s :*: a) -> s :*: a /\ s :*: a y = (s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a x s -> s -> s forall a. Infimum a => a -> a -> a /\ (s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a y s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: a x a -> a -> a forall a. Infimum a => a -> a -> a /\ (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: a y instance (Supremum s, Supremum a) => Supremum (s :*: a) where s :*: a x \/ :: (s :*: a) -> (s :*: a) -> s :*: a \/ s :*: a y = (s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a x s -> s -> s forall a. Supremum a => a -> a -> a \/ (s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a y s -> a -> s :*: a forall s a. s -> a -> s :*: a :*: (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: a x a -> a -> a forall a. Supremum a => a -> a -> a \/ (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: 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 :*: 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 :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a x 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) # (s :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract s :*: a x instance {-# OVERLAPS #-} Semimonoidal t (->) (:*:) (:*:) => Semimonoidal (t <:.:> t := (:*:)) (->) (:*:) (:*:) where multiply_ :: ((:=) (t <:.:> t) (:*:) a :*: (:=) (t <:.:> t) (:*:) b) -> (:=) (t <:.:> t) (:*:) (a :*: b) multiply_ (T_U (t a xls :*: t a xrs) :*: T_U (t b yls :*: t b yrs)) = (t (a :*: b) :*: t (a :*: b)) -> (:=) (t <:.:> t) (:*:) (a :*: b) forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *) (t :: k -> k) (u :: k -> k) (a :: k). p (t a) (u a) -> T_U ct cu p t u a T_U ((t (a :*: b) :*: t (a :*: b)) -> (:=) (t <:.:> t) (:*:) (a :*: b)) -> (t (a :*: b) :*: t (a :*: b)) -> (:=) (t <:.:> t) (:*:) (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ (t a :*: t b) -> t (a :*: b) forall k (t :: k -> *) (p :: * -> * -> *) (source :: * -> * -> *) (target :: k -> k -> k) (a :: k) (b :: k). Semimonoidal t p source target => p (source (t a) (t b)) (t (target a b)) multiply_ (t a xls t a -> t b -> t a :*: t b forall s a. s -> a -> s :*: a :*: t b yls) t (a :*: b) -> t (a :*: b) -> t (a :*: b) :*: t (a :*: b) forall s a. s -> a -> s :*: a :*: (t a :*: t b) -> t (a :*: b) forall k (t :: k -> *) (p :: * -> * -> *) (source :: * -> * -> *) (target :: k -> k -> k) (a :: k) (b :: k). Semimonoidal t p source target => p (source (t a) (t b)) (t (target a b)) multiply_ (t a xrs t a -> t b -> t a :*: t b forall s a. s -> a -> s :*: a :*: t b yrs) 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 twosome :: t a -> u a -> (<:.:>) t u (:*:) a twosome :: t a -> u a -> (<:.:>) t u (:*:) a twosome t a x u a y = (t a :*: u a) -> (<:.:>) t u (:*:) a forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *) (t :: k -> k) (u :: k -> k) (a :: k). p (t a) (u a) -> T_U ct cu p t u a T_U ((t a :*: u a) -> (<:.:>) t u (:*:) a) -> (t a :*: u a) -> (<:.:>) t u (:*:) a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ t a x t a -> u a -> t a :*: u a forall s a. s -> a -> s :*: a :*: u a y