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