{-# LANGUAGE UndecidableInstances #-} module Pandora.Paradigm.Primary.Transformer.Reverse where import Pandora.Pattern.Semigroupoid ((.)) import Pandora.Pattern.Category ((<--), (<---), (<----), (<-----)) import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-))) import Pandora.Pattern.Functor.Contravariant (Contravariant ((>-|-))) import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult)) import Pandora.Pattern.Functor.Monoidal (Monoidal (unit)) import Pandora.Pattern.Functor.Traversable (Traversable ((<<-), (<<--))) import Pandora.Pattern.Functor.Distributive (Distributive ((-<<), (--<<))) import Pandora.Pattern.Transformer.Liftable (Liftable (lift)) import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower)) import Pandora.Pattern.Transformer.Hoistable (Hoistable ((/|\))) import Pandora.Paradigm.Primary.Transformer.Backwards (Backwards (Backwards)) import Pandora.Paradigm.Algebraic.Exponential (type (<--), type (-->)) import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:))) import Pandora.Paradigm.Algebraic.Sum ((:+:)) import Pandora.Paradigm.Algebraic.One (One (One)) import Pandora.Paradigm.Algebraic (point, extract, empty, (<-||-)) import Pandora.Pattern.Morphism.Flip (Flip (Flip)) import Pandora.Pattern.Morphism.Straight (Straight (Straight)) import Pandora.Core.Interpreted (Interpreted (Primary, run, unite, (<~), (<~~~))) newtype Reverse t a = Reverse (t a) instance Covariant (->) (->) t => Covariant (->) (->) (Reverse t) where a -> b f <-|- :: (a -> b) -> Reverse t a -> Reverse t b <-|- Reverse t a x = t b -> Reverse t b forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (t b -> Reverse t b) -> t b -> Reverse t b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <---- a -> b f (a -> b) -> t a -> t b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) <-|- t a x instance (Semimonoidal (-->) (:*:) (:*:) t, Covariant (->) (->) t) => Semimonoidal (-->) (:*:) (:*:) (Reverse t) where mult :: (Reverse t a :*: Reverse t b) --> Reverse t (a :*: b) mult = ((Reverse t a :*: Reverse t b) -> Reverse t (a :*: b)) -> (Reverse t a :*: Reverse t b) --> Reverse t (a :*: b) forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (((Reverse t a :*: Reverse t b) -> Reverse t (a :*: b)) -> (Reverse t a :*: Reverse t b) --> Reverse t (a :*: b)) -> ((Reverse t a :*: Reverse t b) -> Reverse t (a :*: b)) -> (Reverse t a :*: Reverse t b) --> Reverse t (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(Reverse t a x :*: Reverse t b y) -> t (a :*: b) -> Reverse t (a :*: b) forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (t (a :*: b) -> Reverse t (a :*: b)) -> t (a :*: b) -> Reverse t (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <---- forall k (p :: * -> * -> *) (source :: * -> * -> *) (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k). Semimonoidal p source target t => p (source (t a) (t b)) (t (target a b)) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Semimonoidal (-->) source target t => source (t a) (t b) --> t (target a b) mult @(-->) ((t a :*: t b) --> t (a :*: b)) -> (t a :*: t b) -> t (a :*: b) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a <~~~ t a x t a -> t b -> t a :*: t b forall s a. s -> a -> s :*: a :*: t b y instance (Covariant (->) (->) t, Monoidal (-->) (-->) (:*:) (:*:) t) => Monoidal (-->) (-->) (:*:) (:*:) (Reverse t) where unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> Reverse t a unit Proxy (:*:) _ = (Straight (->) One a -> Reverse t a) -> Straight (->) (Straight (->) One a) (Reverse t a) forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight ((Straight (->) One a -> Reverse t a) -> Straight (->) (Straight (->) One a) (Reverse t a)) -> (Straight (->) One a -> Reverse t a) -> Straight (->) (Straight (->) One a) (Reverse t a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- t a -> Reverse t a forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (t a -> Reverse t a) -> (Straight (->) One a -> t a) -> Straight (->) One a -> Reverse t a forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> t a forall (t :: * -> *) a. Pointable t => a -> t a point (a -> t a) -> (Straight (->) One a -> a) -> Straight (->) One a -> t a forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (Straight (->) One a -> One -> a forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a <~ One One) instance (Semimonoidal (<--) (:*:) (:*:) t, Covariant (->) (->) t) => Semimonoidal (<--) (:*:) (:*:) (Reverse t) where mult :: (Reverse t a :*: Reverse t b) <-- Reverse t (a :*: b) mult = (Reverse t (a :*: b) -> Reverse t a :*: Reverse t b) -> (Reverse t a :*: Reverse t b) <-- Reverse t (a :*: b) forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip ((Reverse t (a :*: b) -> Reverse t a :*: Reverse t b) -> (Reverse t a :*: Reverse t b) <-- Reverse t (a :*: b)) -> (Reverse t (a :*: b) -> Reverse t a :*: Reverse t b) -> (Reverse t a :*: Reverse t b) <-- Reverse t (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- (t a -> Reverse t a forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (t a -> Reverse t a) -> (t a :*: Reverse t b) -> Reverse t a :*: Reverse t b forall (m :: * -> * -> *) (p :: * -> * -> *) a b c. (Covariant m m (Flip p c), Interpreted m (Flip p c)) => m a b -> m (p a c) (p b c) <-||-) ((t a :*: Reverse t b) -> Reverse t a :*: Reverse t b) -> (Reverse t (a :*: b) -> t a :*: Reverse t b) -> Reverse t (a :*: b) -> Reverse t a :*: Reverse t b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (t b -> Reverse t b forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (t b -> Reverse t b) -> (t a :*: t b) -> t a :*: Reverse t b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) <-|-) ((t a :*: t b) -> t a :*: Reverse t b) -> (Reverse t (a :*: b) -> t a :*: t b) -> Reverse t (a :*: b) -> t a :*: Reverse t b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (forall k (p :: * -> * -> *) (source :: * -> * -> *) (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k). Semimonoidal p source target t => p (source (t a) (t b)) (t (target a b)) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Semimonoidal (<--) source target t => source (t a) (t b) <-- t (target a b) mult @(<--) ((t a :*: t b) <-- t (a :*: b)) -> t (a :*: b) -> t a :*: t b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a <~) (t (a :*: b) -> t a :*: t b) -> (Reverse t (a :*: b) -> t (a :*: b)) -> Reverse t (a :*: b) -> t a :*: t b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . Reverse t (a :*: b) -> t (a :*: b) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run instance (Covariant (->) (->) t, Monoidal (<--) (-->) (:*:) (:*:) t) => Monoidal (<--) (-->) (:*:) (:*:) (Reverse t) where unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- Reverse t a unit Proxy (:*:) _ = (Reverse t a -> Straight (->) One a) -> Flip (->) (Straight (->) One a) (Reverse t a) forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip ((Reverse t a -> Straight (->) One a) -> Flip (->) (Straight (->) One a) (Reverse t a)) -> (Reverse t a -> Straight (->) One a) -> Flip (->) (Straight (->) One a) (Reverse t a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(Reverse t a x) -> (One -> a) -> Straight (->) One a forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (\One _ -> t a -> a forall (t :: * -> *) a. Extractable t => t a -> a extract t a x) instance (Semimonoidal (-->) (:*:) (:+:) t, Covariant (->) (->) t) => Semimonoidal (-->) (:*:) (:+:) (Reverse t) where mult :: (Reverse t a :*: Reverse t b) --> Reverse t (a :+: b) mult = ((Reverse t a :*: Reverse t b) -> Reverse t (a :+: b)) -> (Reverse t a :*: Reverse t b) --> Reverse t (a :+: b) forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (((Reverse t a :*: Reverse t b) -> Reverse t (a :+: b)) -> (Reverse t a :*: Reverse t b) --> Reverse t (a :+: b)) -> ((Reverse t a :*: Reverse t b) -> Reverse t (a :+: b)) -> (Reverse t a :*: Reverse t b) --> Reverse t (a :+: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(Reverse t a x :*: Reverse t b y) -> t (a :+: b) -> Reverse t (a :+: b) forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (t (a :+: b) -> Reverse t (a :+: b)) -> t (a :+: b) -> Reverse t (a :+: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <---- forall k (p :: * -> * -> *) (source :: * -> * -> *) (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k). Semimonoidal p source target t => p (source (t a) (t b)) (t (target a b)) forall (t :: * -> *) a b. Semimonoidal (-->) (:*:) (:+:) t => (t a :*: t b) --> t (a :+: b) mult @(-->) @(:*:) @(:+:) ((t a :*: t b) --> t (a :+: b)) -> (t a :*: t b) -> t (a :+: b) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a <~~~ t a x t a -> t b -> t a :*: t b forall s a. s -> a -> s :*: a :*: t b y instance (Covariant (->) (->) t, Monoidal (-->) (-->) (:*:) (:+:) t) => Monoidal (-->) (-->) (:*:) (:+:) (Reverse t) where unit :: Proxy (:*:) -> (Unit (:+:) --> a) --> Reverse t a unit Proxy (:*:) _ = ((Zero --> a) -> Reverse t a) -> Straight (->) (Zero --> a) (Reverse t a) forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (((Zero --> a) -> Reverse t a) -> Straight (->) (Zero --> a) (Reverse t a)) -> ((Zero --> a) -> Reverse t a) -> Straight (->) (Zero --> a) (Reverse t a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \Zero --> a _ -> t a -> Reverse t a forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse t a forall (t :: * -> *) a. Emptiable t => t a empty instance Traversable (->) (->) t => Traversable (->) (->) (Reverse t) where a -> u b f <<- :: (a -> u b) -> Reverse t a -> u (Reverse t b) <<- Reverse t a x = t b -> Reverse t b forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (t b -> Reverse t b) -> u (t b) -> u (Reverse t b) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) <-|- Backwards u (t b) -> u (t b) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run (u b -> Backwards u b forall k (t :: k -> *) (a :: k). t a -> Backwards t a Backwards (u b -> Backwards u b) -> (a -> u b) -> a -> Backwards u b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> u b f (a -> Backwards u b) -> t a -> Backwards u (t b) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Traversable source target t, Covariant source target u, Monoidal (Straight source) (Straight target) (:*:) (:*:) u) => source a (u b) -> target (t a) (u (t b)) <<-- t a x) instance Distributive (->) (->) t => Distributive (->) (->) (Reverse t) where a -> Reverse t b f -<< :: (a -> Reverse t b) -> u a -> Reverse t (u b) -<< u a x = t (u b) -> Reverse t (u b) forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (t (u b) -> Reverse t (u b)) -> t (u b) -> Reverse t (u b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <--- Reverse t b -> t b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run (Reverse t b -> t b) -> (a -> Reverse t b) -> a -> t b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> Reverse t b f (a -> t b) -> u a -> t (u b) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Distributive source target t, Covariant source target u) => source a (t b) -> target (u a) (t (u b)) -<< u a x instance Contravariant (->) (->) t => Contravariant (->) (->) (Reverse t) where a -> b f >-|- :: (a -> b) -> Reverse t b -> Reverse t a >-|- Reverse t b x = t a -> Reverse t a forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (t a -> Reverse t a) -> t a -> Reverse t a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <---- a -> b f (a -> b) -> t b -> t a forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Contravariant source target t => source a b -> target (t b) (t a) >-|- t b x instance Interpreted (->) (Reverse t) where type Primary (Reverse t) a = t a run :: ((->) < Reverse t a) < Primary (Reverse t) a run ~(Reverse t a x) = t a Primary (Reverse t) a x unite :: ((->) < Primary (Reverse t) a) < Reverse t a unite = ((->) < Primary (Reverse t) a) < Reverse t a forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse instance Liftable (->) Reverse where lift :: u a -> Reverse u a lift = u a -> Reverse u a forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse instance Lowerable (->) Reverse where lower :: Reverse u a -> u a lower = Reverse u a -> u a forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run instance Hoistable (->) Reverse where forall a. u a -> v a f /|\ :: (forall a. u a -> v a) -> forall a. Reverse u a -> Reverse v a /|\ Reverse u a x = v a -> Reverse v a forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (v a -> Reverse v a) -> v a -> Reverse v a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- u a -> v a forall a. u a -> v a f u a x