module Pandora.Paradigm.Schemes.U_T 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 U_T ct cu t u a = U_T (u a :*: t a)

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

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

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

instance Lowerable (U_T Covariant Covariant t) where
	lower :: t <.:.> u ~> u
	lower :: (<.:.>) t u a -> u a
lower (U_T (u a
x :*: t a
_)) = u a
x

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