module Pandora.Paradigm.Primary.Transformer.Backwards where

import Pandora.Pattern.Category ((.), ($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>), (.#..)), Covariant_ ((-<$>-)))
import Pandora.Pattern.Functor.Contravariant (Contravariant ((>$<)))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Pointable (Pointable (point))
import Pandora.Pattern.Functor.Applicative (Semimonoidal (multiply))
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.Primary.Algebraic ((-<*>-))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%))
import Pandora.Paradigm.Controlflow.Effect.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 (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t a
x

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 (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
-<$>- t a
x

instance Pointable t (->) => Pointable (Backwards t) (->) where
	point :: a -> Backwards t a
point = t a -> Backwards t a
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (t a -> Backwards t a) -> (a -> t a) -> a -> Backwards t a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> t a
forall (t :: * -> *) (source :: * -> * -> *) a.
Pointable t source =>
source a (t a)
point

instance Extractable t (->) => Extractable (Backwards t) (->) where
	extract :: Backwards t a -> a
extract (Backwards t a
x) = t a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract t a
x

-- TODO: check that effects evaluation goes in opposite order
instance Semimonoidal t (:*:) (->) (->) => Semimonoidal (Backwards t) (:*:) (->) (->) where
	multiply :: ((a :*: b) -> r)
-> (Backwards t a :*: Backwards t b) -> Backwards t r
multiply (a :*: b) -> r
f (Backwards t a
x :*: Backwards t b
y) = t r -> Backwards t r
forall k (t :: k -> *) (a :: k). t a -> Backwards t a
Backwards (t r -> Backwards t r) -> t r -> Backwards t r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
#
		(a :*: b) -> r
f ((a :*: b) -> r)
-> (((->) b :. (->) a) := (a :*: b)) -> ((->) b :. (->) a) := r
forall (t :: * -> *) (v :: * -> * -> *) a c d b.
(Covariant t, t ~ v a, Category v) =>
v c d -> ((v a :. v b) := c) -> (v a :. v b) := d
.#.. (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) := r) -> t b -> t (a -> r)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
-<$>- t b
y t (a -> r) -> t a -> t r
forall a b (t :: * -> *).
Semimonoidal t (:*:) (->) (->) =>
t (a -> b) -> t a -> t b
-<*>- 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 (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) a b.
Covariant_ t source target =>
source a b -> target (t a) (t b)
-<$>- a -> u b
f (a -> u b) -> t a -> u (t b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) (u :: * -> *) a b.
(Traversable t source target, Covariant_ u source target,
 Pointable u target, Semimonoidal u (:*:) source target) =>
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 (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Backwards t b -> t b) -> (a -> Backwards t b) -> a -> t b
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> Backwards t b
f (a -> t b) -> u a -> t (u b)
forall (t :: * -> *) (source :: * -> * -> *)
       (target :: * -> * -> *) (u :: * -> *) a b.
(Distributive t source target, Covariant_ u source target) =>
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 (t :: * -> *) a b. Contravariant t => (a -> b) -> 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 ~> Backwards u
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 ~> u
lower = Backwards u a -> u a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

instance Hoistable Backwards where
	u ~> v
f /|\ :: (u ~> v) -> Backwards u ~> Backwards v
/|\ 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
u ~> v
f u a
x