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