{-# LANGUAGE UndecidableInstances #-} module Pandora.Paradigm.Primary.Transformer.Tap where import Pandora.Core.Functor (type (>>>>>>)) import Pandora.Pattern.Semigroupoid ((.)) import Pandora.Pattern.Category ((<--), (<---), (<----), (<------)) import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--))) import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult)) import Pandora.Pattern.Functor.Monoidal (Monoidal (unit)) import Pandora.Pattern.Functor.Traversable (Traversable ((<-/-))) import Pandora.Pattern.Functor.Extendable (Extendable ((<<=), (<<==))) import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower)) import Pandora.Pattern.Transformer.Hoistable (Hoistable ((/|\))) import Pandora.Core.Interpreted ((<~), (<~~~)) import Pandora.Paradigm.Algebraic ((<-*--), (<-||--), extract) import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), (<:*:>)) import Pandora.Paradigm.Algebraic.Exponential (type (<--), type (-->)) import Pandora.Pattern.Morphism.Flip (Flip (Flip)) import Pandora.Pattern.Morphism.Straight (Straight (Straight)) import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>)) data Tap t a = Tap a (t a) instance Covariant (->) (->) t => Covariant (->) (->) (Tap t) where a -> b f <-|- :: (a -> b) -> Tap t a -> Tap t b <-|- Tap a x t a xs = b -> t b -> Tap t b forall (t :: * -> *) a. a -> t a -> Tap t a Tap (b -> t b -> Tap t b) -> b -> t b -> Tap t b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <---- a -> b f a x (t b -> Tap t b) -> t b -> Tap 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 xs instance Semimonoidal (-->) (:*:) (:*:) t => Semimonoidal (-->) (:*:) (:*:) (Tap t) where mult :: (Tap t a :*: Tap t b) --> Tap t (a :*: b) mult = ((Tap t a :*: Tap t b) -> Tap t (a :*: b)) -> (Tap t a :*: Tap t b) --> Tap t (a :*: b) forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (((Tap t a :*: Tap t b) -> Tap t (a :*: b)) -> (Tap t a :*: Tap t b) --> Tap t (a :*: b)) -> ((Tap t a :*: Tap t b) -> Tap t (a :*: b)) -> (Tap t a :*: Tap t b) --> Tap t (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(Tap a x t a xs :*: Tap b y t b ys) -> (a :*: b) -> t (a :*: b) -> Tap t (a :*: b) forall (t :: * -> *) a. a -> t a -> Tap t a Tap ((a :*: b) -> t (a :*: b) -> Tap t (a :*: b)) -> (a :*: b) -> t (a :*: b) -> Tap t (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <---- a x a -> b -> a :*: b forall s a. s -> a -> s :*: a :*: b y (t (a :*: b) -> Tap t (a :*: b)) -> t (a :*: b) -> Tap 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 xs t a -> t b -> t a :*: t b forall s a. s -> a -> s :*: a :*: t b ys instance Semimonoidal (<--) (:*:) (:*:) t => Semimonoidal (<--) (:*:) (:*:) (Tap t) where mult :: (Tap t a :*: Tap t b) <-- Tap t (a :*: b) mult = (Tap t (a :*: b) -> Tap t a :*: Tap t b) -> (Tap t a :*: Tap t b) <-- Tap t (a :*: b) forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip ((Tap t (a :*: b) -> Tap t a :*: Tap t b) -> (Tap t a :*: Tap t b) <-- Tap t (a :*: b)) -> (Tap t (a :*: b) -> Tap t a :*: Tap t b) -> (Tap t a :*: Tap t b) <-- Tap t (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(Tap (a x :*: b y) t (a :*: b) xys) -> a -> t a -> Tap t a forall (t :: * -> *) a. a -> t a -> Tap t a Tap a x (t a -> Tap t a) -> (t a :*: Tap t b) -> Tap t a :*: Tap 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) <-||-- b -> t b -> Tap t b forall (t :: * -> *) a. a -> t a -> Tap t a Tap b y (t b -> Tap t b) -> (t a :*: t b) -> t a :*: Tap t b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t 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 :*: b) -> t a :*: t b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a <~ t (a :*: b) xys instance Semimonoidal (<--) (:*:) (:*:) t => Monoidal (<--) (-->) (:*:) (:*:) (Tap t) where unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- Tap t a unit Proxy (:*:) _ = (Tap t a -> Straight (->) One a) -> Flip (->) (Straight (->) One a) (Tap t a) forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip ((Tap t a -> Straight (->) One a) -> Flip (->) (Straight (->) One a) (Tap t a)) -> (Tap t a -> Straight (->) One a) -> Flip (->) (Straight (->) One a) (Tap t a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(Tap a x t a _) -> (One -> a) -> Straight (->) One a forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (\One _ -> a x) instance Traversable (->) (->) t => Traversable (->) (->) (Tap t) where a -> u b f <-/- :: (a -> u b) -> Tap t a -> u (Tap t b) <-/- Tap a x t a xs = b -> t b -> Tap t b forall (t :: * -> *) a. a -> t a -> Tap t a Tap (b -> t b -> Tap t b) -> u b -> u (t b -> Tap t b) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) <-|-- a -> u b f a x u (t b -> Tap t b) -> u (t b) -> u (Tap t b) forall (t :: * -> *) a b. (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => t (a -> b) -> t a -> t b <-*-- a -> u b f (a -> u b) -> t a -> 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 xs instance (Semimonoidal (<--) (:*:) (:*:) t, Extendable (->) t, Covariant (->) (->) t) => Extendable (->) (Tap t) where Tap t a -> b f <<= :: (Tap t a -> b) -> Tap t a -> Tap t b <<= Tap t a x = b -> t b -> Tap t b forall (t :: * -> *) a. a -> t a -> Tap t a Tap (b -> t b -> Tap t b) -> b -> t b -> Tap t b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <--- Tap t a -> b f Tap t a x (t b -> Tap t b) -> t b -> Tap t b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <--- Tap t a -> b f (Tap t a -> b) -> (t a -> Tap t a) -> t a -> b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> t a -> Tap t a forall (t :: * -> *) a. a -> t a -> Tap t a Tap (Tap t a -> a forall (t :: * -> *) a. Extractable t => t a -> a extract Tap t a x) (t a -> b) -> t a -> t b forall (source :: * -> * -> *) (t :: * -> *) a b. Extendable source t => source (t a) b -> source (t a) (t b) <<= Tap t a -> t a forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *) a. (Lowerable cat t, Covariant cat cat u) => cat (t u a) (u a) lower Tap t a x instance Lowerable (->) Tap where lower :: Tap u a -> u a lower (Tap a _ u a xs) = u a xs instance Hoistable (->) Tap where forall a. u a -> v a f /|\ :: (forall a. u a -> v a) -> forall a. Tap u a -> Tap v a /|\ Tap a x u a xs = a -> v a -> Tap v a forall (t :: * -> *) a. a -> t a -> Tap t a Tap a x (v a -> Tap v a) -> v a -> Tap 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 xs instance {-# OVERLAPS #-} Semimonoidal (-->) (:*:) (:*:) t => Semimonoidal (-->) (:*:) (:*:) (Tap (t <:.:> t >>>>>> (:*:))) where mult :: (Tap ((t <:.:> t) >>>>>> (:*:)) a :*: Tap ((t <:.:> t) >>>>>> (:*:)) b) --> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b) mult = ((Tap ((t <:.:> t) >>>>>> (:*:)) a :*: Tap ((t <:.:> t) >>>>>> (:*:)) b) -> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b)) -> (Tap ((t <:.:> t) >>>>>> (:*:)) a :*: Tap ((t <:.:> t) >>>>>> (:*:)) b) --> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b) forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (((Tap ((t <:.:> t) >>>>>> (:*:)) a :*: Tap ((t <:.:> t) >>>>>> (:*:)) b) -> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b)) -> (Tap ((t <:.:> t) >>>>>> (:*:)) a :*: Tap ((t <:.:> t) >>>>>> (:*:)) b) --> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b)) -> ((Tap ((t <:.:> t) >>>>>> (:*:)) a :*: Tap ((t <:.:> t) >>>>>> (:*:)) b) -> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b)) -> (Tap ((t <:.:> t) >>>>>> (:*:)) a :*: Tap ((t <:.:> t) >>>>>> (:*:)) b) --> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(Tap a x (T_U (t a xls :*: t a xrs)) :*: Tap b y (T_U (t b yls :*: t b yrs))) -> (a :*: b) -> (>>>>>>) (t <:.:> t) (:*:) (a :*: b) -> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b) forall (t :: * -> *) a. a -> t a -> Tap t a Tap (a x a -> b -> a :*: b forall s a. s -> a -> s :*: a :*: b y) ((>>>>>>) (t <:.:> t) (:*:) (a :*: b) -> Tap ((t <:.:> t) >>>>>> (:*:)) (a :*: b)) -> (>>>>>>) (t <:.:> t) (:*:) (a :*: b) -> Tap ((t <:.:> 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 xls t a -> t b -> t a :*: t b forall s a. s -> a -> s :*: a :*: t b yls) t (a :*: b) -> t (a :*: b) -> (>>>>>>) (t <:.:> t) (:*:) (a :*: b) forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (t <:*:> u) >>>>>> a <:*:> (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 xrs t a -> t b -> t a :*: t b forall s a. s -> a -> s :*: a :*: t b yrs)