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)) 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 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