module Pandora.Paradigm.Primary.Transformer.Backwards where

import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--)))
import Pandora.Pattern.Functor.Contravariant (Contravariant ((>-|-)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Traversable (Traversable ((<-/-)))
import Pandora.Pattern.Functor.Distributive (Distributive ((-<<), (--<<)))
import Pandora.Pattern.Transformer.Liftable (Liftable (lift))
import Pandora.Pattern.Transformer.Lowerable (Lowerable (lower))
import Pandora.Pattern.Transformer.Hoistable (Hoistable ((/|\)))
import Pandora.Paradigm.Algebraic ((<-*-))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Algebraic.Exponential (type (<--), type (-->), (%))
import Pandora.Paradigm.Algebraic.One (One (One))
import Pandora.Paradigm.Algebraic (point, extract, (<-||-))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Core.Interpreted (Interpreted (Primary, run, unite, (<~)))

newtype Backwards t a = Backwards (t a)

instance Covariant (->) (->) t => Covariant (->) (->) (Backwards t) where
	a -> b
f <-|- :: (a -> b) -> Backwards t a -> Backwards t b
<-|- Backwards t a
x = t b -> Backwards t b
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (t b -> Backwards t b) -> t b -> Backwards t b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- a -> b
f (a -> b) -> t a -> t b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t a
x

-- TODO: check that effects evaluation goes in opposite order
instance (Semimonoidal (-->) (:*:) (:*:) t, Covariant (->) (->) t) => Semimonoidal (-->) (:*:) (:*:) (Backwards t) where
	mult :: (Backwards t a :*: Backwards t b) --> Backwards t (a :*: b)
mult = ((Backwards t a :*: Backwards t b) -> Backwards t (a :*: b))
-> (Backwards t a :*: Backwards t b) --> Backwards t (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Backwards t a :*: Backwards t b) -> Backwards t (a :*: b))
 -> (Backwards t a :*: Backwards t b) --> Backwards t (a :*: b))
-> ((Backwards t a :*: Backwards t b) -> Backwards t (a :*: b))
-> (Backwards t a :*: Backwards t b) --> Backwards t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Backwards t a
x :*: Backwards t b
y) -> t (a :*: b) -> Backwards t (a :*: b)
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (t (a :*: b) -> Backwards t (a :*: b))
-> t (a :*: b) -> Backwards t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (a -> b -> a :*: b
forall s a. s -> a -> s :*: a
(:*:) (a -> b -> a :*: b) -> b -> a -> a :*: b
forall a b c. (a -> b -> c) -> b -> a -> c
%) (b -> a -> a :*: b) -> t b -> t (a -> a :*: b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- t b
y t (a -> a :*: b) -> t a -> t (a :*: b)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- t a
x

instance (Covariant (->) (->) t, Monoidal (-->) (-->) (:*:) (:*:) t) => Monoidal (-->) (-->) (:*:) (:*:) (Backwards t) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> Backwards t a
unit Proxy (:*:)
_ = (Straight (->) One a -> Backwards t a)
-> Straight (->) (Straight (->) One a) (Backwards t a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((Straight (->) One a -> Backwards t a)
 -> Straight (->) (Straight (->) One a) (Backwards t a))
-> (Straight (->) One a -> Backwards t a)
-> Straight (->) (Straight (->) One a) (Backwards t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- t a -> Backwards t a
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (t a -> Backwards t a)
-> (Straight (->) One a -> t a)
-> Straight (->) One a
-> Backwards t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> t a
forall (t :: * -> *) a. Pointable t => a -> t a
point (a -> t a)
-> (Straight (->) One a -> a) -> Straight (->) One a -> t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Straight (->) One a -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ One
One)

instance (Semimonoidal (<--) (:*:) (:*:) t, Covariant (->) (->) t) => Semimonoidal (<--) (:*:) (:*:) (Backwards t) where
	mult :: (Backwards t a :*: Backwards t b) <-- Backwards t (a :*: b)
mult = (Backwards t (a :*: b) -> Backwards t a :*: Backwards t b)
-> (Backwards t a :*: Backwards t b) <-- Backwards t (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Backwards t (a :*: b) -> Backwards t a :*: Backwards t b)
 -> (Backwards t a :*: Backwards t b) <-- Backwards t (a :*: b))
-> (Backwards t (a :*: b) -> Backwards t a :*: Backwards t b)
-> (Backwards t a :*: Backwards t b) <-- Backwards t (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (t a -> Backwards t a
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (t a -> Backwards t a)
-> (t a :*: Backwards t b) -> Backwards t a :*: Backwards t b
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Covariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p a c) (p b c)
<-||-) ((t a :*: Backwards t b) -> Backwards t a :*: Backwards t b)
-> (Backwards t (a :*: b) -> t a :*: Backwards t b)
-> Backwards t (a :*: b)
-> Backwards t a :*: Backwards t b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t b -> Backwards t b
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (t b -> Backwards t b) -> (t a :*: t b) -> t a :*: Backwards t b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) ((t a :*: t b) -> t a :*: Backwards t b)
-> (Backwards t (a :*: b) -> t a :*: t b)
-> Backwards t (a :*: b)
-> t a :*: Backwards t b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (forall k (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (t :: k -> *) (a :: k) (b :: k).
Semimonoidal p source target t =>
p (source (t a) (t b)) (t (target a b))
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Semimonoidal (<--) source target t =>
source (t a) (t b) <-- t (target a b)
mult @(<--) ((t a :*: t b) <-- t (a :*: b)) -> t (a :*: b) -> t a :*: t b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~) (t (a :*: b) -> t a :*: t b)
-> (Backwards t (a :*: b) -> t (a :*: b))
-> Backwards t (a :*: b)
-> t a :*: t b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Backwards t (a :*: b) -> t (a :*: b)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run

instance (Covariant (->) (->) t, Monoidal (<--) (-->) (:*:) (:*:) t) => Monoidal (<--) (-->) (:*:) (:*:) (Backwards t) where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- Backwards t a
unit Proxy (:*:)
_ = (Backwards t a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Backwards t a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Backwards t a -> Straight (->) One a)
 -> Flip (->) (Straight (->) One a) (Backwards t a))
-> (Backwards t a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Backwards t a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Backwards t a
x) -> (One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> t a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract t a
x)

instance Traversable (->) (->) t => Traversable (->) (->) (Backwards t) where
	a -> u b
f <-/- :: (a -> u b) -> Backwards t a -> u (Backwards t b)
<-/- Backwards t a
x = t b -> Backwards t b
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (t b -> Backwards t b) -> u (t b) -> u (Backwards t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- a -> u b
f (a -> u b) -> t a -> u (t b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<-/- t a
x

instance Distributive (->) (->) t => Distributive (->) (->) (Backwards t) where
	a -> Backwards t b
f -<< :: (a -> Backwards t b) -> u a -> Backwards t (u b)
-<< u a
x = t (u b) -> Backwards t (u b)
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (t (u b) -> Backwards t (u b)) -> t (u b) -> Backwards t (u b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Backwards t b -> t b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Backwards t b -> t b) -> (a -> Backwards t b) -> a -> t b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Backwards t b
f (a -> t b) -> u a -> t (u b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Distributive source target t, Covariant source target u) =>
source a (t b) -> target (u a) (t (u b))
-<< u a
x

instance Contravariant (->) (->) t => Contravariant (->) (->) (Backwards t) where
	a -> b
f >-|- :: (a -> b) -> Backwards t b -> Backwards t a
>-|- Backwards t b
x = t a -> Backwards t a
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (t a -> Backwards t a) -> t a -> Backwards t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- a -> b
f (a -> b) -> t b -> t a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
>-|- t b
x

instance Interpreted (->) (Backwards t) where
	type Primary (Backwards t) a = t a
	run :: ((->) < Backwards t a) < Primary (Backwards t) a
run ~(Backwards t a
x) = t a
Primary (Backwards t) a
x
	unite :: ((->) < Primary (Backwards t) a) < Backwards t a
unite = ((->) < Primary (Backwards t) a) < Backwards t a
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards

instance Liftable (->) Backwards where
	lift :: u a -> Backwards u a
lift = u a -> Backwards u a
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards

instance Lowerable (->) Backwards where
	lower :: Backwards u a -> u a
lower = Backwards u a -> u a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run

instance Hoistable (->) Backwards where
	forall a. u a -> v a
f /|\ :: (forall a. u a -> v a) -> forall a. Backwards u a -> Backwards v a
/|\ Backwards u a
x = v a -> Backwards v a
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (v a -> Backwards v a) -> v a -> Backwards v a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- u a -> v a
forall a. u a -> v a
f u a
x