{-# 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 (multiply)) import Pandora.Pattern.Functor.Monoidal (Monoidal (unit)) import Pandora.Pattern.Functor.Traversable (Traversable ((<<-))) import Pandora.Pattern.Functor.Distributive (Distributive ((-<<))) import Pandora.Pattern.Functor.Bivariant ((<->)) 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.Primary.Algebraic.Exponential (type (<--)) import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:))) import Pandora.Paradigm.Primary.Algebraic.One (One (One)) import Pandora.Paradigm.Primary.Algebraic (point, extract) import Pandora.Paradigm.Primary.Transformer.Flip (Flip (Flip)) import Pandora.Paradigm.Controlflow.Effect.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 multiply :: (Reverse t a :*: Reverse t b) -> Reverse t (a :*: b) multiply (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) # (t a :*: t b) -> t (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)) multiply (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 (:*:) _ Unit (:*:) -> a f = t a -> Reverse t a forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (t a -> Reverse t a) -> (a -> t a) -> 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. Monoidal (->) (->) (:*:) (:*:) t => a -> t a point (a -> Reverse t a) -> a -> Reverse t a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ Unit (:*:) -> a f One Unit (:*:) One instance (Semimonoidal (<--) (:*:) (:*:) t, Covariant (->) (->) t) => Semimonoidal (<--) (:*:) (:*:) (Reverse t) where multiply :: (Reverse t a :*: Reverse t b) <-- Reverse t (a :*: b) multiply = (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) $ \(Reverse t (a :*: b) x) -> let Flip t (a :*: b) -> t a :*: t b f = 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) multiply @(<--) @(:*:) @(:*:) in (t a -> Reverse t a forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse (t a -> Reverse t a) -> (t b -> Reverse t b) -> (t a :*: t b) -> Reverse t a :*: Reverse t b forall (left :: * -> * -> *) (right :: * -> * -> *) (target :: * -> * -> *) (v :: * -> * -> *) a b c d. Bivariant left right target v => left a b -> right c d -> target (v a c) (v b d) <-> t b -> Reverse t b forall k (t :: k -> *) (a :: k). t a -> Reverse t a Reverse) ((t a :*: t b) -> Reverse t a :*: Reverse t b) -> (t a :*: t b) -> Reverse t a :*: Reverse t b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ t (a :*: b) -> t a :*: t b forall a b. t (a :*: b) -> t a :*: t b f t (a :*: b) x instance (Covariant (->) (->) t, Monoidal (<--) (->) (:*:) (:*:) t) => Monoidal (<--) (->) (:*:) (:*:) (Reverse t) where unit :: Proxy (:*:) -> (Unit (:*:) -> a) <-- Reverse t a unit Proxy (:*:) _ = (Reverse t a -> One -> a) -> Flip (->) (One -> a) (Reverse t a) forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip ((Reverse t a -> One -> a) -> Flip (->) (One -> a) (Reverse t a)) -> (Reverse t a -> One -> a) -> Flip (->) (One -> a) (Reverse t a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ \(Reverse t a x) -> (\One _ -> t a -> a forall (t :: * -> *) a. Extractable_ t => t a -> a extract t a x) 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) -> Primary (Backwards u) (t b) forall (t :: * -> *) a. Interpreted t => 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 source 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 (t :: * -> *) a. Interpreted t => 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 (t :: * -> *) a. Interpreted t => t a -> Primary t a run instance Hoistable Reverse where u ~> v f /|\ :: (u ~> v) -> Reverse u ~> Reverse v /|\ 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 u ~> v f u a x