module Pandora.Paradigm.Schemes.UT where

import Pandora.Core.Functor (type (:.), type (:=), type (~>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category (($), identity)
import Pandora.Pattern.Functor.Covariant (Covariant, Covariant ((-<$>-)), (-<$$>-))
import Pandora.Pattern.Functor.Contravariant (Contravariant)
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (multiply))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)))
import Pandora.Pattern.Functor.Bivariant ((<->))
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (<--))
import Pandora.Paradigm.Primary.Algebraic.One (One (One))
import Pandora.Paradigm.Primary.Algebraic ((:*:) ((:*:)), point, extract)
import Pandora.Paradigm.Primary.Transformer.Flip (Flip (Flip))

newtype UT ct cu t u a = UT (u :. t := a)

infixr 3 <.:>, >.:>, <.:<, >.:<

type (<.:>) = UT Covariant Covariant
type (>.:>) = UT Contravariant Covariant
type (<.:<) = UT Covariant Contravariant
type (>.:<) = UT Contravariant Contravariant

instance Interpreted (UT ct cu t u) where
	type Primary (UT ct cu t u) a = u :. t := a
	run :: UT ct cu t u a -> Primary (UT ct cu t u) a
run ~(UT (u :. t) := a
x) = (u :. t) := a
Primary (UT ct cu t u) a
x
	unite :: Primary (UT ct cu t u) a -> UT ct cu t u a
unite = Primary (UT ct cu t u) a -> UT ct cu t u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT

instance (Covariant (->) (->) t, Covariant (->) (->) u) => Covariant (->) (->) (t <.:> u) where
	a -> b
f -<$>- :: (a -> b) -> (<.:>) t u a -> (<.:>) t u b
-<$>- (<.:>) t u a
x = ((u :. t) := b) -> (<.:>) t u b
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := b) -> (<.:>) t u b)
-> ((u :. t) := b) -> (<.:>) t u b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> b
f (a -> b) -> u (t a) -> (u :. t) := b
forall (t :: * -> *) (u :: * -> *) (category :: * -> * -> *) a b.
(Covariant category category u, Covariant category category t) =>
category a b -> category (t (u a)) (t (u b))
-<$$>- (<.:>) t u a -> Primary (t <.:> u) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<.:>) t u a
x

instance (Covariant (->) (->) u, Semimonoidal (->) (:*:) (:*:) t, Semimonoidal (->) (:*:) (:*:) u) => Semimonoidal (->) (:*:) (:*:) (t <.:> u) where
	multiply :: ((<.:>) t u a :*: (<.:>) t u b) -> (<.:>) t u (a :*: b)
multiply (UT (u :. t) := a
x :*: UT (u :. t) := b
y) = ((u :. t) := (a :*: b)) -> (<.:>) t u (a :*: b)
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := (a :*: b)) -> (<.:>) t u (a :*: b))
-> ((u :. t) := (a :*: b)) -> (<.:>) t u (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 (target :: * -> * -> *) (t :: * -> *) a b.
Semimonoidal (->) (:*:) target t =>
(t a :*: t b) -> t (target a b)
multiply @(->) @(:*:) ((t a :*: t b) -> t (a :*: b))
-> u (t a :*: t b) -> (u :. t) := (a :*: b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- (((u :. t) := a) :*: ((u :. t) := b)) -> u (t a :*: t 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))
multiply ((u :. t) := a
x ((u :. t) := a)
-> ((u :. t) := b) -> ((u :. t) := a) :*: ((u :. t) := b)
forall s a. s -> a -> s :*: a
:*: (u :. t) := b
y)

instance (Covariant (->) (->) t, Covariant (->) (->) u, Semimonoidal (->) (:*:) (:*:) u, Monoidal (->) (->) (:*:) (:*:) t, Monoidal (->) (->) (:*:) (:*:) u) => Monoidal (->) (->) (:*:) (:*:) (t <.:> u) where
	unit :: Proxy (:*:) -> (Unit (:*:) -> a) -> (<.:>) t u a
unit Proxy (:*:)
_ Unit (:*:) -> a
f = ((u :. t) := a) -> (<.:>) t u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := a) -> (<.:>) t u a)
-> (a -> (u :. t) := a) -> a -> (<.:>) t u a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. t a -> (u :. t) := a
forall (t :: * -> *) a.
Monoidal (->) (->) (:*:) (:*:) t =>
a -> t a
point (t a -> (u :. t) := a) -> (a -> t a) -> a -> (u :. t) := a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> t a
forall (t :: * -> *) a.
Monoidal (->) (->) (:*:) (:*:) t =>
a -> t a
point (a -> (<.:>) t u a) -> a -> (<.:>) t u a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Unit (:*:) -> a
f One
Unit (:*:)
One

instance (Traversable (->) (->) t, Bindable (->) t, Semimonoidal (->) (:*:) (:*:) u, Monoidal (->) (->) (:*:) (:*:) u, Bindable (->) u) => Bindable (->) (t <.:> u) where
	a -> (<.:>) t u b
f =<< :: (a -> (<.:>) t u b) -> (<.:>) t u a -> (<.:>) t u b
=<< UT (u :. t) := a
x = ((u :. t) := b) -> (<.:>) t u b
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := b) -> (<.:>) t u b)
-> ((u :. t) := b) -> (<.:>) t u b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ ((t b -> t b
forall (m :: * -> * -> *) a. Category m => m a a
identity (t b -> t b) -> t (t b) -> t b
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<<) (t (t b) -> t b) -> u (t (t b)) -> (u :. t) := b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>-) (u (t (t b)) -> (u :. t) := b)
-> (t a -> u (t (t b))) -> t a -> (u :. t) := b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((<.:>) t u b -> (u :. t) := b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<.:>) t u b -> (u :. t) := b)
-> (a -> (<.:>) t u b) -> a -> (u :. t) := b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> (<.:>) t u b
f (a -> (u :. t) := b) -> t a -> u (t (t b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal source target (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<-) (t a -> (u :. t) := b) -> ((u :. t) := a) -> (u :. t) := b
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< (u :. t) := a
x

instance (Covariant (->) (->) u, Semimonoidal (<--) (:*:) (:*:) t, Semimonoidal (<--) (:*:) (:*:) u) => Semimonoidal (<--) (:*:) (:*:) (t <.:> u) where
	multiply :: ((<.:>) t u a :*: (<.:>) t u b) <-- (<.:>) t u (a :*: b)
multiply = ((<.:>) 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)
$ \(UT (u :. t) := (a :*: b)
xys) ->
		let Flip u (a :*: b) -> u a :*: u b
f = 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 (t :: * -> *) a b.
Semimonoidal (<--) (:*:) (:*:) t =>
(t a :*: t b) <-- t (a :*: b)
multiply @(<--) @(:*:) @(:*:) in
		let Flip t (a :*: b) -> t a :*: t b
g = 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 (t :: * -> *) a b.
Semimonoidal (<--) (:*:) (:*:) t =>
(t a :*: t b) <-- t (a :*: b)
multiply @(<--) @(:*:) @(:*:) in
		(((u :. t) := a) -> (<.:>) t u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := a) -> (<.:>) t u a)
-> (u (t b) -> (<.:>) t u b)
-> (((u :. t) := a) :*: u (t b))
-> (<.:>) t u a :*: (<.:>) t 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)
<-> u (t b) -> (<.:>) t u b
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT) ((((u :. t) := a) :*: u (t b)) -> (<.:>) t u a :*: (<.:>) t u b)
-> (((u :. t) := a) :*: u (t b)) -> (<.:>) t u a :*: (<.:>) t u b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ u (t a :*: t b) -> ((u :. t) := a) :*: u (t b)
forall a b. u (a :*: b) -> u a :*: u b
f (t (a :*: b) -> t a :*: t b
forall a b. t (a :*: b) -> t a :*: t b
g (t (a :*: b) -> t a :*: t b)
-> ((u :. t) := (a :*: b)) -> u (t a :*: t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- (u :. t) := (a :*: b)
xys) where

instance (Covariant (->) (->) u, Monoidal (<--) (->) (:*:) (:*:) t, Monoidal (<--) (->) (:*:) (:*:) u) => Monoidal (<--) (->) (:*:) (:*:) (t <.:> u) where
	unit :: Proxy (:*:) -> (Unit (:*:) -> a) <-- (<.:>) t u a
unit Proxy (:*:)
_ = ((<.:>) t u a -> One -> a) -> Flip (->) (One -> a) ((<.:>) t u a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip (((<.:>) t u a -> One -> a) -> Flip (->) (One -> a) ((<.:>) t u a))
-> ((<.:>) t u a -> One -> a)
-> Flip (->) (One -> a) ((<.:>) t u a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(UT (u :. t) := a
x) -> (\One
_ -> t a -> a
forall (t :: * -> *) a. Extractable_ t => t a -> a
extract (t a -> a) -> t a -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ ((u :. t) := a) -> t a
forall (t :: * -> *) a. Extractable_ t => t a -> a
extract (u :. t) := a
x)

instance Monoidal (->) (->) (:*:) (:*:) t => Liftable (->) (UT Covariant Covariant t) where
	lift :: Covariant (->) (->) u => u ~> t <.:> u
	lift :: u ~> (t <.:> u)
lift u a
x = ((u :. t) := a) -> UT Covariant Covariant t u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) := a) -> UT ct cu t u a
UT (((u :. t) := a) -> UT Covariant Covariant t u a)
-> ((u :. t) := a) -> UT Covariant Covariant t u a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> t a
forall (t :: * -> *) a.
Monoidal (->) (->) (:*:) (:*:) t =>
a -> t a
point (a -> t a) -> u a -> (u :. t) := a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- u a
x

instance Monoidal (<--) (->) (:*:) (:*:) t => Lowerable (->) (UT Covariant Covariant t) where
	lower :: Covariant (->) (->) u => t <.:> u ~> u
	lower :: (t <.:> u) ~> u
lower (UT (u :. t) := a
x) = t a -> a
forall (t :: * -> *) a. Extractable_ t => t a -> a
extract (t a -> a) -> ((u :. t) := a) -> u a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>- (u :. t) := a
x