module Pandora.Paradigm.Primary.Transformer.Construction where import Pandora.Core.Functor (type (:.), type (:=), type (|->), type (~>)) import Pandora.Pattern.Category ((.), ($)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (<$$>))) import Pandora.Pattern.Functor.Avoidable (Avoidable (empty)) import Pandora.Pattern.Functor.Pointable (Pointable (point)) import Pandora.Pattern.Functor.Extractable (Extractable (extract)) import Pandora.Pattern.Functor.Alternative (Alternative ((<+>))) import Pandora.Pattern.Functor.Applicative (Applicative ((<*>), (<**>))) import Pandora.Pattern.Functor.Traversable (Traversable ((->>), (->>>))) import Pandora.Pattern.Functor.Bindable (Bindable ((>>=))) import Pandora.Pattern.Functor.Extendable (Extendable ((=>>), extend)) import Pandora.Pattern.Functor.Monad (Monad) import Pandora.Pattern.Functor.Comonad (Comonad) import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower)) import Pandora.Pattern.Transformer.Hoistable (Hoistable (hoist)) import Pandora.Pattern.Object.Setoid (Setoid ((==))) import Pandora.Pattern.Object.Semigroup (Semigroup ((+))) import Pandora.Pattern.Object.Ringoid ((*)) import Pandora.Pattern.Object.Monoid (Monoid (zero)) import Pandora.Paradigm.Controlflow (run) import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>)) data Construction t a = Construct a (t :. Construction t := a) instance Covariant t => Covariant (Construction t) where a -> b f <$> :: (a -> b) -> Construction t a -> Construction t b <$> Construction t a x = b -> ((t :. Construction t) := b) -> Construction t b forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> b f (a -> b) -> a -> b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a <-| Construction t forall (t :: * -> *) a. Extractable t => a <-| t extract Construction t a x) (((t :. Construction t) := b) -> Construction t b) -> ((t :. Construction t) := b) -> Construction 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 :: * -> *) (u :: * -> *) a b. (Covariant t, Covariant u) => (a -> b) -> ((t :. u) := a) -> (t :. u) := b <$$> Construction t a -> (t :. Construction t) := a forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction t a x instance Avoidable t => Pointable (Construction t) where point :: a |-> Construction t point a x = 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 forall (t :: * -> *) a. Avoidable t => t a empty instance Covariant t => Extractable (Construction t) where extract :: a <-| Construction t extract ~(Construct a x (t :. Construction t) := a _) = a x instance Applicative t => Applicative (Construction t) where Construction t (a -> b) f <*> :: Construction t (a -> b) -> Construction t a -> Construction t b <*> Construction t a x = b -> ((t :. Construction t) := b) -> Construction t b forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct ((a -> b) <-| Construction t forall (t :: * -> *) a. Extractable t => a <-| t extract Construction t (a -> b) f (a -> b) -> a -> b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a <-| Construction t forall (t :: * -> *) a. Extractable t => a <-| t extract Construction t a x) (((t :. Construction t) := b) -> Construction t b) -> ((t :. Construction t) := b) -> Construction t b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction t (a -> b) -> (:.) t (Construction t) (a -> b) forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction t (a -> b) f (:.) t (Construction t) (a -> b) -> ((t :. Construction t) := a) -> (t :. Construction t) := b forall (t :: * -> *) (u :: * -> *) a b. (Applicative t, Applicative u) => ((t :. u) := (a -> b)) -> ((t :. u) := a) -> (t :. u) := b <**> Construction t a -> (t :. Construction t) := a forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction t a x instance Traversable t => Traversable (Construction t) where Construction t a x ->> :: Construction t a -> (a -> u b) -> (u :. Construction t) := b ->> a -> u b f = b -> ((t :. Construction t) := b) -> Construction t b forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (b -> ((t :. Construction t) := b) -> Construction t b) -> u b -> u (((t :. Construction t) := b) -> Construction t b) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> a -> u b f (a <-| Construction t forall (t :: * -> *) a. Extractable t => a <-| t extract Construction t a x) u (((t :. Construction t) := b) -> Construction t b) -> u ((t :. Construction t) := b) -> (u :. Construction t) := b forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b <*> Construction t a -> (:.) t (Construction t) a forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction t a x (:.) t (Construction t) a -> (a -> u b) -> u ((t :. Construction t) := b) forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b. (Traversable t, Pointable u, Applicative u, Traversable v) => ((v :. t) := a) -> (a -> u b) -> (u :. (v :. t)) := b ->>> a -> u b f instance Alternative t => Bindable (Construction t) where Construction t a x >>= :: Construction t a -> (a -> Construction t b) -> Construction t b >>= a -> Construction t b f = b -> ((t :. Construction t) := b) -> Construction t b forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (b <-| Construction t forall (t :: * -> *) a. Extractable t => a <-| t extract (b <-| Construction t) -> (a -> Construction t b) -> a -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Construction t b f (a -> b) -> a -> b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a <-| Construction t forall (t :: * -> *) a. Extractable t => a <-| t extract Construction t a x) (((t :. Construction t) := b) -> Construction t b) -> ((t :. Construction t) := b) -> Construction t b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (Construction t b -> (t :. Construction t) := b forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct (Construction t b -> (t :. Construction t) := b) -> (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 . a -> Construction t b f (a -> (t :. Construction t) := b) -> a -> (t :. Construction t) := b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a <-| Construction t forall (t :: * -> *) a. Extractable t => a <-| t extract Construction t a x) ((t :. Construction t) := b) -> ((t :. Construction t) := b) -> (t :. Construction t) := b forall (t :: * -> *) a. Alternative t => t a -> t a -> t a <+> (Construction t a -> (a -> Construction t b) -> Construction t b forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b >>= a -> Construction t b f) (Construction t a -> Construction t b) -> t (Construction t a) -> (t :. Construction t) := b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> Construction t a -> t (Construction t a) forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction t a x instance Covariant t => Extendable (Construction t) where Construction t a x =>> :: Construction t a -> (Construction t a -> b) -> Construction t b =>> Construction t a -> b f = b -> ((t :. Construction t) := b) -> Construction t b forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (Construction t a -> b f Construction t a x) (((t :. Construction t) := b) -> Construction t b) -> ((t :. Construction t) := b) -> Construction t b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (Construction t a -> b) -> Construction t a -> Construction t b forall (t :: * -> *) a b. Extendable t => (t a -> b) -> t a -> t b extend Construction t a -> b f (Construction t a -> Construction t b) -> t (Construction t a) -> (t :. Construction t) := b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> Construction t a -> t (Construction t a) forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction t a x instance (Avoidable t, Alternative t) => Monad (Construction t) where instance Covariant t => Comonad (Construction t) where instance Lowerable Construction where lower :: Construction u ~> u lower Construction u a x = a <-| Construction u forall (t :: * -> *) a. Extractable t => a <-| t extract (a <-| Construction u) -> u (Construction u a) -> u a forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> Construction u a -> u (Construction u a) forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction u a x instance Hoistable Construction where hoist :: (u ~> v) -> Construction u ~> Construction v hoist u ~> v f Construction u a x = a -> ((v :. Construction v) := a) -> Construction v a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a <-| Construction u forall (t :: * -> *) a. Extractable t => a <-| t extract Construction u a x) (((v :. Construction v) := a) -> Construction v a) -> (u (Construction v a) -> (v :. Construction v) := a) -> u (Construction v a) -> Construction v a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . u (Construction v a) -> (v :. Construction v) := a u ~> v f (u (Construction v a) -> Construction v a) -> u (Construction v a) -> Construction v a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (u ~> v) -> Construction u ~> Construction v forall k (t :: (* -> *) -> k -> *) (u :: * -> *) (v :: * -> *). (Hoistable t, Covariant u) => (u ~> v) -> t u ~> t v hoist u ~> v f (Construction u a -> Construction v a) -> u (Construction u a) -> u (Construction v a) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> Construction u a -> u (Construction u a) forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction u a x instance (Setoid a, forall b . Setoid b => Setoid (t b), Covariant t) => Setoid (Construction t a) where Construction t a x == :: Construction t a -> Construction t a -> Boolean == Construction t a y = (a <-| Construction t forall (t :: * -> *) a. Extractable t => a <-| t extract Construction t a x a -> a -> Boolean forall a. Setoid a => a -> a -> Boolean == a <-| Construction t forall (t :: * -> *) a. Extractable t => a <-| t extract Construction t a y) Boolean -> Boolean -> Boolean forall a. Ringoid a => a -> a -> a * (Construction t a -> (:.) t (Construction t) a forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction t a x (:.) t (Construction t) a -> (:.) t (Construction t) a -> Boolean forall a. Setoid a => a -> a -> Boolean == Construction t a -> (:.) t (Construction t) a forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction t a y) instance (Semigroup a, forall b . Semigroup b => Semigroup (t b), Covariant t) => Semigroup (Construction t a) where Construction t a x + :: Construction t a -> Construction t a -> Construction t a + Construction t a y = a -> ((t :. Construction t) := a) -> Construction t a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a <-| Construction t forall (t :: * -> *) a. Extractable t => a <-| t extract Construction t a x a -> a -> a forall a. Semigroup a => a -> a -> a + a <-| Construction t forall (t :: * -> *) a. Extractable t => a <-| t extract Construction t a y) (((t :. Construction t) := a) -> Construction t a) -> ((t :. Construction t) := a) -> Construction t a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Construction t a -> (t :. Construction t) := a forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction t a x ((t :. Construction t) := a) -> ((t :. Construction t) := a) -> (t :. Construction t) := a forall a. Semigroup a => a -> a -> a + Construction t a -> (t :. Construction t) := a forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Construction t a y instance (Monoid a, forall b . Semigroup b => Monoid (t b), Covariant t) => Monoid (Construction t a) where zero :: Construction t a zero = a -> ((t :. Construction t) := a) -> Construction t a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a forall a. Monoid a => a zero (t :. Construction t) := a forall a. Monoid a => a zero deconstruct :: Construction t a -> (t :. Construction t) a deconstruct :: Construction t a -> (:.) t (Construction t) a deconstruct ~(Construct a _ (:.) t (Construction t) a xs) = (:.) t (Construction t) a xs iterate :: Covariant t => (a |-> t) -> (a |-> Construction t) iterate :: (a |-> t) -> a |-> Construction t iterate a |-> t f a x = 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) -> ((t :. Construction t) := a) -> Construction t a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (a |-> t) -> a |-> Construction t forall (t :: * -> *) a. Covariant t => (a |-> t) -> a |-> Construction t iterate a |-> t f (a |-> Construction t) -> t a -> (t :. Construction t) := a forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> a |-> t f a x section :: Comonad t => t ~> Construction t section :: t ~> Construction t section t a xs = a -> ((t :. Construction t) := a) -> Construction t a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a <-| t forall (t :: * -> *) a. Extractable t => a <-| t extract t a xs) (((t :. Construction t) := a) -> Construction t a) -> ((t :. Construction t) := a) -> Construction t a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ t a xs t a -> (t a -> Construction t a) -> (t :. Construction t) := a forall (t :: * -> *) a b. Extendable t => t a -> (t a -> b) -> t b =>> t a -> Construction t a forall (t :: * -> *). Comonad t => t ~> Construction t section instance (Covariant u, Covariant t) => Covariant (t <:.> Construction u) where a -> b f <$> :: (a -> b) -> (<:.>) t (Construction u) a -> (<:.>) t (Construction u) b <$> (<:.>) t (Construction u) a g = ((t :. Construction u) := b) -> (<:.>) t (Construction u) 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 u) := b) -> (<:.>) t (Construction u) b) -> ((t :. Construction u) := b) -> (<:.>) t (Construction u) b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a -> b f (a -> b) -> ((t :. Construction u) := a) -> (t :. Construction u) := b forall (t :: * -> *) (u :: * -> *) a b. (Covariant t, Covariant u) => (a -> b) -> ((t :. u) := a) -> (t :. u) := b <$$> (<:.>) t (Construction u) a -> Primary (t <:.> Construction u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (<:.>) t (Construction u) a g instance (Avoidable u, Pointable t) => Pointable (t <:.> Construction u) where point :: a |-> (t <:.> Construction u) point a x = ((t :. Construction u) := a) -> TU Covariant Covariant t (Construction u) 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 u) := a) -> TU Covariant Covariant t (Construction u) a) -> (((u :. Construction u) := a) -> (t :. Construction u) := a) -> ((u :. Construction u) := a) -> TU Covariant Covariant t (Construction u) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction u a |-> t forall (t :: * -> *) a. Pointable t => a |-> t point (Construction u a |-> t) -> (((u :. Construction u) := a) -> Construction u a) -> ((u :. Construction u) := a) -> (t :. Construction u) := a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> ((u :. Construction u) := a) -> Construction u a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (((u :. Construction u) := a) -> TU Covariant Covariant t (Construction u) a) -> ((u :. Construction u) := a) -> TU Covariant Covariant t (Construction u) a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (u :. Construction u) := a forall (t :: * -> *) a. Avoidable t => t a empty instance (Applicative u, Applicative t) => Applicative (t <:.> Construction u) where (<:.>) t (Construction u) (a -> b) f <*> :: (<:.>) t (Construction u) (a -> b) -> (<:.>) t (Construction u) a -> (<:.>) t (Construction u) b <*> (<:.>) t (Construction u) a x = ((t :. Construction u) := b) -> (<:.>) t (Construction u) 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 u) := b) -> (<:.>) t (Construction u) b) -> ((t :. Construction u) := b) -> (<:.>) t (Construction u) b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (<:.>) t (Construction u) (a -> b) -> Primary (t <:.> Construction u) (a -> b) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (<:.>) t (Construction u) (a -> b) f ((t :. Construction u) := (a -> b)) -> ((t :. Construction u) := a) -> (t :. Construction u) := b forall (t :: * -> *) (u :: * -> *) a b. (Applicative t, Applicative u) => ((t :. u) := (a -> b)) -> ((t :. u) := a) -> (t :. u) := b <**> (<:.>) t (Construction u) a -> Primary (t <:.> Construction u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (<:.>) t (Construction u) a x instance (Covariant u, Alternative t) => Alternative (t <:.> Construction u) where (<:.>) t (Construction u) a x <+> :: (<:.>) t (Construction u) a -> (<:.>) t (Construction u) a -> (<:.>) t (Construction u) a <+> (<:.>) t (Construction u) a y = ((t :. Construction u) := a) -> (<:.>) t (Construction u) 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 u) := a) -> (<:.>) t (Construction u) a) -> ((t :. Construction u) := a) -> (<:.>) t (Construction u) a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ (<:.>) t (Construction u) a -> Primary (t <:.> Construction u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (<:.>) t (Construction u) a x ((t :. Construction u) := a) -> ((t :. Construction u) := a) -> (t :. Construction u) := a forall (t :: * -> *) a. Alternative t => t a -> t a -> t a <+> (<:.>) t (Construction u) a -> Primary (t <:.> Construction u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (<:.>) t (Construction u) a y instance (Covariant u, Avoidable t) => Avoidable (t <:.> Construction u) where empty :: (<:.>) t (Construction u) a empty = ((t :. Construction u) := a) -> (<:.>) t (Construction u) 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 u) := a forall (t :: * -> *) a. Avoidable t => t a empty instance (Traversable u, Traversable t) => Traversable (t <:.> Construction u) where (<:.>) t (Construction u) a g ->> :: (<:.>) t (Construction u) a -> (a -> u b) -> (u :. (t <:.> Construction u)) := b ->> a -> u b f = ((t :. Construction u) := b) -> TU Covariant Covariant t (Construction u) 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 u) := b) -> TU Covariant Covariant t (Construction u) b) -> u ((t :. Construction u) := b) -> (u :. (t <:.> Construction u)) := b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> (<:.>) t (Construction u) a -> Primary (t <:.> Construction u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (<:.>) t (Construction u) a g ((t :. Construction u) := a) -> (a -> u b) -> u ((t :. Construction u) := b) forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b. (Traversable t, Pointable u, Applicative u, Traversable v) => ((v :. t) := a) -> (a -> u b) -> (u :. (v :. t)) := b ->>> a -> u b f