{-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE UndecidableInstances #-} module Pandora.Paradigm.Structure.Modification.Prefixed where import Pandora.Core.Functor (type (:.), type (:=)) import Pandora.Pattern.Semigroupoid ((.)) import Pandora.Pattern.Category (($)) import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-)), (-<$$>-)) import Pandora.Pattern.Functor.Pointable (Pointable (point)) import Pandora.Pattern.Functor.Traversable (Traversable ((<<-)), (-<<-<<-)) import Pandora.Pattern.Functor.Extractable (extract) import Pandora.Pattern.Object.Monoid (Monoid (zero)) import Pandora.Paradigm.Primary.Algebraic () import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:))) import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite)) import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Into), premorph) import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty) newtype Prefixed t k a = Prefixed (t :. (:*:) k := a) instance Interpreted (Prefixed t k) where type Primary (Prefixed t k) a = t :. (:*:) k := a run :: Prefixed t k a -> Primary (Prefixed t k) a run ~(Prefixed (t :. (:*:) k) := a x) = (t :. (:*:) k) := a Primary (Prefixed t k) a x unite :: Primary (Prefixed t k) a -> Prefixed t k a unite = Primary (Prefixed t k) a -> Prefixed t k a forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a Prefixed instance Covariant t (->) (->) => Covariant (Prefixed t k) (->) (->) where a -> b f -<$>- :: (a -> b) -> Prefixed t k a -> Prefixed t k b -<$>- Prefixed (t :. (:*:) k) := a x = ((t :. (:*:) k) := b) -> Prefixed t k b forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a Prefixed (((t :. (:*:) k) := b) -> Prefixed t k b) -> ((t :. (:*:) k) := b) -> Prefixed t k b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ a -> b f (a -> b) -> ((t :. (:*:) k) := a) -> (t :. (:*:) k) := b forall (t :: * -> *) (u :: * -> *) (category :: * -> * -> *) a b. (Covariant u category category, Covariant t category category) => category a b -> category (t (u a)) (t (u b)) -<$$>- (t :. (:*:) k) := a x instance Traversable t (->) (->) => Traversable (Prefixed t k) (->) (->) where a -> u b f <<- :: (a -> u b) -> Prefixed t k a -> u (Prefixed t k b) <<- Prefixed (t :. (:*:) k) := a x = ((t :. (:*:) k) := b) -> Prefixed t k b forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a Prefixed (((t :. (:*:) k) := b) -> Prefixed t k b) -> u ((t :. (:*:) k) := b) -> u (Prefixed t k b) forall (t :: * -> *) (source :: * -> * -> *) (target :: * -> * -> *) a b. Covariant t source target => source a b -> target (t a) (t b) -<$>- a -> u b f (a -> u b) -> ((t :. (:*:) k) := a) -> u ((t :. (:*:) k) := b) forall (t :: * -> *) (u :: * -> *) (v :: * -> *) (category :: * -> * -> *) a b. (Traversable t category category, Covariant u category category, Pointable u category, Semimonoidal u category (:*:) (:*:), Traversable v category category) => category a (u b) -> category (v (t a)) (u (v (t b))) -<<-<<- (t :. (:*:) k) := a x instance (Monoid k, Pointable t (->)) => Pointable (Prefixed t k) (->) where point :: a -> Prefixed t k a point = ((t :. (:*:) k) := a) -> Prefixed t k a forall (t :: * -> *) k a. ((t :. (:*:) k) := a) -> Prefixed t k a Prefixed (((t :. (:*:) k) := a) -> Prefixed t k a) -> (a -> (t :. (:*:) k) := a) -> a -> Prefixed t k a forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (k :*: a) -> (t :. (:*:) k) := a forall (t :: * -> *) (source :: * -> * -> *) a. Pointable t source => source a (t a) point ((k :*: a) -> (t :. (:*:) k) := a) -> (a -> k :*: a) -> a -> (t :. (:*:) k) := a forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . k -> a -> k :*: a forall s a. s -> a -> s :*: a (:*:) k forall a. Monoid a => a zero instance Covariant t (->) (->) => Morphable (Into t) (Prefixed t k) where type Morphing (Into t) (Prefixed t k) = t morphing :: (<:.>) (Tagged ('Into t)) (Prefixed t k) a -> Morphing ('Into t) (Prefixed t k) a morphing (Prefixed t k a -> t (k :*: a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Prefixed t k a -> t (k :*: a)) -> ((<:.>) (Tagged ('Into t)) (Prefixed t k) a -> Prefixed t k a) -> (<:.>) (Tagged ('Into t)) (Prefixed t k) a -> t (k :*: a) forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (<:.>) (Tagged ('Into t)) (Prefixed t k) a -> Prefixed t k a forall k (mod :: k) (struct :: * -> *). Morphable mod struct => (Tagged mod <:.> struct) ~> struct premorph -> t (k :*: a) prefixed) = forall a. Extractable ((:*:) k) (->) => (k :*: a) -> a forall (t :: * -> *) (source :: * -> * -> *) a. Extractable t source => source (t a) a extract @_ @(->) ((k :*: a) -> a) -> t (k :*: a) -> t a forall (t :: * -> *) (source :: * -> * -> *) (target :: * -> * -> *) a b. Covariant t source target => source a b -> target (t a) (t b) -<$>- t (k :*: a) prefixed type instance Nonempty (Prefixed t k) = Prefixed (Nonempty t) k