module Pandora.Paradigm.Schemes.TUT where import Pandora.Core.Functor (type (:.), type (:=), type (~>)) import Pandora.Pattern.Category (identity, (.), ($)) import Pandora.Pattern.Functor ((<*+>)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (<$$$>))) import Pandora.Pattern.Functor.Contravariant (Contravariant) import Pandora.Pattern.Functor.Applicative (Applicative ((<*>))) import Pandora.Pattern.Functor.Alternative (Alternative ((<+>))) 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.Bindable (Bindable ((>>=), ($>>=))) import Pandora.Pattern.Functor.Extendable (Extendable ((=>>), ($=>>))) import Pandora.Pattern.Functor.Distributive (Distributive ((>>-))) import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (|-))) import Pandora.Pattern.Transformer.Liftable (Liftable (lift)) import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower)) import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite)) newtype TUT ct ct' cu t t' u a = TUT (t :. u :. t' := a) infix 3 <:<.>:>, >:<.>:>, <:<.>:<, >:<.>:<, <:>.<:>, >:>.<:>, <:>.<:<, >:>.<:< type (<:<.>:>) = TUT Covariant Covariant Covariant type (>:<.>:>) = TUT Contravariant Covariant Covariant type (<:<.>:<) = TUT Covariant Covariant Contravariant type (>:<.>:<) = TUT Contravariant Covariant Contravariant type (<:>.<:>) = TUT Covariant Contravariant Covariant type (>:>.<:>) = TUT Contravariant Contravariant Covariant type (<:>.<:<) = TUT Covariant Contravariant Contravariant type (>:>.<:<) = TUT Contravariant Contravariant Contravariant instance Interpreted (TUT ct ct' cu t t' u) where type Primary (TUT ct ct' cu t t' u) a = t :. u :. t' := a run :: TUT ct ct' cu t t' u a -> Primary (TUT ct ct' cu t t' u) a run ~(TUT (t :. (u :. t')) := a x) = (t :. (u :. t')) := a Primary (TUT ct ct' cu t t' u) a x unite :: Primary (TUT ct ct' cu t t' u) a -> TUT ct ct' cu t t' u a unite = Primary (TUT ct ct' cu t t' u) a -> TUT ct ct' cu t t' u a forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT instance (Covariant t, Covariant t', Covariant u) => Covariant (t <:<.>:> t' := u) where a -> b f <$> :: (a -> b) -> (:=) (t <:<.>:> t') u a -> (:=) (t <:<.>:> t') u b <$> TUT (t :. (u :. t')) := a x = ((t :. (u :. t')) := b) -> (:=) (t <:<.>:> t') u b forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT (((t :. (u :. t')) := b) -> (:=) (t <:<.>:> t') u b) -> ((t :. (u :. t')) := b) -> (:=) (t <:<.>:> t') u b forall (m :: * -> * -> *). Category m => m ~~> m $ a -> b f (a -> b) -> ((t :. (u :. t')) := a) -> (t :. (u :. t')) := b forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b. (Covariant t, Covariant u, Covariant v) => (a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b <$$$> (t :. (u :. t')) := a x instance (Adjoint t' t, Bindable u) => Applicative (t <:<.>:> t' := u) where (:=) (t <:<.>:> t') u (a -> b) f <*> :: (:=) (t <:<.>:> t') u (a -> b) -> (:=) (t <:<.>:> t') u a -> (:=) (t <:<.>:> t') u b <*> (:=) (t <:<.>:> t') u a x = ((t :. (u :. t')) := b) -> (:=) (t <:<.>:> t') u b forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT (((t :. (u :. t')) := b) -> (:=) (t <:<.>:> t') u b) -> ((t :. (u :. t')) := b) -> (:=) (t <:<.>:> t') u b forall (m :: * -> * -> *). Category m => m ~~> m $ (u (t' (a -> b)) -> (t' (a -> b) -> u (t' b)) -> u (t' b) forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b >>= (t' (a -> b) -> ((a -> b) -> (t :. (u :. t')) := b) -> u (t' b) forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- ((a -> b) -> ((t :. (u :. t')) := a) -> (t :. (u :. t')) := b forall (t :: * -> *) (u :: * -> *) (v :: * -> *) a b. (Covariant t, Covariant u, Covariant v) => (a -> b) -> ((t :. (u :. v)) := a) -> (t :. (u :. v)) := b <$$$> (:=) (t <:<.>:> t') u a -> Primary ((t <:<.>:> t') := u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) (t <:<.>:> t') u a x))) (u (t' (a -> b)) -> u (t' b)) -> t (u (t' (a -> b))) -> (t :. (u :. t')) := b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> (:=) (t <:<.>:> t') u (a -> b) -> Primary ((t <:<.>:> t') := u) (a -> b) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) (t <:<.>:> t') u (a -> b) f instance (Applicative t, Covariant t', Alternative u) => Alternative (t <:<.>:> t' := u) where (:=) (t <:<.>:> t') u a x <+> :: (:=) (t <:<.>:> t') u a -> (:=) (t <:<.>:> t') u a -> (:=) (t <:<.>:> t') u a <+> (:=) (t <:<.>:> t') u a y = ((t :. (u :. t')) := a) -> (:=) (t <:<.>:> t') u a forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT (((t :. (u :. t')) := a) -> (:=) (t <:<.>:> t') u a) -> ((t :. (u :. t')) := a) -> (:=) (t <:<.>:> t') u a forall (m :: * -> * -> *). Category m => m ~~> m $ (:=) (t <:<.>:> t') u a -> Primary ((t <:<.>:> t') := u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) (t <:<.>:> t') u a x ((t :. (u :. t')) := a) -> ((t :. (u :. t')) := a) -> (t :. (u :. t')) := a forall (t :: * -> *) (u :: * -> *) a. (Applicative t, Alternative u) => ((t :. u) := a) -> ((t :. u) := a) -> (t :. u) := a <*+> (:=) (t <:<.>:> t') u a -> Primary ((t <:<.>:> t') := u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) (t <:<.>:> t') u a y instance (Pointable t, Applicative t, Covariant t', Avoidable u) => Avoidable (t <:<.>:> t' := u) where empty :: (:=) (t <:<.>:> t') u a empty = ((t :. (u :. t')) := a) -> (:=) (t <:<.>:> t') u a forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT (((t :. (u :. t')) := a) -> (:=) (t <:<.>:> t') u a) -> ((t :. (u :. t')) := a) -> (:=) (t <:<.>:> t') u a forall (m :: * -> * -> *). Category m => m ~~> m $ u (t' a) :=> t forall (t :: * -> *) a. Pointable t => a :=> t point u (t' a) forall (t :: * -> *) a. Avoidable t => t a empty instance (Pointable u, Adjoint t' t) => Pointable (t <:<.>:> t' := u) where point :: a :=> ((t <:<.>:> t') := u) point = ((t :. (u :. t')) := a) -> TUT Covariant Covariant Covariant t t' u a forall (t :: * -> *) a. Interpreted t => Primary t a -> t a unite (((t :. (u :. t')) := a) -> TUT Covariant Covariant Covariant t t' u a) -> (a -> (t :. (u :. t')) := a) -> a :=> ((t <:<.>:> t') := u) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a -> (t' a -> u (t' a)) -> (t :. (u :. t')) := a forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| t' a -> u (t' a) forall (t :: * -> *) a. Pointable t => a :=> t point) instance (Adjoint t' t, Bindable u) => Bindable (t <:<.>:> t' := u) where (:=) (t <:<.>:> t') u a x >>= :: (:=) (t <:<.>:> t') u a -> (a -> (:=) (t <:<.>:> t') u b) -> (:=) (t <:<.>:> t') u b >>= a -> (:=) (t <:<.>:> t') u b f = ((t :. (u :. t')) := b) -> (:=) (t <:<.>:> t') u b forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT (((t :. (u :. t')) := b) -> (:=) (t <:<.>:> t') u b) -> ((t :. (u :. t')) := b) -> (:=) (t <:<.>:> t') u b forall (m :: * -> * -> *). Category m => m ~~> m $ (:=) (t <:<.>:> t') u a -> Primary ((t <:<.>:> t') := u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) (t <:<.>:> t') u a x ((t :. (u :. t')) := a) -> (t' a -> u (t' b)) -> (t :. (u :. t')) := b forall (t :: * -> *) (u :: * -> *) a b. (Bindable t, Covariant u) => ((u :. t) := a) -> (a -> t b) -> (u :. t) := b $>>= (t' a -> (a -> (t :. (u :. t')) := b) -> u (t' b) forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (:=) (t <:<.>:> t') u b -> (t :. (u :. t')) := b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((:=) (t <:<.>:> t') u b -> (t :. (u :. t')) := b) -> (a -> (:=) (t <:<.>:> t') u b) -> a -> (t :. (u :. t')) := b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> (:=) (t <:<.>:> t') u b f) instance (Adjoint t' t, Extendable u) => Extendable (t' <:<.>:> t := u) where (:=) (t' <:<.>:> t) u a x =>> :: (:=) (t' <:<.>:> t) u a -> ((:=) (t' <:<.>:> t) u a -> b) -> (:=) (t' <:<.>:> t) u b =>> (:=) (t' <:<.>:> t) u a -> b f = ((t' :. (u :. t)) := b) -> (:=) (t' <:<.>:> t) u b forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT (((t' :. (u :. t)) := b) -> (:=) (t' <:<.>:> t) u b) -> ((t' :. (u :. t)) := b) -> (:=) (t' <:<.>:> t) u b forall (m :: * -> * -> *). Category m => m ~~> m $ (:=) (t' <:<.>:> t) u a -> Primary ((t' <:<.>:> t) := u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (:=) (t' <:<.>:> t) u a x ((t' :. (u :. t)) := a) -> (u (t a) -> t b) -> (t' :. (u :. t)) := b forall (t :: * -> *) (u :: * -> *) a b. (Extendable t, Covariant u) => ((u :. t) := a) -> (t a -> b) -> (u :. t) := b $=>> (u (t a) -> (((t' :. (u :. t)) := a) -> b) -> t b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (:=) (t' <:<.>:> t) u a -> b f ((:=) (t' <:<.>:> t) u a -> b) -> (((t' :. (u :. t)) := a) -> (:=) (t' <:<.>:> t) u a) -> ((t' :. (u :. t)) := a) -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((t' :. (u :. t)) := a) -> (:=) (t' <:<.>:> t) u a forall (t :: * -> *) a. Interpreted t => Primary t a -> t a unite) instance (Adjoint t t', Extractable u) => Extractable (t <:<.>:> t' := u) where extract :: a <:= ((t <:<.>:> t') := u) extract = (t (u (t' a)) -> (u (t' a) -> t' a) -> a forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- u (t' a) -> t' a forall (t :: * -> *) a. Extractable t => a <:= t extract) (t (u (t' a)) -> a) -> (TUT Covariant Covariant Covariant t t' u a -> t (u (t' a))) -> a <:= ((t <:<.>:> t') := u) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TUT Covariant Covariant Covariant t t' u a -> t (u (t' a)) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run instance (Adjoint t' t, Distributive t) => Liftable (t <:<.>:> t') where lift :: Covariant u => u ~> t <:<.>:> t' := u lift :: u ~> ((t <:<.>:> t') := u) lift u a x = ((t :. (u :. t')) := a) -> TUT Covariant Covariant Covariant t t' u a forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT (((t :. (u :. t')) := a) -> TUT Covariant Covariant Covariant t t' u a) -> ((t :. (u :. t')) := a) -> TUT Covariant Covariant Covariant t t' u a forall (m :: * -> * -> *). Category m => m ~~> m $ u a x u a -> (a -> t (t' a)) -> (t :. (u :. t')) := a forall (t :: * -> *) (u :: * -> *) a b. (Distributive t, Covariant u) => u a -> (a -> t b) -> (t :. u) := b >>- (a -> (t' a -> t' a) -> t (t' a) forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| t' a -> t' a forall (m :: * -> * -> *) a. Category m => m a a identity) instance (Adjoint t t', Distributive t') => Lowerable (t <:<.>:> t') where lower :: Covariant u => (t <:<.>:> t' := u) ~> u lower :: ((t <:<.>:> t') := u) ~> u lower (TUT (t :. (u :. t')) := a x) = (t :. (u :. t')) := a x ((t :. (u :. t')) := a) -> ((:.) u t' a -> t' (u a)) -> u a forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- ((:.) u t' a -> (t' a -> t' a) -> t' (u a) forall (t :: * -> *) (u :: * -> *) a b. (Distributive t, Covariant u) => u a -> (a -> t b) -> (t :. u) := b >>- t' a -> t' a forall (m :: * -> * -> *) a. Category m => m a a identity)