{-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE UndecidableInstances #-} module Pandora.Paradigm.Structure.Modification.Comprehension where import Pandora.Core.Functor (type (:=)) import Pandora.Pattern.Semigroupoid ((.)) import Pandora.Pattern.Category (($)) import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-))) import Pandora.Pattern.Functor.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.Bindable (Bindable ((=<<))) import Pandora.Pattern.Transformer.Liftable (lift) import Pandora.Pattern.Object.Semigroup (Semigroup ((+))) import Pandora.Pattern.Object.Monoid (Monoid (zero)) import Pandora.Pattern.Object.Setoid (Setoid ((==))) import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity)) import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct)) import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite)) import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>)) import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>)) import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Push), premorph) import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null)) import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:))) import Pandora.Paradigm.Primary.Algebraic.Sum ((:+:)) import Pandora.Paradigm.Primary.Algebraic (empty) newtype Comprehension t a = Comprehension (t <:.> Construction t := a) instance Interpreted (Comprehension t) where type Primary (Comprehension t) a = t <:.> Construction t := a run :: Comprehension t a -> Primary (Comprehension t) a run ~(Comprehension (t <:.> Construction t) := a x) = Primary (Comprehension t) a (t <:.> Construction t) := a x unite :: Primary (Comprehension t) a -> Comprehension t a unite = Primary (Comprehension t) a -> Comprehension t a forall (t :: * -> *) a. ((t <:.> Construction t) := a) -> Comprehension t a Comprehension instance Covariant (->) (->) (t <:.> Construction t) => Covariant (->) (->) (Comprehension t) where a -> b f -<$>- :: (a -> b) -> Comprehension t a -> Comprehension t b -<$>- Comprehension (t <:.> Construction t) := a x = ((t <:.> Construction t) := b) -> Comprehension t b forall (t :: * -> *) a. ((t <:.> Construction t) := a) -> Comprehension t a Comprehension (((t <:.> Construction t) := b) -> Comprehension t b) -> ((t <:.> Construction t) := b) -> Comprehension t b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ a -> b f (a -> b) -> ((t <:.> Construction t) := a) -> (t <:.> Construction t) := b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) -<$>- (t <:.> Construction t) := a x instance Traversable (->) (->) (t <:.> Construction t) => Traversable (->) (->) (Comprehension t) where a -> u b f <<- :: (a -> u b) -> Comprehension t a -> u (Comprehension t b) <<- Comprehension (t <:.> Construction t) := a x = ((t <:.> Construction t) := b) -> Comprehension t b forall (t :: * -> *) a. ((t <:.> Construction t) := a) -> Comprehension t a Comprehension (((t <:.> Construction t) := b) -> Comprehension t b) -> u ((t <:.> Construction t) := b) -> u (Comprehension 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 -> u b) -> ((t <:.> Construction t) := a) -> u ((t <:.> Construction 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 <:.> Construction t) := a x instance (Covariant (->) (->) t, Semimonoidal (->) (:*:) (:*:) t) => Semimonoidal (->) (:*:) (:*:) (Comprehension t) where multiply :: (Comprehension t a :*: Comprehension t b) -> Comprehension t (a :*: b) multiply (Comprehension (t <:.> Construction t) := a x :*: Comprehension (t <:.> Construction t) := b y) = ((t <:.> Construction t) := (a :*: b)) -> Comprehension t (a :*: b) forall (t :: * -> *) a. ((t <:.> Construction t) := a) -> Comprehension t a Comprehension (((t <:.> Construction t) := (a :*: b)) -> Comprehension t (a :*: b)) -> ((t <:.> Construction t) := (a :*: b)) -> Comprehension t (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ (((t <:.> Construction t) := a) :*: ((t <:.> Construction t) := b)) -> (t <:.> Construction 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 <:.> Construction t) := a x ((t <:.> Construction t) := a) -> ((t <:.> Construction t) := b) -> ((t <:.> Construction t) := a) :*: ((t <:.> Construction t) := b) forall s a. s -> a -> s :*: a :*: (t <:.> Construction t) := b y) instance (Covariant (->) (->) t, Semimonoidal (->) (:*:) (:+:) t) => Semimonoidal (->) (:*:) (:+:) (Comprehension t) where multiply :: (Comprehension t a :*: Comprehension t b) -> Comprehension t (a :+: b) multiply (Comprehension (t <:.> Construction t) := a x :*: Comprehension (t <:.> Construction t) := b y) = ((t <:.> Construction t) := (a :+: b)) -> Comprehension t (a :+: b) forall (t :: * -> *) a. ((t <:.> Construction t) := a) -> Comprehension t a Comprehension (((t <:.> Construction t) := (a :+: b)) -> Comprehension t (a :+: b)) -> ((t <:.> Construction t) := (a :+: b)) -> Comprehension t (a :+: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ (((t <:.> Construction t) := a) :*: ((t <:.> Construction t) := b)) -> (t <:.> Construction 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 <:.> Construction t) := a x ((t <:.> Construction t) := a) -> ((t <:.> Construction t) := b) -> ((t <:.> Construction t) := a) :*: ((t <:.> Construction t) := b) forall s a. s -> a -> s :*: a :*: (t <:.> Construction t) := b y) instance (Covariant (->) (->) t, Monoidal (->) (->) (:*:) (:+:) t) => Monoidal (->) (->) (:*:) (:+:) (Comprehension t) where unit :: Proxy (:*:) -> (Unit (:+:) -> a) -> Comprehension t a unit Proxy (:*:) _ Unit (:+:) -> a _ = ((t <:.> Construction t) := a) -> Comprehension t a forall (t :: * -> *) a. ((t <:.> Construction t) := a) -> Comprehension t a Comprehension (t <:.> Construction t) := a forall (t :: * -> *) a. Monoidal (->) (->) (:*:) (:+:) t => t a empty instance (forall a . Semigroup (t <:.> Construction t := a), Bindable (->) t) => Bindable (->) (Comprehension t) where a -> Comprehension t b f =<< :: (a -> Comprehension t b) -> Comprehension t a -> Comprehension t b =<< Comprehension (TU (t :. Construction t) := a t) = ((t <:.> Construction t) := b) -> Comprehension t b forall (t :: * -> *) a. ((t <:.> Construction t) := a) -> Comprehension t a Comprehension (((t <:.> Construction t) := b) -> Comprehension t b) -> (((t :. Construction t) := b) -> (t <:.> Construction t) := b) -> ((t :. Construction t) := b) -> Comprehension t b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . ((t :. Construction t) := b) -> (t <:.> Construction t) := b forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((t :. Construction t) := b) -> Comprehension t b) -> ((t :. Construction t) := b) -> Comprehension t b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ (\(Construct a x (t :. Construction t) := a xs) -> ((t <:.> Construction t) := b) -> (t :. Construction t) := b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (((t <:.> Construction t) := b) -> (t :. Construction t) := b) -> (Comprehension t b -> (t <:.> Construction t) := b) -> Comprehension t b -> (t :. Construction t) := b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . Comprehension t b -> (t <:.> Construction t) := b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Comprehension t b -> (t :. Construction t) := b) -> Comprehension t b -> (t :. Construction t) := b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ a -> Comprehension t b f a x Comprehension t b -> Comprehension t b -> Comprehension t b forall a. Semigroup a => a -> a -> a + (a -> Comprehension t b f (a -> Comprehension t b) -> Comprehension t a -> Comprehension t b forall (source :: * -> * -> *) (t :: * -> *) a b. Bindable source t => source a (t b) -> source (t a) (t b) =<< TU Covariant Covariant t (Construction t) a -> Comprehension t a forall (t :: * -> *) a. ((t <:.> Construction t) := a) -> Comprehension t a Comprehension (((t :. Construction t) := a) -> TU Covariant Covariant t (Construction t) a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (t :. Construction t) := a xs))) (Construction t a -> (t :. Construction t) := b) -> ((t :. Construction t) := a) -> (t :. Construction t) := b forall (source :: * -> * -> *) (t :: * -> *) a b. Bindable source t => source a (t b) -> source (t a) (t b) =<< (t :. Construction t) := a t instance Setoid (t <:.> Construction t := a) => Setoid (Comprehension t a) where Comprehension (t <:.> Construction t) := a ls == :: Comprehension t a -> Comprehension t a -> Boolean == Comprehension (t <:.> Construction t) := a rs = (t <:.> Construction t) := a ls ((t <:.> Construction t) := a) -> ((t <:.> Construction t) := a) -> Boolean forall a. Setoid a => a -> a -> Boolean == (t <:.> Construction t) := a rs instance Semigroup (t <:.> Construction t := a) => Semigroup (Comprehension t a) where Comprehension (t <:.> Construction t) := a x + :: Comprehension t a -> Comprehension t a -> Comprehension t a + Comprehension (t <:.> Construction t) := a y = ((t <:.> Construction t) := a) -> Comprehension t a forall (t :: * -> *) a. ((t <:.> Construction t) := a) -> Comprehension t a Comprehension (((t <:.> Construction t) := a) -> Comprehension t a) -> ((t <:.> Construction t) := a) -> Comprehension t a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ (t <:.> Construction t) := a x ((t <:.> Construction t) := a) -> ((t <:.> Construction t) := a) -> (t <:.> Construction t) := a forall a. Semigroup a => a -> a -> a + (t <:.> Construction t) := a y instance Monoid (t <:.> Construction t := a) => Monoid (Comprehension t a) where zero :: Comprehension t a zero = ((t <:.> Construction t) := a) -> Comprehension t a forall (t :: * -> *) a. ((t <:.> Construction t) := a) -> Comprehension t a Comprehension (t <:.> Construction t) := a forall a. Monoid a => a zero instance (Covariant (->) (->) t, Monoidal (->) (->) (:*:) (:*:) t) => Morphable Push (Comprehension t) where type Morphing Push (Comprehension t) = Identity <:.:> Comprehension t := (->) morphing :: (<:.>) (Tagged 'Push) (Comprehension t) a -> Morphing 'Push (Comprehension t) a morphing (Comprehension t a -> TU Covariant Covariant t (Construction t) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Comprehension t a -> TU Covariant Covariant t (Construction t) a) -> ((<:.>) (Tagged 'Push) (Comprehension t) a -> Comprehension t a) -> (<:.>) (Tagged 'Push) (Comprehension t) a -> TU Covariant Covariant t (Construction t) a forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Push) (Comprehension t) a -> Comprehension t a forall k (mod :: k) (struct :: * -> *). Morphable mod struct => (Tagged mod <:.> struct) ~> struct premorph -> TU Covariant Covariant t (Construction t) a xs) = (Identity a -> Comprehension t a) -> T_U Covariant Covariant (->) Identity (Comprehension t) 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 ((Identity a -> Comprehension t a) -> T_U Covariant Covariant (->) Identity (Comprehension t) a) -> (Identity a -> Comprehension t a) -> T_U Covariant Covariant (->) Identity (Comprehension t) a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ \(Identity a x) -> TU Covariant Covariant t (Construction t) a -> Comprehension t a forall (t :: * -> *) a. ((t <:.> Construction t) := a) -> Comprehension t a Comprehension (TU Covariant Covariant t (Construction t) a -> Comprehension t a) -> (TU Covariant Covariant t (Construction t) a -> TU Covariant Covariant t (Construction t) a) -> TU Covariant Covariant t (Construction t) a -> Comprehension t a forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . Construction t a -> TU Covariant Covariant t (Construction t) a forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *) a. (Liftable cat t, Covariant cat cat u) => cat (u a) (t u a) lift (Construction t a -> TU Covariant Covariant t (Construction t) a) -> (TU Covariant Covariant t (Construction t) a -> Construction t a) -> TU Covariant Covariant t (Construction t) a -> TU Covariant Covariant t (Construction t) a forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> ((t :. Construction t) := a) -> Construction t a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (((t :. Construction t) := a) -> Construction t a) -> (TU Covariant Covariant t (Construction t) a -> (t :. Construction t) := a) -> TU Covariant Covariant t (Construction t) a -> Construction t a forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . TU Covariant Covariant t (Construction t) a -> (t :. Construction t) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (TU Covariant Covariant t (Construction t) a -> Comprehension t a) -> TU Covariant Covariant t (Construction t) a -> Comprehension t a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ TU Covariant Covariant t (Construction t) a xs instance Nullable (t <:.> Construction t) => Nullable (Comprehension t) where null :: (Predicate :. Comprehension t) := a null = Comprehension t a -> (t <:.> Construction t) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Comprehension t a -> (t <:.> Construction t) := a) -> Predicate ((t <:.> Construction t) := a) -> (Predicate :. Comprehension t) := a forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Contravariant source target t => source a b -> target (t b) (t a) ->$<- Predicate ((t <:.> Construction t) := a) forall k (t :: k -> *) (a :: k). Nullable t => (Predicate :. t) := a null