module Pandora.Paradigm.Primary.Algebraic.Product where

import Pandora.Core.Functor (type (:=))
import Pandora.Core.Appliable ((!))
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.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.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
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
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 :: * -> * -> *) 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 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 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
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

instance {-# OVERLAPS #-} Semimonoidal (-->) (:*:) (:*:) t => Semimonoidal (-->) (:*:) (:*:) (t <:.:> t := (:*:)) where
	mult :: ((:=) (t <:.:> t) (:*:) a :*: (:=) (t <:.:> t) (:*:) b)
--> (:=) (t <:.:> t) (:*:) (a :*: b)
mult = (((:=) (t <:.:> t) (:*:) a :*: (:=) (t <:.:> t) (:*:) b)
 -> (:=) (t <:.:> t) (:*:) (a :*: b))
-> ((:=) (t <:.:> t) (:*:) a :*: (:=) (t <:.:> t) (:*:) b)
   --> (:=) (t <:.:> t) (:*:) (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((((:=) (t <:.:> t) (:*:) a :*: (:=) (t <:.:> t) (:*:) b)
  -> (:=) (t <:.:> t) (:*:) (a :*: b))
 -> ((:=) (t <:.:> t) (:*:) a :*: (:=) (t <:.:> t) (:*:) b)
    --> (:=) (t <:.:> t) (:*:) (a :*: b))
-> (((:=) (t <:.:> t) (:*:) a :*: (:=) (t <:.:> t) (:*:) b)
    -> (:=) (t <:.:> t) (:*:) (a :*: b))
-> ((:=) (t <:.:> t) (:*:) a :*: (:=) (t <:.:> t) (:*:) b)
   --> (:=) (t <:.:> t) (:*:) (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(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)
$ (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((t a :*: t b) --> t (a :*: b)) -> (t a :*: t b) -> t (a :*: b)
forall k k k k (m :: k -> k -> *) (a :: k) (b :: k)
       (n :: k -> k -> *) (c :: k) (d :: k).
Appliable m a b n c d =>
m a b -> n c d
!) (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
:*: (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (-->) source target t =>
source (t a) (t b) --> t (target a b)
mult @(-->) ((t a :*: t b) --> t (a :*: b)) -> (t a :*: t b) -> t (a :*: b)
forall k k k k (m :: k -> k -> *) (a :: k) (b :: k)
       (n :: k -> k -> *) (c :: k) (d :: k).
Appliable m a b n c d =>
m a b -> n c d
!) (t a
xrs t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
yrs)

-- TODO: Generalize (:*:) as Bivariant p
instance (Semimonoidal (<--) (:*:) (:*:) t, Semimonoidal (<--) (:*:) (:*:) u) => Semimonoidal (<--) (:*:) (:*:) (t <:.:> u := (:*:)) where
	mult :: ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
<-- (:=) (t <:.:> u) (:*:) (a :*: b)
mult = ((:=) (t <:.:> u) (:*:) (a :*: b)
 -> (:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
-> ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
   <-- (:=) (t <:.:> u) (:*:) (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((:=) (t <:.:> u) (:*:) (a :*: b)
  -> (:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
 -> ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
    <-- (:=) (t <:.:> u) (:*:) (a :*: b))
-> ((:=) (t <:.:> u) (:*:) (a :*: b)
    -> (:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
-> ((:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b)
   <-- (:=) (t <:.:> u) (:*:) (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(T_U t (a :*: b) :*: u (a :*: b)
lrxys) ->
		-- TODO: I need matrix transposing here
		let ((t a
lxs :*: t b
lys) :*: (u a
rxs :*: u b
rys)) = ((forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (<--) source target t =>
source (t a) (t b) <-- t (target a b)
mult @(<--) ((t a :*: t b) <-- t (a :*: b)) -> t (a :*: b) -> t a :*: t b
forall k k k k (m :: k -> k -> *) (a :: k) (b :: k)
       (n :: k -> k -> *) (c :: k) (d :: k).
Appliable m a b n c d =>
m a b -> n c d
!) (t (a :*: b) -> t a :*: t b)
-> (u (a :*: b) -> u a :*: u b)
-> (t (a :*: b) :*: u (a :*: b))
-> (t a :*: t b) :*: (u a :*: u b)
forall (left :: * -> * -> *) (right :: * -> * -> *)
       (target :: * -> * -> *) (v :: * -> * -> *) a b c d.
Bivariant left right target v =>
left a b -> right c d -> target (v a c) (v b d)
<-> (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (<--) source target t =>
source (t a) (t b) <-- t (target a b)
mult @(<--) ((u a :*: u b) <-- u (a :*: b)) -> u (a :*: b) -> u a :*: u b
forall k k k k (m :: k -> k -> *) (a :: k) (b :: k)
       (n :: k -> k -> *) (c :: k) (d :: k).
Appliable m a b n c d =>
m a b -> n c d
!)) t (a :*: b) :*: u (a :*: b)
lrxys in
		(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
lxs t a -> u a -> t a :*: u a
forall s a. s -> a -> s :*: a
:*: u a
rxs) (:=) (t <:.:> u) (:*:) a
-> (:=) (t <:.:> u) (:*:) b
-> (:=) (t <:.:> u) (:*:) a :*: (:=) (t <:.:> u) (:*:) b
forall s a. s -> a -> s :*: a
:*: (t b :*: u b) -> (:=) (t <:.:> u) (:*:) 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
lys t b -> u b -> t b :*: u b
forall s a. s -> a -> s :*: a
:*: u b
rys)

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