module Pandora.Paradigm.Schemes.TU where import Pandora.Core.Functor (type (:.), type (:=), type (~>)) import Pandora.Pattern.Category ((.), ($)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>))) import Pandora.Pattern.Functor.Contravariant (Contravariant) import Pandora.Pattern.Functor.Pointable (Pointable (point)) import Pandora.Pattern.Functor.Extractable (Extractable (extract)) import Pandora.Pattern.Transformer.Liftable (Liftable (lift)) import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower)) import Pandora.Pattern.Transformer.Hoistable (Hoistable (hoist)) import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run)) newtype TU ct cu t u a = TU (t :. u := a) type (<:.>) = TU Covariant Covariant type (>:.>) = TU Contravariant Covariant type (<:.<) = TU Covariant Contravariant type (>:.<) = TU Contravariant Contravariant instance Interpreted (TU ct cu t u) where type Primary (TU ct cu t u) a = t :. u := a run :: TU ct cu t u a -> Primary (TU ct cu t u) a run ~(TU (t :. u) := a x) = (t :. u) := a Primary (TU ct cu t u) a x instance Pointable t => Liftable (TU Covariant Covariant t) where lift :: Covariant u => u ~> t <:.> u lift :: u ~> (t <:.> u) lift = ((t :. u) := a) -> TU Covariant Covariant t u a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((t :. u) := a) -> TU Covariant Covariant t u a) -> (u a -> (t :. u) := a) -> u a -> TU Covariant Covariant t u a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . u a -> (t :. u) := a forall (t :: * -> *) a. Pointable t => a |-> t point instance Extractable t => Lowerable (TU Covariant Covariant t) where lower :: t <:.> u ~> u lower :: (<:.>) t u a -> u a lower (TU (t :. u) := a x) = u a <-| t forall (t :: * -> *) a. Extractable t => a <-| t extract (t :. u) := a x instance Covariant t => Hoistable (TU Covariant Covariant t) where hoist :: u ~> v -> (t <:.> u ~> t <:.> v) hoist :: (u ~> v) -> (t <:.> u) ~> (t <:.> v) hoist u ~> v f (TU (t :. u) := a x) = ((t :. v) := a) -> TU Covariant Covariant t v a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((t :. v) := a) -> TU Covariant Covariant t v a) -> ((t :. v) := a) -> TU 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 -> v a) -> ((t :. u) := a) -> (t :. v) := a forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> (t :. u) := a x