{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Schemes.T_U where

import Pandora.Core.Functor (type (>>>>>>))
import Pandora.Core.Interpreted (Interpreted (Primary, run, unite, (=#-), (-#=)))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Morphism.Flip (Flip)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|-|-)))
import Pandora.Pattern.Functor.Contravariant (Contravariant ((>-|-|-)))
import Pandora.Paradigm.Algebraic.Exponential ()

newtype T_U ct cu p t u a = T_U (p (t a) (u a))

infixr 5 <:.:>, >:.:>, <:.:<, >:.:<

type (<:.:>) t u p = T_U Covariant Covariant p t u
type (>:.:>) t u p = T_U Contravariant Covariant p t u
type (<:.:<) t u p = T_U Covariant Contravariant p t u
type (>:.:<) t u p = T_U Contravariant Contravariant p t u

instance Interpreted (->) (T_U ct cu p t u) where
	type Primary (T_U ct cu p t u) a = p (t a) (u a)
	run :: ((->) < T_U ct cu p t u a) < Primary (T_U ct cu p t u) a
run ~(T_U p (t a) (u a)
x) = p (t a) (u a)
Primary (T_U ct cu p t u) a
x
	unite :: ((->) < Primary (T_U ct cu p t u) a) < T_U ct cu p t u a
unite = ((->) < Primary (T_U ct cu p t u) a) < T_U ct cu p t u a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U

-- TODO: generalize over (->)
instance (forall i . Covariant (->) (->) (p i), forall o . Covariant (->) (->) (Flip p o), Covariant (->) (->) t, Covariant (->) (->) u) => Covariant (->) (->) (t <:.:> u >>>>>> p) where
	a -> b
f <-|- :: (a -> b) -> (>>>>>>) (t <:.:> u) p a -> (>>>>>>) (t <:.:> u) p b
<-|- (>>>>>>) (t <:.:> u) p a
x = ((((->) < Flip p (u b) (t a)) < Flip p (u b) (t b))
-> ((->) < Primary (Flip p (u b)) (t a))
   < Primary (Flip p (u b)) (t b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @_ @(Flip _ _) ((a -> b) -> ((->) < Flip p (u b) (t a)) < Flip p (u b) (t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
(<-|-|-) a -> b
f) (p (t a) (u b) -> p (t b) (u b))
-> (p (t a) (u a) -> p (t a) (u b))
-> p (t a) (u a)
-> p (t b) (u b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((a -> b) -> p (t a) (u a) -> p (t a) (u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
(<-|-|-) a -> b
f)) (Primary ((t <:.:> u) >>>>>> p) a
 -> Primary ((t <:.:> u) >>>>>> p) b)
-> (>>>>>>) (t <:.:> u) p a -> (>>>>>>) (t <:.:> u) p b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#- (>>>>>>) (t <:.:> u) p a
x

-- TODO: generalize over (->)
instance (Contravariant (->) (->) t, forall a . Covariant (->) (->) (p (t a)), Covariant (->) (->) u, forall b . Contravariant (->) (->) (Flip p (u b))) => Covariant (->) (->) (t >:.:> u >>>>>> p) where
	<-|- :: (a -> b) -> (>>>>>>) (t >:.:> u) p a -> (>>>>>>) (t >:.:> u) p b
(<-|-) a -> b
f = (((->) < Primary ((t >:.:> u) >>>>>> p) a)
 < Primary ((t >:.:> u) >>>>>> p) b)
-> (>>>>>>) (t >:.:> u) p a -> (>>>>>>) (t >:.:> u) p b
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
(=#-) ((((->) < Flip p (u b) (t a)) < Flip p (u b) (t b))
-> ((->) < Primary (Flip p (u b)) (t a))
   < Primary (Flip p (u b)) (t b)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < t a) < u b) -> (m < Primary t a) < Primary u b
(-#=) @_ @(Flip _ _) ((a -> b) -> ((->) < Flip p (u b) (t a)) < Flip p (u b) (t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Contravariant source target t,
 Contravariant source (Betwixt source target) u,
 Contravariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
(>-|-|-) a -> b
f) (p (t a) (u b) -> p (t b) (u b))
-> (p (t a) (u a) -> p (t a) (u b))
-> p (t a) (u a)
-> p (t b) (u b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((a -> b) -> p (t a) (u a) -> p (t a) (u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Covariant source target t,
 Covariant source (Betwixt source target) u,
 Covariant (Betwixt source target) target t) =>
source a b -> target (t (u a)) (t (u b))
(<-|-|-) a -> b
f))