module Pandora.Paradigm.Primary.Transformer.Yoneda where import Pandora.Pattern.Category (identity, (.), ($), (#)) import Pandora.Pattern.Functor ((<*+>)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>))) import Pandora.Pattern.Functor.Alternative (Alternative ((<+>))) import Pandora.Pattern.Functor.Applicative (Applicative ((<*>))) 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.Adjoint (Adjoint ((-|), (|-))) import Pandora.Pattern.Transformer.Liftable (Liftable (lift)) import Pandora.Paradigm.Primary.Functor.Function ((!)) newtype Yoneda t a = Yoneda { Yoneda t a -> forall b. (a -> b) -> t b yoneda :: forall b . (a -> b) -> t b } instance Covariant (Yoneda t) where a -> b f <$> :: (a -> b) -> Yoneda t a -> Yoneda t b <$> Yoneda t a x = (forall b. (b -> b) -> t b) -> Yoneda t b forall (t :: * -> *) a. (forall b. (a -> b) -> t b) -> Yoneda t a Yoneda (\b -> b k -> Yoneda t a -> (a -> b) -> t b forall (t :: * -> *) a. Yoneda t a -> forall b. (a -> b) -> t b yoneda Yoneda t a x (b -> b k (b -> b) -> (a -> b) -> a -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> b f)) instance Alternative t => Alternative (Yoneda t) where Yoneda forall b. (a -> b) -> t b f <+> :: Yoneda t a -> Yoneda t a -> Yoneda t a <+> Yoneda forall b. (a -> b) -> t b g = (forall b. (a -> b) -> t b) -> Yoneda t a forall (t :: * -> *) a. (forall b. (a -> b) -> t b) -> Yoneda t a Yoneda (((->) (a -> b) :. t) := b forall b. (a -> b) -> t b f (((->) (a -> b) :. t) := b) -> (((->) (a -> b) :. t) := b) -> ((->) (a -> b) :. t) := b forall (t :: * -> *) (u :: * -> *) a. (Applicative t, Alternative u) => ((t :. u) := a) -> ((t :. u) := a) -> (t :. u) := a <*+> ((->) (a -> b) :. t) := b forall b. (a -> b) -> t b g) instance Applicative t => Applicative (Yoneda t) where Yoneda forall b. ((a -> b) -> b) -> t b f <*> :: Yoneda t (a -> b) -> Yoneda t a -> Yoneda t b <*> Yoneda forall b. (a -> b) -> t b x = (forall b. (b -> b) -> t b) -> Yoneda t b forall (t :: * -> *) a. (forall b. (a -> b) -> t b) -> Yoneda t a Yoneda (\b -> b g -> ((a -> b) -> a -> b) -> t (a -> b) forall b. ((a -> b) -> b) -> t b f (b -> b g (b -> b) -> (a -> b) -> a -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c .) t (a -> b) -> t a -> t b forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b <*> (a -> a) -> t a forall b. (a -> b) -> t b x a -> a forall (m :: * -> * -> *) a. Category m => m a a identity) instance Avoidable t => Avoidable (Yoneda t) where empty :: Yoneda t a empty = (forall b. (a -> b) -> t b) -> Yoneda t a forall (t :: * -> *) a. (forall b. (a -> b) -> t b) -> Yoneda t a Yoneda (t b forall (t :: * -> *) a. Avoidable t => t a empty t b -> (a -> b) -> t b forall a b. a -> b -> a !) instance Pointable t => Pointable (Yoneda t) where point :: a :=> Yoneda t point a x = (forall b. (a -> b) -> t b) -> Yoneda t a forall (t :: * -> *) a. (forall b. (a -> b) -> t b) -> Yoneda t a Yoneda (\a -> b f -> b :=> t forall (t :: * -> *) a. Pointable t => a :=> t point (b :=> t) -> b :=> t forall (m :: * -> * -> *). Category m => m ~~> m $ a -> b f a x) instance Extractable t => Extractable (Yoneda t) where extract :: a <:= Yoneda t extract (Yoneda forall b. (a -> b) -> t b f) = a <:= t forall (t :: * -> *) a. Extractable t => a <:= t extract (a <:= t) -> a <:= t forall (m :: * -> * -> *). Category m => m ~~> m $ (a -> a) -> t a forall b. (a -> b) -> t b f a -> a forall (m :: * -> * -> *) a. Category m => m a a identity instance Liftable Yoneda where lift :: u ~> Yoneda u lift u a x = (forall b. (a -> b) -> u b) -> Yoneda u a forall (t :: * -> *) a. (forall b. (a -> b) -> t b) -> Yoneda t a Yoneda ((a -> b) -> u a -> u b forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> u a x) instance (Extractable t, Pointable t, Extractable u, Pointable u) => Adjoint (Yoneda t) (Yoneda u) where a x -| :: a -> (Yoneda t a -> b) -> Yoneda u b -| Yoneda t a -> b f = b :=> Yoneda u forall (t :: * -> *) a. Pointable t => a :=> t point (b :=> Yoneda u) -> (a -> b) -> a -> Yoneda u b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Yoneda t a -> b f (Yoneda t a -> b) -> (a -> Yoneda t a) -> a -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Yoneda t a forall (t :: * -> *) a. Pointable t => a :=> t point (a -> Yoneda u b) -> a -> Yoneda u b forall (m :: * -> * -> *). Category m => m ~~> m # a x Yoneda t a x |- :: Yoneda t a -> (a -> Yoneda u b) -> b |- a -> Yoneda u b g = b <:= Yoneda u forall (t :: * -> *) a. Extractable t => a <:= t extract (b <:= Yoneda u) -> (Yoneda t (Yoneda u b) -> Yoneda u b) -> Yoneda t (Yoneda u b) -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Yoneda t (Yoneda u b) -> Yoneda u b forall (t :: * -> *) a. Extractable t => a <:= t extract (Yoneda t (Yoneda u b) -> b) -> Yoneda t (Yoneda u b) -> b forall (m :: * -> * -> *). Category m => m ~~> m # a -> Yoneda u b g (a -> Yoneda u b) -> Yoneda t a -> Yoneda t (Yoneda u b) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b <$> Yoneda t a x