module Pandora.Paradigm.Schemes.T_U where import Pandora.Core.Functor (type (:=)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)), Covariant_ ((-<$>-))) import Pandora.Pattern.Functor.Contravariant (Contravariant ((>$<))) import Pandora.Pattern.Functor.Bivariant (Bivariant ((<->))) import Pandora.Pattern.Functor.Divariant (Divariant ((>->))) import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite, (||=))) newtype T_U ct cu p t u a = T_U (p (t a) (u a)) infixr 2 <:.:>, >:.:>, <:.:<, >:.:< type (<:.:>) t u p = T_U Covariant Covariant p t u type (>:.:>) t u p = T_U Contravariant Covariant p t u type (<:.:<) t u p = T_U Covariant Contravariant p t u type (>:.:<) t u p = T_U Contravariant Contravariant p t u instance Interpreted (T_U ct cu p t u) where type Primary (T_U ct cu p t u) a = p (t a) (u a) run :: T_U ct cu p t u a -> Primary (T_U ct cu p t u) a run ~(T_U p (t a) (u a) x) = p (t a) (u a) Primary (T_U ct cu p t u) a x unite :: Primary (T_U ct cu p t u) a -> T_U ct cu p t u a unite = Primary (T_U ct cu p t u) a -> T_U ct cu p t u a forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *) (t :: k -> k) (u :: k -> k) (a :: k). p (t a) (u a) -> T_U ct cu p t u a T_U instance (forall i . Covariant (p i), Bivariant p (->) (->) (->), Covariant t, Covariant u) => Covariant (t <:.:> u := p) where a -> b f <$> :: (a -> b) -> (:=) (t <:.:> u) p a -> (:=) (t <:.:> u) p b <$> (:=) (t <:.:> u) p a x = (a -> b f (a -> b) -> t a -> t b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$>) (t a -> t b) -> (u a -> u b) -> p (t a) (u a) -> p (t b) (u b) forall (v :: * -> * -> *) (left :: * -> * -> *) (right :: * -> * -> *) (target :: * -> * -> *) a b c d. Bivariant v left right target => left a b -> right c d -> target (v a c) (v b d) <-> (a -> b f (a -> b) -> u a -> u b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$>) (Primary ((t <:.:> u) := p) a -> Primary ((t <:.:> u) := p) b) -> (:=) (t <:.:> u) p a -> (:=) (t <:.:> u) p b forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (Primary t a -> Primary u b) -> t a -> u b ||= (:=) (t <:.:> u) p a x instance (forall i . Covariant_ (p i) (->) (->), Bivariant p (->) (->) (->), Covariant_ t (->) (->), Covariant_ u (->) (->)) => Covariant_ (t <:.:> u := p) (->) (->) where a -> b f -<$>- :: (a -> b) -> (:=) (t <:.:> u) p a -> (:=) (t <:.:> u) p b -<$>- (:=) (t <:.:> u) p a x = (a -> b f (a -> b) -> t a -> t b forall (t :: * -> *) (source :: * -> * -> *) (target :: * -> * -> *) a b. Covariant_ t source target => source a b -> target (t a) (t b) -<$>-) (t a -> t b) -> (u a -> u b) -> p (t a) (u a) -> p (t b) (u b) forall (v :: * -> * -> *) (left :: * -> * -> *) (right :: * -> * -> *) (target :: * -> * -> *) a b c d. Bivariant v left right target => left a b -> right c d -> target (v a c) (v b d) <-> (a -> b f (a -> b) -> u a -> u b forall (t :: * -> *) (source :: * -> * -> *) (target :: * -> * -> *) a b. Covariant_ t source target => source a b -> target (t a) (t b) -<$>-) (Primary ((t <:.:> u) := p) a -> Primary ((t <:.:> u) := p) b) -> (:=) (t <:.:> u) p a -> (:=) (t <:.:> u) p b forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (Primary t a -> Primary u b) -> t a -> u b ||= (:=) (t <:.:> u) p a x instance (Divariant p (->) (->) (->), Contravariant t, Covariant u) => Covariant (t >:.:> u := p) where a -> b f <$> :: (a -> b) -> (:=) (t >:.:> u) p a -> (:=) (t >:.:> u) p b <$> (:=) (t >:.:> u) p a x = (a -> b f (a -> b) -> t b -> t a forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a >$<) (t b -> t a) -> (u a -> u b) -> p (t a) (u a) -> p (t b) (u b) forall (v :: * -> * -> *) (left :: * -> * -> *) (right :: * -> * -> *) (target :: * -> * -> *) a b c d. Divariant v left right target => left a b -> right c d -> target (v b c) (v a d) >-> (a -> b f (a -> b) -> u a -> u b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$>) (Primary ((t >:.:> u) := p) a -> Primary ((t >:.:> u) := p) b) -> (:=) (t >:.:> u) p a -> (:=) (t >:.:> u) p b forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (Primary t a -> Primary u b) -> t a -> u b ||= (:=) (t >:.:> u) p a x instance (forall i . Covariant (p i), Bivariant p (->) (->) (->), Contravariant t, Contravariant u) => Contravariant (t >:.:< u := p) where a -> b f >$< :: (a -> b) -> (:=) (t >:.:< u) p b -> (:=) (t >:.:< u) p a >$< (:=) (t >:.:< u) p b x = (a -> b f (a -> b) -> t b -> t a forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a >$<) (t b -> t a) -> (u b -> u a) -> p (t b) (u b) -> p (t a) (u a) forall (v :: * -> * -> *) (left :: * -> * -> *) (right :: * -> * -> *) (target :: * -> * -> *) a b c d. Bivariant v left right target => left a b -> right c d -> target (v a c) (v b d) <-> (a -> b f (a -> b) -> u b -> u a forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a >$<) (Primary ((t >:.:< u) := p) b -> Primary ((t >:.:< u) := p) a) -> (:=) (t >:.:< u) p b -> (:=) (t >:.:< u) p a forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (Primary t a -> Primary u b) -> t a -> u b ||= (:=) (t >:.:< u) p b x