module Pandora.Paradigm.Primary.Transformer.Yoneda where

import Pandora.Core.Morphism ((!))
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))

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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ (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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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