module Pandora.Paradigm.Controlflow.Effect.Interpreted where import Pandora.Core.Functor (type (:.), type (:=)) import Pandora.Pattern.Category ((.)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (<$$>), (<$$$>), (<$$$$>)), Covariant_) import Pandora.Pattern.Transformer.Liftable (Liftable (lift)) import Pandora.Paradigm.Primary.Functor.Function () 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. Category 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. Category 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. Category 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. Category 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 (t :: * -> *) a b. Covariant t => (a -> b) -> 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 :: * -> *) a b. (Covariant t, Covariant u) => (a -> b) -> ((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 :: * -> *) a b. (Covariant t, Covariant u, Covariant v) => (a -> b) -> ((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 (t :: * -> *) (u :: * -> *) (v :: * -> *) (w :: * -> *) a b. (Covariant t, Covariant u, Covariant v, Covariant w) => (a -> b) -> ((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 (t :: * -> *) a b. Covariant t => (a -> b) -> 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 :: * -> *) a b. (Covariant t, Covariant u) => (a -> b) -> ((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 :: * -> *) a b. (Covariant t, Covariant u, Covariant v) => (a -> b) -> ((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 (t :: * -> *) (u :: * -> *) (v :: * -> *) (w :: * -> *) a b. (Covariant t, Covariant u, Covariant v, Covariant w) => (a -> b) -> ((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, 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. Category 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. Category m => m b c -> m a b -> m a c . u a -> t u a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant_ u (->) (->)) => u ~> t u lift