module Pandora.Paradigm.Schemes.T_U where

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Functor.Covariant (Covariant, Covariant ((-<$>-)))
import Pandora.Pattern.Functor.Contravariant (Contravariant, Contravariant ((->$<-)))
import Pandora.Pattern.Functor.Bivariant (Bivariant ((<->)))
import Pandora.Pattern.Functor.Divariant (Divariant ((>->)))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite, (||=)))

newtype T_U ct cu p t u a = T_U (p (t a) (u a))

infixr 2 <:.:>, >:.:>, <:.:<, >:.:<

type (<:.:>) t u p = T_U Covariant Covariant p t u
type (>:.:>) t u p = T_U Contravariant Covariant p t u
type (<:.:<) t u p = T_U Covariant Contravariant p t u
type (>:.:<) t u p = T_U Contravariant Contravariant p t u

instance Interpreted (T_U ct cu p t u) where
	type Primary (T_U ct cu p t u) a = p (t a) (u a)
	run :: T_U ct cu p t u a -> Primary (T_U ct cu p t u) a
run ~(T_U p (t a) (u a)
x) = p (t a) (u a)
Primary (T_U ct cu p t u) a
x
	unite :: Primary (T_U ct cu p t u) a -> T_U ct cu p t u a
unite = Primary (T_U ct cu p t u) a -> T_U ct cu p 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

instance (forall i . Covariant (->) (->) (p i), Bivariant (->) (->) (->) p,  Covariant (->) (->) t, Covariant (->) (->) u) => Covariant (->) (->) (t <:.:> u := p) where
	a -> b
f -<$>- :: (a -> b) -> (:=) (t <:.:> u) p a -> (:=) (t <:.:> u) p b
-<$>- (:=) (t <:.:> u) p a
x = (a -> b
f (a -> b) -> t a -> t b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>-) (t a -> t b) -> (u a -> u b) -> p (t a) (u a) -> p (t b) (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)
<-> (a -> b
f (a -> b) -> u a -> u b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>-) (Primary ((t <:.:> u) := p) a -> Primary ((t <:.:> u) := p) b)
-> (:=) (t <:.:> u) p a -> (:=) (t <:.:> u) p b
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= (:=) (t <:.:> u) p a
x

instance (Divariant (->) (->) (->) p, Contravariant (->) (->) t, Covariant (->) (->) u) => Covariant (->) (->) (t >:.:> u := p) where
	a -> b
f -<$>- :: (a -> b) -> (:=) (t >:.:> u) p a -> (:=) (t >:.:> u) p b
-<$>- (:=) (t >:.:> u) p a
x = (a -> b
f (a -> b) -> t b -> t a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
->$<-) (t b -> t a) -> (u a -> u b) -> p (t a) (u a) -> p (t b) (u b)
forall (left :: * -> * -> *) (right :: * -> * -> *)
       (target :: * -> * -> *) (v :: * -> * -> *) a b c d.
Divariant left right target v =>
left a b -> right c d -> target (v b c) (v a d)
>-> (a -> b
f (a -> b) -> u a -> u b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
-<$>-) (Primary ((t >:.:> u) := p) a -> Primary ((t >:.:> u) := p) b)
-> (:=) (t >:.:> u) p a -> (:=) (t >:.:> u) p b
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= (:=) (t >:.:> u) p a
x

instance (forall i . Covariant (->) (->) (p i), Bivariant (->) (->) (->) p, Contravariant (->) (->) t, Contravariant (->) (->) u) => Contravariant (->) (->) (t >:.:< u := p) where
	a -> b
f ->$<- :: (a -> b) -> (:=) (t >:.:< u) p b -> (:=) (t >:.:< u) p a
->$<- (:=) (t >:.:< u) p b
x = (a -> b
f (a -> b) -> t b -> t a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
->$<-) (t b -> t a) -> (u b -> u a) -> p (t b) (u b) -> p (t a) (u a)
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)
<-> (a -> b
f (a -> b) -> u b -> u a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
->$<-) (Primary ((t >:.:< u) := p) b -> Primary ((t >:.:< u) := p) a)
-> (:=) (t >:.:< u) p b -> (:=) (t >:.:< u) p a
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= (:=) (t >:.:< u) p b
x