module Pandora.Paradigm.Schemes.UT where import Pandora.Core.Functor (type (:.), type (:=), type (~>)) import Pandora.Pattern.Semigroupoid ((.)) import Pandora.Pattern.Category (($), identity) import Pandora.Pattern.Functor.Covariant (Covariant, Covariant ((-<$>-)), (-<$$>-)) import Pandora.Pattern.Functor.Contravariant (Contravariant) import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (multiply)) import Pandora.Pattern.Functor.Monoidal (Monoidal (unit)) import Pandora.Pattern.Functor.Bindable (Bindable ((=<<))) import Pandora.Pattern.Functor.Traversable (Traversable ((<<-))) import Pandora.Pattern.Functor.Bivariant ((<->)) import Pandora.Pattern.Transformer.Liftable (Liftable (lift)) import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower)) import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite)) import Pandora.Paradigm.Primary.Algebraic.Exponential (type (<--)) import Pandora.Paradigm.Primary.Algebraic.One (One (One)) import Pandora.Paradigm.Primary.Algebraic ((:*:) ((:*:)), point, extract) import Pandora.Paradigm.Primary.Transformer.Flip (Flip (Flip)) newtype UT ct cu t u a = UT (u :. t := a) infixr 3 <.:>, >.:>, <.:<, >.:< type (<.:>) = UT Covariant Covariant type (>.:>) = UT Contravariant Covariant type (<.:<) = UT Covariant Contravariant type (>.:<) = UT Contravariant Contravariant instance Interpreted (UT ct cu t u) where type Primary (UT ct cu t u) a = u :. t := a run :: UT ct cu t u a -> Primary (UT ct cu t u) a run ~(UT (u :. t) := a x) = (u :. t) := a Primary (UT ct cu t u) a x unite :: Primary (UT ct cu t u) a -> UT ct cu t u a unite = Primary (UT ct cu t u) a -> UT ct cu t u a forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT instance (Covariant (->) (->) t, Covariant (->) (->) u) => Covariant (->) (->) (t <.:> u) where a -> b f -<$>- :: (a -> b) -> (<.:>) t u a -> (<.:>) t u b -<$>- (<.:>) t u a x = ((u :. t) := b) -> (<.:>) t u b forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT (((u :. t) := b) -> (<.:>) t u b) -> ((u :. t) := b) -> (<.:>) t u b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ a -> b f (a -> b) -> u (t a) -> (u :. t) := 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)) -<$$>- (<.:>) t u a -> Primary (t <.:> u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (<.:>) t u a x instance (Covariant (->) (->) u, Semimonoidal (->) (:*:) (:*:) t, Semimonoidal (->) (:*:) (:*:) u) => Semimonoidal (->) (:*:) (:*:) (t <.:> u) where multiply :: ((<.:>) t u a :*: (<.:>) t u b) -> (<.:>) t u (a :*: b) multiply (UT (u :. t) := a x :*: UT (u :. t) := b y) = ((u :. t) := (a :*: b)) -> (<.:>) t u (a :*: b) forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT (((u :. t) := (a :*: b)) -> (<.:>) t u (a :*: b)) -> ((u :. t) := (a :*: b)) -> (<.:>) t u (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ forall k (p :: * -> * -> *) (source :: * -> * -> *) (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k). Semimonoidal p source target t => p (source (t a) (t b)) (t (target a b)) forall (target :: * -> * -> *) (t :: * -> *) a b. Semimonoidal (->) (:*:) target t => (t a :*: t b) -> t (target a b) multiply @(->) @(:*:) ((t a :*: t b) -> t (a :*: b)) -> u (t a :*: t b) -> (u :. t) := (a :*: b) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) -<$>- (((u :. t) := a) :*: ((u :. t) := b)) -> u (t a :*: t b) forall k (p :: * -> * -> *) (source :: * -> * -> *) (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k). Semimonoidal p source target t => p (source (t a) (t b)) (t (target a b)) multiply ((u :. t) := a x ((u :. t) := a) -> ((u :. t) := b) -> ((u :. t) := a) :*: ((u :. t) := b) forall s a. s -> a -> s :*: a :*: (u :. t) := b y) instance (Covariant (->) (->) t, Covariant (->) (->) u, Semimonoidal (->) (:*:) (:*:) u, Monoidal (->) (->) (:*:) (:*:) t, Monoidal (->) (->) (:*:) (:*:) u) => Monoidal (->) (->) (:*:) (:*:) (t <.:> u) where unit :: Proxy (:*:) -> (Unit (:*:) -> a) -> (<.:>) t u a unit Proxy (:*:) _ Unit (:*:) -> a f = ((u :. t) := a) -> (<.:>) t u a forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT (((u :. t) := a) -> (<.:>) t u a) -> (a -> (u :. t) := a) -> a -> (<.:>) t u a forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . t a -> (u :. t) := a forall (t :: * -> *) a. Monoidal (->) (->) (:*:) (:*:) t => a -> t a point (t a -> (u :. t) := a) -> (a -> t a) -> a -> (u :. t) := a forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> t a forall (t :: * -> *) a. Monoidal (->) (->) (:*:) (:*:) t => a -> t a point (a -> (<.:>) t u a) -> a -> (<.:>) t u a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ Unit (:*:) -> a f One Unit (:*:) One instance (Traversable (->) (->) t, Bindable (->) t, Semimonoidal (->) (:*:) (:*:) u, Monoidal (->) (->) (:*:) (:*:) u, Bindable (->) u) => Bindable (->) (t <.:> u) where a -> (<.:>) t u b f =<< :: (a -> (<.:>) t u b) -> (<.:>) t u a -> (<.:>) t u b =<< UT (u :. t) := a x = ((u :. t) := b) -> (<.:>) t u b forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT (((u :. t) := b) -> (<.:>) t u b) -> ((u :. t) := b) -> (<.:>) t u b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ ((t b -> t b forall (m :: * -> * -> *) a. Category m => m a a identity (t b -> t b) -> t (t b) -> t b forall (source :: * -> * -> *) (t :: * -> *) a b. Bindable source t => source a (t b) -> source (t a) (t b) =<<) (t (t b) -> t b) -> u (t (t b)) -> (u :. t) := b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) -<$>-) (u (t (t b)) -> (u :. t) := b) -> (t a -> u (t (t b))) -> t a -> (u :. t) := b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . ((<.:>) t u b -> (u :. t) := b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<.:>) t u b -> (u :. t) := b) -> (a -> (<.:>) t u b) -> a -> (u :. t) := b forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> (<.:>) t u b f (a -> (u :. t) := b) -> t a -> u (t (t b)) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Traversable source target t, Covariant source target u, Monoidal source target (:*:) (:*:) u) => source a (u b) -> target (t a) (u (t b)) <<-) (t a -> (u :. t) := b) -> ((u :. t) := a) -> (u :. t) := b forall (source :: * -> * -> *) (t :: * -> *) a b. Bindable source t => source a (t b) -> source (t a) (t b) =<< (u :. t) := a x instance (Covariant (->) (->) u, Semimonoidal (<--) (:*:) (:*:) t, Semimonoidal (<--) (:*:) (:*:) u) => Semimonoidal (<--) (:*:) (:*:) (t <.:> u) where multiply :: ((<.:>) t u a :*: (<.:>) t u b) <-- (<.:>) t u (a :*: b) multiply = ((<.:>) t u (a :*: b) -> (<.:>) t u a :*: (<.:>) t u b) -> ((<.:>) t u a :*: (<.:>) t u b) <-- (<.:>) t u (a :*: b) forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip (((<.:>) t u (a :*: b) -> (<.:>) t u a :*: (<.:>) t u b) -> ((<.:>) t u a :*: (<.:>) t u b) <-- (<.:>) t u (a :*: b)) -> ((<.:>) t u (a :*: b) -> (<.:>) t u a :*: (<.:>) t u b) -> ((<.:>) t u a :*: (<.:>) t u b) <-- (<.:>) t u (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ \(UT (u :. t) := (a :*: b) xys) -> let Flip u (a :*: b) -> u a :*: u b f = forall k (p :: * -> * -> *) (source :: * -> * -> *) (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k). Semimonoidal p source target t => p (source (t a) (t b)) (t (target a b)) forall (t :: * -> *) a b. Semimonoidal (<--) (:*:) (:*:) t => (t a :*: t b) <-- t (a :*: b) multiply @(<--) @(:*:) @(:*:) in let Flip t (a :*: b) -> t a :*: t b g = forall k (p :: * -> * -> *) (source :: * -> * -> *) (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k). Semimonoidal p source target t => p (source (t a) (t b)) (t (target a b)) forall (t :: * -> *) a b. Semimonoidal (<--) (:*:) (:*:) t => (t a :*: t b) <-- t (a :*: b) multiply @(<--) @(:*:) @(:*:) in (((u :. t) := a) -> (<.:>) t u a forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT (((u :. t) := a) -> (<.:>) t u a) -> (u (t b) -> (<.:>) t u b) -> (((u :. t) := a) :*: u (t b)) -> (<.:>) t u a :*: (<.:>) t u b forall (left :: * -> * -> *) (right :: * -> * -> *) (target :: * -> * -> *) (v :: * -> * -> *) a b c d. Bivariant left right target v => left a b -> right c d -> target (v a c) (v b d) <-> u (t b) -> (<.:>) t u b forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT) ((((u :. t) := a) :*: u (t b)) -> (<.:>) t u a :*: (<.:>) t u b) -> (((u :. t) := a) :*: u (t b)) -> (<.:>) t u a :*: (<.:>) t u b forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ u (t a :*: t b) -> ((u :. t) := a) :*: u (t b) forall a b. u (a :*: b) -> u a :*: u b f (t (a :*: b) -> t a :*: t b forall a b. t (a :*: b) -> t a :*: t b g (t (a :*: b) -> t a :*: t b) -> ((u :. t) := (a :*: b)) -> u (t a :*: t b) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) -<$>- (u :. t) := (a :*: b) xys) where instance (Covariant (->) (->) u, Monoidal (<--) (->) (:*:) (:*:) t, Monoidal (<--) (->) (:*:) (:*:) u) => Monoidal (<--) (->) (:*:) (:*:) (t <.:> u) where unit :: Proxy (:*:) -> (Unit (:*:) -> a) <-- (<.:>) t u a unit Proxy (:*:) _ = ((<.:>) t u a -> One -> a) -> Flip (->) (One -> a) ((<.:>) t u a) forall (v :: * -> * -> *) a e. v e a -> Flip v a e Flip (((<.:>) t u a -> One -> a) -> Flip (->) (One -> a) ((<.:>) t u a)) -> ((<.:>) t u a -> One -> a) -> Flip (->) (One -> a) ((<.:>) t u a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ \(UT (u :. t) := a x) -> (\One _ -> t a -> a forall (t :: * -> *) a. Extractable_ t => t a -> a extract (t a -> a) -> t a -> a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ ((u :. t) := a) -> t a forall (t :: * -> *) a. Extractable_ t => t a -> a extract (u :. t) := a x) instance Monoidal (->) (->) (:*:) (:*:) t => Liftable (->) (UT Covariant Covariant t) where lift :: Covariant (->) (->) u => u ~> t <.:> u lift :: u ~> (t <.:> u) lift u a x = ((u :. t) := a) -> UT Covariant Covariant t u a forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT (((u :. t) := a) -> UT Covariant Covariant t u a) -> ((u :. t) := a) -> UT Covariant Covariant t u a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ a -> t a forall (t :: * -> *) a. Monoidal (->) (->) (:*:) (:*:) t => a -> t a point (a -> t a) -> u a -> (u :. t) := a forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) -<$>- u a x instance Monoidal (<--) (->) (:*:) (:*:) t => Lowerable (->) (UT Covariant Covariant t) where lower :: Covariant (->) (->) u => t <.:> u ~> u lower :: (t <.:> u) ~> u lower (UT (u :. t) := a x) = t a -> a forall (t :: * -> *) a. Extractable_ t => t a -> a extract (t a -> a) -> ((u :. t) := a) -> u a forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) -<$>- (u :. t) := a x