module Pandora.Paradigm.Controlflow.Effect.Interpreted where import Pandora.Core.Functor (type (:.), type (:=)) import Pandora.Pattern.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 t where {-# MINIMAL run, unite #-} type Primary t a :: * run :: t a -> Primary t a unite :: Primary t a -> t a (||=) :: Interpreted u => (Primary t a -> Primary u b) -> t a -> u b (||=) Primary t a -> Primary u b f = Primary u b -> u b forall (t :: * -> *) a. Interpreted t => Primary t a -> t a unite (Primary u b -> u b) -> (t a -> Primary u b) -> t a -> u b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . Primary t a -> Primary u b f (Primary t a -> Primary u b) -> (t a -> Primary t a) -> t a -> Primary u b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . t a -> Primary t a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (=||) :: Interpreted u => (t a -> u b) -> Primary t a -> Primary u b (=||) t a -> u b f = u b -> Primary u b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (u b -> Primary u b) -> (Primary t a -> u b) -> Primary t a -> Primary u b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . t a -> u b f (t a -> u b) -> (Primary t a -> t a) -> Primary t a -> u b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . Primary t a -> t a forall (t :: * -> *) a. Interpreted t => Primary t a -> t a unite (<$||=) :: (Covariant (->) (->) j, Interpreted u) => (Primary t a -> Primary u b) -> j := t a -> j := u b Primary t a -> Primary u b f <$||= j := t a x = (Primary t a -> Primary u b f (Primary t a -> Primary u b) -> t a -> u b forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (Primary t a -> Primary u b) -> t a -> u b ||=) (t a -> u b) -> (j := t a) -> j := u b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) -<$>- j := t a x (<$$||=) :: (Covariant (->) (->) j, Covariant (->) (->) k, Interpreted u) => (Primary t a -> Primary u b) -> j :. k := t a -> j :. k := u b Primary t a -> Primary u b f <$$||= (j :. k) := t a x = (Primary t a -> Primary u b f (Primary t a -> Primary u b) -> t a -> u b forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (Primary t a -> Primary u b) -> t a -> u b ||=) (t a -> u b) -> ((j :. k) := t a) -> (j :. k) := u b forall (t :: * -> *) (u :: * -> *) (category :: * -> * -> *) a b. (Covariant category category u, Covariant category category t) => category a b -> category (t (u a)) (t (u b)) -<$$>- (j :. k) := t a x (<$$$||=) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Interpreted u) => (Primary t a -> Primary u b) -> j :. k :. l := t a -> j :. k :. l := u b Primary t a -> Primary u b f <$$$||= (j :. (k :. l)) := t a x = (Primary t a -> Primary u b f (Primary t a -> Primary u b) -> t a -> u b forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (Primary t a -> Primary u b) -> t a -> u b ||=) (t a -> u b) -> ((j :. (k :. l)) := t a) -> (j :. (k :. l)) := u b forall (t :: * -> *) (u :: * -> *) (v :: * -> *) (category :: * -> * -> *) a b. (Covariant category category t, Covariant category category u, Covariant category category v) => category a b -> category (t (u (v a))) (t (u (v b))) -<$$$>- (j :. (k :. l)) := t a x (<$$$$||=) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Covariant (->) (->) m, Interpreted u) => (Primary t a -> Primary u b) -> j :. k :. l :. m := t a -> j :. k :. l :. m := u b Primary t a -> Primary u b f <$$$$||= (j :. (k :. (l :. m))) := t a x = (Primary t a -> Primary u b f (Primary t a -> Primary u b) -> t a -> u b forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (Primary t a -> Primary u b) -> t a -> u b ||=) (t a -> u b) -> ((j :. (k :. (l :. m))) := t a) -> (j :. (k :. (l :. m))) := u b forall (category :: * -> * -> *) (t :: * -> *) (u :: * -> *) (v :: * -> *) (w :: * -> *) a b. (Covariant category category t, Covariant category category u, Covariant category category v, Covariant category category w) => category a b -> category (t (u (v (w a)))) (t (u (v (w b)))) -<$$$$>- (j :. (k :. (l :. m))) := t a x (=||$>) :: (Covariant (->) (->) j, Interpreted u) => (t a -> u b) -> j := Primary t a -> j := Primary u b t a -> u b f =||$> j := Primary t a x = (t a -> u b f (t a -> u b) -> Primary t a -> Primary u b forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (t a -> u b) -> Primary t a -> Primary u b =||) (Primary t a -> Primary u b) -> (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) -<$>- j := Primary t a x (=||$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Interpreted u) => (t a -> u b) -> j :. k := Primary t a -> j :. k := Primary u b t a -> u b f =||$$> (j :. k) := Primary t a x = (t a -> u b f (t a -> u b) -> Primary t a -> Primary u b forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (t a -> u b) -> Primary t a -> Primary u b =||) (Primary t a -> Primary u b) -> ((j :. k) := Primary t a) -> (j :. k) := Primary u b forall (t :: * -> *) (u :: * -> *) (category :: * -> * -> *) a b. (Covariant category category u, Covariant category category t) => category a b -> category (t (u a)) (t (u b)) -<$$>- (j :. k) := Primary t a x (=||$$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Interpreted u) => (t a -> u b) -> j :. k :. l := Primary t a -> j :. k :. l := Primary u b t a -> u b f =||$$$> (j :. (k :. l)) := Primary t a x = (t a -> u b f (t a -> u b) -> Primary t a -> Primary u b forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (t a -> u b) -> Primary t a -> Primary u b =||) (Primary t a -> Primary u b) -> ((j :. (k :. l)) := Primary t a) -> (j :. (k :. l)) := Primary u b forall (t :: * -> *) (u :: * -> *) (v :: * -> *) (category :: * -> * -> *) a b. (Covariant category category t, Covariant category category u, Covariant category category v) => category a b -> category (t (u (v a))) (t (u (v b))) -<$$$>- (j :. (k :. l)) := Primary t a x (=||$$$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Covariant (->) (->) m, Interpreted u) => (t a -> u b) -> j :. k :. l :. m := Primary t a -> j :. k :. l :. m := Primary u b t a -> u b f =||$$$$> (j :. (k :. (l :. m))) := Primary t a x = (t a -> u b f (t a -> u b) -> Primary t a -> Primary u b forall (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (t a -> u b) -> Primary t a -> Primary u b =||) (Primary t a -> Primary u b) -> ((j :. (k :. (l :. m))) := Primary t a) -> (j :. (k :. (l :. m))) := Primary u b forall (category :: * -> * -> *) (t :: * -> *) (u :: * -> *) (v :: * -> *) (w :: * -> *) a b. (Covariant category category t, Covariant category category u, Covariant category category v, Covariant category category w) => category a b -> category (t (u (v (w a)))) (t (u (v (w b)))) -<$$$$>- (j :. (k :. (l :. m))) := Primary t a x (-=:) :: (Liftable (->) t, Interpreted (t u), Interpreted (t v), Covariant (->) (->) u) => (t u a -> t v b) -> u a -> Primary (t v) b -=: :: (t u a -> t v b) -> u a -> Primary (t v) b (-=:) t u a -> t v b f = t v b -> Primary (t v) b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (t v b -> Primary (t v) b) -> (u a -> t v b) -> u a -> Primary (t v) b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . t u a -> t v b f (t u a -> t v b) -> (u a -> t u a) -> u a -> t v b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . u a -> t u a forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *) a. (Liftable cat t, Covariant cat cat u) => cat (u a) (t u a) lift