{-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE UndecidableInstances #-} module Pandora.Paradigm.Structure.Modification.Comprehension where import Pandora.Core.Functor (type (:=)) import Pandora.Pattern.Category ((.), ($)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>))) import Pandora.Pattern.Functor.Contravariant ((>$<)) import Pandora.Pattern.Functor.Pointable (Pointable (point)) import Pandora.Pattern.Functor.Applicative (Applicative ((<*>))) import Pandora.Pattern.Functor.Alternative (Alternative ((<+>))) import Pandora.Pattern.Functor.Avoidable (Avoidable (empty)) import Pandora.Pattern.Functor.Traversable (Traversable ((->>))) import Pandora.Pattern.Functor.Bindable (Bindable ((>>=))) import Pandora.Pattern.Functor.Monad (Monad) 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.Functor.Function ((%)) 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)) 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 :: * -> * -> *). Category m => m ~~> m $ a -> b f (a -> b) -> ((t <:.> Construction t) := a) -> (t <:.> Construction t) := b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> (t <:.> Construction t) := a x instance (Avoidable t, Pointable t) => Pointable (Comprehension t) where point :: a :=> Comprehension t point = ((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) -> (a -> (t <:.> Construction t) := a) -> a :=> Comprehension t forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((t :. Construction t) := a) -> (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) -> (t <:.> Construction t) := a) -> (a -> (t :. Construction t) := a) -> a -> (t <:.> Construction t) := a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction t a :=> t forall (t :: * -> *) a. Pointable t => a :=> t point (Construction t a :=> t) -> (a -> Construction t a) -> a -> (t :. Construction t) := a forall (m :: * -> * -> *) b c a. Category 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 -> ((t :. Construction t) := a) -> Construction t a) -> ((t :. Construction t) := a) -> a -> Construction t a forall a b c. (a -> b -> c) -> b -> a -> c % (t :. Construction t) := a forall (t :: * -> *) a. Avoidable t => t a empty instance Alternative t => Alternative (Comprehension t) 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 :: * -> * -> *). Category m => m ~~> m $ (t <:.> Construction t) := a x ((t <:.> Construction t) := a) -> ((t <:.> Construction t) := a) -> (t <:.> Construction t) := a forall (t :: * -> *) a. Alternative t => t a -> t a -> t a <+> (t <:.> Construction t) := a y instance (Avoidable t, Alternative t) => Avoidable (Comprehension t) where empty :: Comprehension t a empty = ((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. Avoidable t => t a empty instance Traversable (t <:.> Construction t) => Traversable (Comprehension t) where Comprehension (t <:.> Construction t) := a x ->> :: Comprehension t a -> (a -> u b) -> (u :. Comprehension t) := b ->> a -> u b f = ((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 (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> (t <:.> Construction t) := a x ((t <:.> Construction t) := a) -> (a -> u b) -> u ((t <:.> Construction t) := b) forall (t :: * -> *) (u :: * -> *) a b. (Traversable t, Pointable u, Applicative u) => t a -> (a -> u b) -> (u :. t) := b ->> a -> u b f instance (forall a . Semigroup (t <:.> Construction t := a), Bindable t, Pointable t, Avoidable t) => Applicative (Comprehension t) where Comprehension t (a -> b) fs <*> :: Comprehension t (a -> b) -> Comprehension t a -> Comprehension t b <*> Comprehension t a xs = Comprehension t (a -> b) fs Comprehension t (a -> b) -> ((a -> b) -> Comprehension t b) -> Comprehension t b forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b >>= \a -> b f -> Comprehension t a xs Comprehension t a -> (a -> Comprehension t b) -> Comprehension t b forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b >>= ((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) -> (a -> (t <:.> Construction t) := b) -> a -> Comprehension t b forall (m :: * -> * -> *) b c a. Category 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) -> (t <:.> Construction t) := b) -> (a -> (t :. Construction t) := b) -> a -> (t <:.> Construction t) := b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction t b :=> t forall (t :: * -> *) a. Pointable t => a :=> t point (Construction t b :=> t) -> (a -> Construction t b) -> a -> (t :. Construction t) := b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . b :=> Construction t forall (t :: * -> *) a. Pointable t => a :=> t point (b :=> Construction t) -> (a -> b) -> a -> Construction t b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> b f instance (forall a . Semigroup (t <:.> Construction t := a), Bindable t) => Bindable (Comprehension t) where Comprehension (TU (t :. Construction t) := a t) >>= :: Comprehension t a -> (a -> Comprehension t b) -> Comprehension t b >>= a -> Comprehension t b f = ((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. Category 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 :: * -> * -> *). Category m => m ~~> m $ (t :. Construction t) := a t ((t :. Construction t) := a) -> (Construction t a -> (t :. Construction t) := b) -> (t :. Construction t) := b forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t 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. Category 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 :: * -> * -> *). Category m => m ~~> m $ a -> Comprehension t b f a x Comprehension t b -> Comprehension t b -> Comprehension t b forall a. Semigroup a => a -> a -> a + (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) Comprehension t a -> (a -> Comprehension t b) -> Comprehension t b forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b >>= a -> Comprehension t b f) instance (forall a . Semigroup (t <:.> Construction t := a), Pointable t, Avoidable t, Bindable t) => Monad (Comprehension t) where 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 :: * -> * -> *). Category m => m ~~> m $ (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 Pointable 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. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Push) (Comprehension t) a -> Comprehension t a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t 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 :: * -> * -> *). Category m => m ~~> m $ \(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. Category m => m b c -> m a b -> m a c . Construction t a -> TU Covariant Covariant t (Construction t) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u 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. Category 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. Category 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 :: * -> * -> *). Category m => m ~~> m $ 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 (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a >$< Predicate ((t <:.> Construction t) := a) forall k (t :: k -> *) (a :: k). Nullable t => (Predicate :. t) := a null