module Pandora.Paradigm.Primary.Functor.Product where import Pandora.Core.Functor (type (:=)) import Pandora.Pattern.Category (($), (#)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>))) import Pandora.Pattern.Functor.Applicative (Applicative ((<*>))) import Pandora.Pattern.Functor.Extractable (Extractable (extract)) import Pandora.Pattern.Functor.Traversable (Traversable ((->>))) 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.Schemes.T_U (T_U (T_U), type (<:.:>)) infixr 0 :*: data Product s a = s :*: a type (:*:) = Product instance Covariant (Product s) where a -> b f <$> :: (a -> b) -> Product s a -> Product s b <$> Product s a x = Product s a -> s forall a b. (a :*: b) -> a attached Product s a x s -> b -> Product s b forall s a. s -> a -> Product s a :*: a -> b f (a -> b) -> a -> b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t extract Product s a x instance Extractable (Product a) where extract :: a <:= Product a extract ~(a _ :*: a y) = a y instance Traversable (Product s) where Product s a x ->> :: Product s a -> (a -> u b) -> (u :. Product s) := b ->> a -> u b f = (Product s a -> s forall a b. (a :*: b) -> a attached Product s a x s -> b -> Product s b forall s a. s -> a -> Product s a :*:) (b -> Product s b) -> u b -> (u :. Product s) := b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> a -> u b f (a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t extract Product s a x) instance Extendable (Product s) where Product s a x =>> :: Product s a -> (Product s a -> b) -> Product s b =>> Product s a -> b f = Product s a -> s forall a b. (a :*: b) -> a attached Product s a x s -> b -> Product s b forall s a. s -> a -> Product s a :*: Product s a -> b f (Product s a -> s forall a b. (a :*: b) -> a attached Product s a x s -> a -> Product s a forall s a. s -> a -> Product s a :*: a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t extract Product s a x) instance Comonad (Product s) where instance Bivariant Product where a -> b f <-> :: (a -> b) -> (c -> d) -> Product a c -> Product b d <-> c -> d g = \ ~(a s :*: c x) -> a -> b f a s b -> d -> Product b d forall s a. s -> a -> Product 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 * (a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t extract s :*: a x a -> a -> Boolean forall a. Setoid a => a -> a -> Boolean == a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t 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 -> Product s a :*: a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t extract s :*: a x a -> a -> a forall a. Semigroup a => a -> a -> a + a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t 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 -> Product 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 -> Product s a :*: a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t extract s :*: a x a -> a -> a forall a. Ringoid a => a -> a -> a * a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t 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 -> Product 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 -> Product s a :*: a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t extract s :*: a x a -> a -> a forall a. Infimum a => a -> a -> a /\ a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t 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 -> Product s a :*: a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t extract s :*: a x a -> a -> a forall a. Supremum a => a -> a -> a \/ a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t 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 -> Product 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 <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t extract s :*: a x instance {-# OVERLAPS #-} Applicative t => Applicative (t <:.:> t := (:*:)) where T_U (t (a -> b) lfs :*: t (a -> b) rfs) <*> :: (:=) (t <:.:> t) Product (a -> b) -> (:=) (t <:.:> t) Product a -> (:=) (t <:.:> t) Product b <*> T_U (t a ls :*: t a rs) = (t b :*: t b) -> (:=) (t <:.:> t) Product 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 b :*: t b) -> (:=) (t <:.:> t) Product b) -> (t b :*: t b) -> (:=) (t <:.:> t) Product b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ t (a -> b) lfs t (a -> b) -> t a -> t b forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b <*> t a ls t b -> t b -> t b :*: t b forall s a. s -> a -> Product s a :*: t (a -> b) rfs t (a -> b) -> t a -> t b forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b <*> t a rs delta :: a -> a :*: a delta :: a -> a :*: a delta a x = a x a -> a -> a :*: a forall s a. s -> a -> Product 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 -> Product 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 Product a twosome t a x u a y = (t a :*: u a) -> (<:.:>) t u Product 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 Product a) -> (t a :*: u a) -> (<:.:>) t u Product 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 -> Product s a :*: u a y