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