module Pandora.Paradigm.Schemes.T_U where

import Pandora.Core.Functor (type (~>))
import Pandora.Pattern.Category (($))
import Pandora.Pattern.Functor.Covariant (Covariant)
import Pandora.Pattern.Functor.Contravariant (Contravariant)
import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable (hoist))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite))

newtype T_U ct cu t u a = T_U (t a :*: u a)

type (<:*:>) = T_U Covariant Covariant
type (>:*:>) = T_U Contravariant Covariant
type (<:*:<) = T_U Covariant Contravariant
type (>:*:<) = T_U Contravariant Contravariant

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

instance Avoidable t => Liftable (T_U Covariant Covariant t) where
	lift :: Covariant u => u ~> t <:*:> u
	lift :: u ~> (t <:*:> u)
lift u a
x = (t a :*: u a) -> T_U Covariant Covariant t u a
forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *)
       (a :: k).
(t a :*: u a) -> T_U ct cu t u a
T_U ((t a :*: u a) -> T_U Covariant Covariant t u a)
-> (t a :*: u a) -> T_U Covariant Covariant t u a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ t a
forall (t :: * -> *) a. Avoidable t => t a
empty t a -> u a -> t a :*: u a
forall s a. s -> a -> Product s a
:*: u a
x

instance Lowerable (T_U Covariant Covariant t) where
	lower :: t <:*:> u ~> u
	lower :: (<:*:>) t u a -> u a
lower ~(T_U (t a
_ :*: u a
y)) = u a
y

instance Covariant t => Hoistable (T_U Covariant Covariant t) where
	hoist :: u ~> v -> (t <:*:> u ~> t <:*:> v)
	hoist :: (u ~> v) -> (t <:*:> u) ~> (t <:*:> v)
hoist u ~> v
f (T_U (t a
x :*: u a
y)) = (t a :*: v a) -> T_U Covariant Covariant t v a
forall k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> *)
       (a :: k).
(t a :*: u a) -> T_U ct cu t u a
T_U ((t a :*: v a) -> T_U Covariant Covariant t v a)
-> (t a :*: v a) -> T_U Covariant Covariant t v a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ t a
x t a -> v a -> t a :*: v a
forall s a. s -> a -> Product s a
:*: u a -> v a
u ~> v
f u a
y