{-# LANGUAGE UndecidableInstances #-} module Pandora.Paradigm.Structure.Ability.Comprehension where import Pandora.Core.Functor (type (:=)) import Pandora.Pattern.Category ((.), ($)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>))) import Pandora.Pattern.Functor.Bindable (Bindable ((>>=))) import Pandora.Pattern.Object.Semigroup (Semigroup ((+))) import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>)) import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct)) import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run)) 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 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 a b -> m a b $ 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 (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 :: * -> * -> *) a b. Category m => m a b -> m a b $ (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) -> ((t <:.> Construction t) := b) -> (t :. Construction t) := b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Comprehension t b -> Primary (Comprehension t) b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (a -> Comprehension t b f a x) ((t <:.> Construction t) := b) -> ((t <:.> Construction t) := b) -> (t <:.> Construction t) := b forall a. Semigroup a => a -> a -> a + Comprehension t b -> Primary (Comprehension t) b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (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)