module Pandora.Paradigm.Schemes.T_U where

import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.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 t p u a = T_U (p (t a) (u a))

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

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

instance (Bivariant p, Covariant t, Covariant u)
	=> Covariant (T_U Covariant Covariant t p u) where
		a -> b
f <$> :: (a -> b)
-> T_U Covariant Covariant t p u a
-> T_U Covariant Covariant t p u b
<$> T_U Covariant Covariant t p u a
x = ((a -> b
f (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (t a -> t b) -> (u a -> u b) -> p (t a) (u a) -> p (t b) (u b)
forall (v :: * -> * -> *) a b c d.
Bivariant v =>
(a -> b) -> (c -> d) -> v a c -> v b d
<-> (a -> b
f (a -> b) -> u a -> u b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>)) (Primary (T_U Covariant Covariant t p u) a
 -> Primary (T_U Covariant Covariant t p u) b)
-> T_U Covariant Covariant t p u a
-> T_U Covariant Covariant t p u b
forall (t :: * -> *) a b.
Interpreted t =>
(Primary t a -> Primary t b) -> t a -> t b
||= T_U Covariant Covariant t p u a
x

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