module Pandora.Paradigm.Schemes.TU where

import Pandora.Core.Functor (type (:.), type (:=), type (~>))
import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Contravariant (Contravariant)
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable (hoist))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run))

newtype TU ct cu t u a = TU (t :. u := a)

type (<:.>) = TU Covariant Covariant
type (>:.>) = TU Contravariant Covariant
type (<:.<) = TU Covariant Contravariant
type (>:.<) = TU Contravariant Contravariant

instance Interpreted (TU ct cu t u) where
	type Primary (TU ct cu t u) a = t :. u := a
	run :: TU ct cu t u a -> Primary (TU ct cu t u) a
run ~(TU (t :. u) := a
x) = (t :. u) := a
Primary (TU ct cu t u) a
x

instance Pointable t => Liftable (TU Covariant Covariant t) where
	lift :: Covariant u => u ~> t <:.> u
	lift :: u ~> (t <:.> u)
lift = ((t :. u) := a) -> TU Covariant Covariant t u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((t :. u) := a) -> TU Covariant Covariant t u a)
-> (u a -> (t :. u) := a) -> u a -> TU Covariant Covariant t u a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. u a -> (t :. u) := a
forall (t :: * -> *) a. Pointable t => a |-> t
point

instance Extractable t => Lowerable (TU Covariant Covariant t) where
	lower :: t <:.> u ~> u
	lower :: (<:.>) t u a -> u a
lower (TU (t :. u) := a
x) = u a <-| t
forall (t :: * -> *) a. Extractable t => a <-| t
extract (t :. u) := a
x

instance Covariant t => Hoistable (TU Covariant Covariant t) where
	hoist :: u ~> v -> (t <:.> u ~> t <:.> v)
	hoist :: (u ~> v) -> (t <:.> u) ~> (t <:.> v)
hoist u ~> v
f (TU (t :. u) := a
x) = ((t :. v) := a) -> TU Covariant Covariant t v a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((t :. v) := a) -> TU Covariant Covariant t v a)
-> ((t :. v) := a) -> TU Covariant Covariant t v a
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ u a -> v a
u ~> v
f (u a -> v a) -> ((t :. u) := a) -> (t :. v) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (t :. u) := a
x