module Pandora.Paradigm.Controlflow.Effect.Interpreted where import Pandora.Pattern.Morphism.Straight (Straight (Straight)) import Pandora.Pattern.Morphism.Flip (Flip (Flip)) import Pandora.Core.Functor (type (:.), type (:=)) import Pandora.Pattern.Semigroupoid (Semigroupoid ((.))) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)), (<$$>), (<$$$>), (<$$$$>)) import Pandora.Pattern.Transformer.Liftable (Liftable (lift)) import Pandora.Paradigm.Primary.Algebraic.Exponential () infixr 2 ||=, =|| type family Schematic (c :: (* -> * -> *) -> (* -> *) -> k) (t :: * -> *) = (r :: (* -> *) -> * -> *) | r -> t class Interpreted m t where {-# MINIMAL run, unite #-} type Primary t a :: * run :: m (t a) (Primary t a) unite :: m (Primary t a) (t a) (||=) :: (Semigroupoid m, Interpreted m u) => m (Primary t a) (Primary u b) -> m (t a) (u b) (||=) m (Primary t a) (Primary u b) f = m (Primary u b) (u b) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (Primary t a) (t a) unite m (Primary u b) (u b) -> m (t a) (Primary u b) -> m (t a) (u b) forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . m (Primary t a) (Primary u b) f m (Primary t a) (Primary u b) -> m (t a) (Primary t a) -> m (t a) (Primary u b) forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . m (t a) (Primary t a) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) run (=||) :: (Semigroupoid m, Interpreted m u) => m (t a) (u b) -> m (Primary t a) (Primary u b) (=||) m (t a) (u b) f = m (u b) (Primary u b) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) run m (u b) (Primary u b) -> m (Primary t a) (u b) -> m (Primary t a) (Primary u b) forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . m (t a) (u b) f m (t a) (u b) -> m (Primary t a) (t a) -> m (Primary t a) (u b) forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . m (Primary t a) (t a) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (Primary t a) (t a) unite (<$||=) :: (Semigroupoid m, Covariant m m j, Interpreted m u) => m (Primary t a) (Primary u b) -> m (j := t a) (j := u b) (<$||=) m (Primary t a) (Primary u b) f = m (t a) (u b) -> m (j := t a) (j := u b) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) (<$>) (m (Primary t a) (Primary u b) -> m (t a) (u b) forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Interpreted m t, Semigroupoid m, Interpreted m u) => m (Primary t a) (Primary u b) -> m (t a) (u b) (||=) m (Primary t a) (Primary u b) f) (<$$||=) :: (Semigroupoid m, Covariant m m j, Covariant m m k, Interpreted m u) => m (Primary t a) (Primary u b) -> m (j :. k := t a) (j :. k := u b) (<$$||=) m (Primary t a) (Primary u b) f = m (t a) (u b) -> m ((j :. k) := t a) ((j :. k) := u b) forall (source :: * -> * -> *) (between :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Covariant source between u, Covariant between target t) => source a b -> target (t (u a)) (t (u b)) (<$$>) @m @m (m (Primary t a) (Primary u b) -> m (t a) (u b) forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Interpreted m t, Semigroupoid m, Interpreted m u) => m (Primary t a) (Primary u b) -> m (t a) (u b) (||=) m (Primary t a) (Primary u b) f) (<$$$||=) :: (Semigroupoid m, Covariant m m j, Covariant m m k, Covariant m m l, Interpreted m u) => m (Primary t a) (Primary u b) -> m (j :. k :. l := t a) (j :. k :. l := u b) (<$$$||=) m (Primary t a) (Primary u b) f = m (t a) (u b) -> m ((j :. (k :. l)) := t a) ((j :. (k :. l)) := u b) forall (source :: * -> * -> *) (between1 :: * -> * -> *) (between2 :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) (v :: * -> *) a b. (Covariant source between1 v, Covariant between1 between2 u, Covariant between2 target t) => source a b -> target (t (u (v a))) (t (u (v b))) (<$$$>) @m @m @m (m (Primary t a) (Primary u b) -> m (t a) (u b) forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Interpreted m t, Semigroupoid m, Interpreted m u) => m (Primary t a) (Primary u b) -> m (t a) (u b) (||=) m (Primary t a) (Primary u b) f) (<$$$$||=) :: (Semigroupoid m, Covariant m m j, Covariant m m k, Covariant m m l, Covariant m m n, Interpreted m u) => m (Primary t a) (Primary u b) -> m (j :. k :. l :. n := t a) (j :. k :. l :. n := u b) (<$$$$||=) m (Primary t a) (Primary u b) f = m (t a) (u b) -> m ((j :. (k :. (l :. n))) := t a) ((j :. (k :. (l :. n))) := u b) forall (source :: * -> * -> *) (between1 :: * -> * -> *) (between2 :: * -> * -> *) (between3 :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) (v :: * -> *) (w :: * -> *) a b. (Covariant source between1 w, Covariant between1 between2 v, Covariant between2 between3 u, Covariant between3 target t) => source a b -> target (t (u (v (w a)))) (t (u (v (w b)))) (<$$$$>) @m @m @m @m (m (Primary t a) (Primary u b) -> m (t a) (u b) forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Interpreted m t, Semigroupoid m, Interpreted m u) => m (Primary t a) (Primary u b) -> m (t a) (u b) (||=) m (Primary t a) (Primary u b) f) (=||$>) :: (Covariant m m j, Interpreted m u) => m (t a) (u b) -> m (j := Primary t a) (j := Primary u b) (=||$>) m (t a) (u b) f = m (Primary t a) (Primary u b) -> m (j := Primary t a) (j := Primary u b) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) (<$>) (m (t a) (u b) -> m (Primary t a) (Primary u b) forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Interpreted m t, Semigroupoid m, Interpreted m u) => m (t a) (u b) -> m (Primary t a) (Primary u b) (=||) m (t a) (u b) f) (=||$$>) :: (Covariant m m j, Covariant m m k, Interpreted m u) => m (t a) (u b) -> m (j :. k := Primary t a) (j :. k := Primary u b) (=||$$>) m (t a) (u b) f = m (Primary t a) (Primary u b) -> m ((j :. k) := Primary t a) ((j :. k) := Primary u b) forall (source :: * -> * -> *) (between :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Covariant source between u, Covariant between target t) => source a b -> target (t (u a)) (t (u b)) (<$$>) @m @m (m (t a) (u b) -> m (Primary t a) (Primary u b) forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Interpreted m t, Semigroupoid m, Interpreted m u) => m (t a) (u b) -> m (Primary t a) (Primary u b) (=||) m (t a) (u b) f) (=||$$$>) :: (Covariant m m j, Covariant m m k, Covariant m m l, Interpreted m u) => m (t a) (u b) -> m (j :. k :. l := Primary t a) (j :. k :. l := Primary u b) (=||$$$>) m (t a) (u b) f = m (Primary t a) (Primary u b) -> m ((j :. (k :. l)) := Primary t a) ((j :. (k :. l)) := Primary u b) forall (source :: * -> * -> *) (between1 :: * -> * -> *) (between2 :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) (v :: * -> *) a b. (Covariant source between1 v, Covariant between1 between2 u, Covariant between2 target t) => source a b -> target (t (u (v a))) (t (u (v b))) (<$$$>) @m @m @m (m (t a) (u b) -> m (Primary t a) (Primary u b) forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Interpreted m t, Semigroupoid m, Interpreted m u) => m (t a) (u b) -> m (Primary t a) (Primary u b) (=||) m (t a) (u b) f) (=||$$$$>) :: (Covariant m m j, Covariant m m k, Covariant m m l, Covariant m m n, Interpreted m u) => m (t a) (u b) -> m (j :. k :. l :. n := Primary t a) (j :. k :. l :. n := Primary u b) (=||$$$$>) m (t a) (u b) f = m (Primary t a) (Primary u b) -> m ((j :. (k :. (l :. n))) := Primary t a) ((j :. (k :. (l :. n))) := Primary u b) forall (source :: * -> * -> *) (between1 :: * -> * -> *) (between2 :: * -> * -> *) (between3 :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) (v :: * -> *) (w :: * -> *) a b. (Covariant source between1 w, Covariant between1 between2 v, Covariant between2 between3 u, Covariant between3 target t) => source a b -> target (t (u (v (w a)))) (t (u (v (w b)))) (<$$$$>) @m @m @m @m (m (t a) (u b) -> m (Primary t a) (Primary u b) forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Interpreted m t, Semigroupoid m, Interpreted m u) => m (t a) (u b) -> m (Primary t a) (Primary u b) (=||) m (t a) (u b) f) (-=:) :: (Liftable m t, Interpreted m (t u), Interpreted m (t v), Covariant m m u) => m (t u a) (t v b) -> m (u a) (Primary (t v) b) -=: :: m (t u a) (t v b) -> m (u a) (Primary (t v) b) (-=:) m (t u a) (t v b) f = m (t v b) (Primary (t v) b) forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => m (t a) (Primary t a) run m (t v b) (Primary (t v) b) -> m (u a) (t v b) -> m (u a) (Primary (t v) b) forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . m (t u a) (t v b) f m (t u a) (t v b) -> m (u a) (t u a) -> m (u a) (t v b) forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . m (u a) (t u a) forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *) a. (Liftable cat t, Covariant cat cat u) => cat (u a) (t u a) lift instance Interpreted (->) (Flip v a) where type Primary (Flip v a) e = v e a run :: Flip v a a -> Primary (Flip v a) a run ~(Flip v a a x) = v a a Primary (Flip v a) a x unite :: Primary (Flip v a) a -> Flip v a a unite = Primary (Flip v a) a -> Flip v a a forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip instance Interpreted (->) (Straight v e) where type Primary (Straight v e) a = v e a run :: Straight v e a -> Primary (Straight v e) a run ~(Straight v e a x) = v e a Primary (Straight v e) a x unite :: Primary (Straight v e) a -> Straight v e a unite = Primary (Straight v e) a -> Straight v e a forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight