module Pandora.Paradigm.Primary.Functor.Product where import Pandora.Pattern.Functor.Covariant (Covariant ((<$>))) 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)) infixr 1 :*: 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 <:= 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 :*: 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 <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t extract s :*: a x) 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