module Pandora.Paradigm.Primary.Transformer.Kan where import Pandora.Pattern.Category ((.), ($)) import Pandora.Pattern.Functor.Contravariant (Contravariant ((>$<))) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>))) import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite)) import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right)) data family Kan (v :: * -> k) (t :: * -> *) (u :: * -> *) b a data instance Kan Left t u b a = Lan ((t b -> a) -> u b) instance Contravariant (Kan Left t u b) where a -> b f >$< :: (a -> b) -> Kan 'Left t u b b -> Kan 'Left t u b a >$< Lan x = ((t b -> a) -> u b) -> Kan 'Left t u b a forall (t :: * -> *) (u :: * -> *) b a. ((t b -> a) -> u b) -> Kan 'Left t u b a Lan (((t b -> a) -> u b) -> Kan 'Left t u b a) -> ((t b -> a) -> u b) -> Kan 'Left t u b a forall (m :: * -> * -> *). Category m => m ~~> m $ (t b -> b) -> u b x ((t b -> b) -> u b) -> ((t b -> a) -> t b -> b) -> (t b -> a) -> u b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a -> b f (a -> b) -> (t b -> a) -> t b -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c .) instance Interpreted (Kan Left t u b) where type Primary (Kan Left t u b) a = (t b -> a) -> u b run :: Kan 'Left t u b a -> Primary (Kan 'Left t u b) a run ~(Lan x) = Primary (Kan 'Left t u b) a (t b -> a) -> u b x unite :: Primary (Kan 'Left t u b) a -> Kan 'Left t u b a unite = Primary (Kan 'Left t u b) a -> Kan 'Left t u b a forall (t :: * -> *) (u :: * -> *) b a. ((t b -> a) -> u b) -> Kan 'Left t u b a Lan data instance Kan Right t u b a = Ran ((a -> t b) -> u b) instance Covariant (Kan Right t u b) where a -> b f <$> :: (a -> b) -> Kan 'Right t u b a -> Kan 'Right t u b b <$> Ran x = ((b -> t b) -> u b) -> Kan 'Right t u b b forall (t :: * -> *) (u :: * -> *) b a. ((a -> t b) -> u b) -> Kan 'Right t u b a Ran (((b -> t b) -> u b) -> Kan 'Right t u b b) -> ((b -> t b) -> u b) -> Kan 'Right t u b b forall (m :: * -> * -> *). Category m => m ~~> m $ (a -> t b) -> u b x ((a -> t b) -> u b) -> ((b -> t b) -> a -> t b) -> (b -> t b) -> u b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . ((b -> t b) -> (a -> b) -> a -> t b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> b f) instance Interpreted (Kan Right t u b) where type Primary (Kan Right t u b) a = (a -> t b) -> u b run :: Kan 'Right t u b a -> Primary (Kan 'Right t u b) a run ~(Ran x) = Primary (Kan 'Right t u b) a (a -> t b) -> u b x unite :: Primary (Kan 'Right t u b) a -> Kan 'Right t u b a unite = Primary (Kan 'Right t u b) a -> Kan 'Right t u b a forall (t :: * -> *) (u :: * -> *) b a. ((a -> t b) -> u b) -> Kan 'Right t u b a Ran