{-# LANGUAGE UndecidableInstances #-}

module Pandora.Paradigm.Primary.Transformer.Yoneda where

import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category (identity, ($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-)))
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.Algebraic.Exponential ()

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.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> b
f))

instance Pointable t (->) => Pointable (Yoneda t) (->) where
	point :: a -> Yoneda t a
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 b
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point (b -> t b) -> b -> t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> b
f a
x)

instance Extractable t (->) => Extractable (Yoneda t) (->) where
	extract :: Yoneda t a -> a
extract (Yoneda forall b. (a -> b) -> t b
f) = t a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (t a -> a) -> t a -> a
forall (m :: * -> * -> *) a b. Category m => 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 :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- u a
x)

instance (Extractable t (->), Pointable t (->), Extractable u (->) , Pointable u (->)) => Adjoint (Yoneda t) (Yoneda u) (->) (->) where
	Yoneda t a -> b
f -| :: (Yoneda t a -> b) -> a -> Yoneda u b
-| a
x = b -> Yoneda u b
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point (b -> Yoneda u b) -> (a -> b) -> a -> Yoneda u b
forall (m :: * -> * -> *) b c a.
Semigroupoid 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.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Yoneda t a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point (a -> Yoneda u b) -> a -> Yoneda u b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# a
x
	a -> Yoneda u b
g |- :: (a -> Yoneda u b) -> Yoneda t a -> b
|- Yoneda t a
x = Yoneda u b -> b
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Yoneda u b -> b)
-> (Yoneda t (Yoneda u b) -> Yoneda u b)
-> Yoneda t (Yoneda u b)
-> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Yoneda t (Yoneda u b) -> Yoneda u b
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Yoneda t (Yoneda u b) -> b) -> Yoneda t (Yoneda u b) -> b
forall (m :: * -> * -> *) a b. Category m => 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 :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant t source target =>
source a b -> target (t a) (t b)
-<$>- Yoneda t a
x