module Pandora.Paradigm.Schemes.UT where

import Pandora.Core.Functor (type (:.), type (:=), type (~>))
import Pandora.Core.Appliable ((!))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category (($), identity)
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)), (<$$>))
import Pandora.Pattern.Functor.Contravariant (Contravariant)
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
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 (<--), type (-->))
import Pandora.Paradigm.Primary.Algebraic.One (One (One))
import Pandora.Paradigm.Primary.Algebraic ((:*:) ((:*:)), point, extract)
import Pandora.Pattern.Morphism.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 m m t, Covariant m m u, Interpreted m (t <.:> u)) => Covariant m m (t <.:> u) where
	<$> :: m a b -> m ((<.:>) t u a) ((<.:>) t u b)
(<$>) m a b
f = m (Primary (t <.:> u) a) (Primary (t <.:> u) b)
-> m ((<.:>) t u a) ((<.:>) t u b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
(||=) (m a b -> m (u (t a)) (u (t b))
forall (source :: * -> * -> *) (between :: * -> * -> *)
       (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Covariant source between u, Covariant between target t) =>
source a b -> target (t (u a)) (t (u b))
(<$$>) @m @m m a b
f)

instance (Covariant (->) (->) u, Semimonoidal (-->) (:*:) (:*:) t, Semimonoidal (-->) (:*:) (:*:) u) => Semimonoidal (-->) (:*:) (:*:) (t <.:> u) where
	mult :: ((<.:>) t u a :*: (<.:>) t u b) --> (<.:>) t u (a :*: b)
mult = (((<.:>) t u a :*: (<.:>) t u b) -> (<.:>) t u (a :*: b))
-> ((<.:>) t u a :*: (<.:>) t u b) --> (<.:>) t u (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((((<.:>) t u a :*: (<.:>) t u b) -> (<.:>) t u (a :*: b))
 -> ((<.:>) t u a :*: (<.:>) t u b) --> (<.:>) t u (a :*: b))
-> (((<.:>) t u a :*: (<.:>) t u b) -> (<.:>) t u (a :*: b))
-> ((<.:>) t u a :*: (<.:>) t u b) --> (<.:>) t u (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ ((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))
-> (((<.:>) t u a :*: (<.:>) t u b) -> (u :. t) := (a :*: b))
-> ((<.:>) t u a :*: (<.:>) t u b)
-> (<.:>) t u (a :*: b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((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)
(<$>) (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
!) (u (t a :*: t b) -> (u :. t) := (a :*: b))
-> (((<.:>) t u a :*: (<.:>) t u b) -> u (t a :*: t b))
-> ((<.:>) t u a :*: (<.:>) t u b)
-> (u :. t) := (a :*: b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (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 :. t) := a) :*: ((u :. t) := b)) --> u (t a :*: t b))
-> (((u :. t) := a) :*: ((u :. t) := b)) -> u (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
!) ((((u :. t) := a) :*: ((u :. t) := b)) -> u (t a :*: t b))
-> (((<.:>) t u a :*: (<.:>) t u b)
    -> ((u :. t) := a) :*: ((u :. t) := b))
-> ((<.:>) t u a :*: (<.:>) t u b)
-> u (t a :*: t b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (forall (t :: * -> *) a. Interpreted (->) t => t a -> Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run @(->) ((<.:>) t u a -> (u :. t) := a)
-> ((<.:>) t u b -> (u :. t) := b)
-> ((<.:>) t u a :*: (<.:>) t u b)
-> ((u :. t) := a) :*: ((u :. t) := 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 (t :: * -> *) a. Interpreted (->) t => t a -> Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run @(->))

instance (Covariant (->) (->) t, Covariant (->) (->) u, Semimonoidal (-->) (:*:) (:*:) u, Monoidal (-->) (->) (:*:) (:*:) t, Monoidal (-->) (->) (:*:) (:*:) u) => Monoidal (-->) (->) (:*:) (:*:) (t <.:> u) where
	unit :: Proxy (:*:) -> (Unit (:*:) -> a) --> (<.:>) t u a
unit Proxy (:*:)
_ = ((One -> a) -> (<.:>) t u a)
-> Straight (->) (One -> a) ((<.:>) t u a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((One -> a) -> (<.:>) t u a)
 -> Straight (->) (One -> a) ((<.:>) t u a))
-> ((One -> a) -> (<.:>) t u a)
-> Straight (->) (One -> a) ((<.:>) t u a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ ((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)
-> ((One -> a) -> (u :. t) := a) -> (One -> 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. Pointable t => a -> t a
point (t a -> (u :. t) := a)
-> ((One -> a) -> t a) -> (One -> 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. Pointable t => a -> t a
point (a -> t a) -> ((One -> a) -> a) -> (One -> a) -> t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((One -> a) -> One -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ One
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 (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (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 (Straight 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
	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)
$ \(UT (u :. t) := (a :*: b)
xys) -> (((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 :*: t b) -> ((u :. t) := a) :*: ((u :. t) := b))
-> u (t a :*: t b)
-> (<.:>) t u a :*: (<.:>) t u b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (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 :. t) := a) :*: ((u :. t) := b)) <-- u (t a :*: t b))
-> u (t a :*: t b) -> ((u :. t) := a) :*: ((u :. 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
!) (u (t a :*: t b) -> (<.:>) t u a :*: (<.:>) t u b)
-> u (t a :*: t b) -> (<.:>) t u a :*: (<.:>) t u 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 :*: 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 :. 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

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. Pointable 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