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