{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Strength where

import Data.Kind (Constraint)

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), Tensor)
import Proarrow.Category.Monoidal.Action (Act, CoprodAction, MonoidalAction, actHom)
import Proarrow.Colimit.BinaryCoproduct (COPROD (..), HasBinaryCoproducts (..), swapCoprod)
import Proarrow.Core (CAT, CategoryOf (..), Hom, Profunctor (..), Promonad (..), obj, type (+->))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), corepUniv)
import Proarrow.Profunctor.Instance.Coproduct ((:+:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Product ((:*:) (..))
import Proarrow.Profunctor.Representable (Representable (..), repUniv)

-- | Profuntorial strength for a monoidal actions.
-- Gives functorial strength for representable profunctors,
-- and functorial costrength for corepresentable profunctors.
type Strong :: forall {m} {k}. (m, k) +-> k -> k +-> k -> Constraint
class (MonoidalAction t, Profunctor p) => Strong t p where
  act :: (Ob a) => p x y -> p (Act t a x) (Act t a y)

instance (Strong t p, Strong t q) => Strong t (p :*: q) where
  act :: forall (a :: m) (x :: j) (y :: j).
Ob a =>
(:*:) p q x y -> (:*:) p q (Act t a x) (Act t a y)
act @a (p x y
p :*: q x y
q) = forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, j) +-> j) (p :: j +-> j) (a :: m) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @_ @a p x y
p p (t % '(a, x)) (t % '(a, y))
-> q (t % '(a, x)) (t % '(a, y))
-> (:*:) p q (t % '(a, x)) (t % '(a, y))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> q a b -> (:*:) p q a b
:*: forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, j) +-> j) (p :: j +-> j) (a :: m) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @_ @a q x y
q

instance (Strong t p, Strong t q) => Strong t (p :+: q) where
  act :: forall (a :: m) (x :: j) (y :: j).
Ob a =>
(:+:) p q x y -> (:+:) p q (Act t a x) (Act t a y)
act @a (InjL p x y
p) = p (t % '(a, x)) (t % '(a, y))
-> (:+:) p q (t % '(a, x)) (t % '(a, y))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) (q :: j +-> k).
p a b -> (:+:) p q a b
InjL (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, j) +-> j) (p :: j +-> j) (a :: m) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @_ @a p x y
p)
  act @a (InjR q x y
q) = q (t % '(a, x)) (t % '(a, y))
-> (:+:) p q (t % '(a, x)) (t % '(a, y))
forall {j} {k} (q :: j +-> k) (a :: k) (b :: j) (p :: j +-> k).
q a b -> (:+:) p q a b
InjR (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, j) +-> j) (p :: j +-> j) (a :: m) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @_ @a q x y
q)

instance (MonoidalAction t) => Strong t (Id :: CAT k) where
  act :: forall (a :: m) (x :: k) (y :: k).
Ob a =>
Id x y -> Id (Act t a x) (Act t a y)
act @a (Id x ~> y
g) = ((t % '(a, x)) ~> (t % '(a, y))) -> Id (t % '(a, x)) (t % '(a, y))
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (forall {m} {k} (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k)
       (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
forall (t :: (m, k) +-> k) (a :: m) (b :: m) (x :: k) (y :: k).
Representable t =>
(a ~> b) -> (x ~> y) -> Act t a x ~> Act t b y
actHom @t (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) x ~> y
g)

type MonStrong (p :: k +-> k) = (Strong Tensor p, SymMonoidal k)

-- | If a strong profunctor is representable, we get the usual strength for the representing functor.
strength
  :: forall {m} t p a b. (Representable p, Strong t p, Ob (a :: m), Ob b) => Act t a (p % b) ~> p % Act t a b
strength :: forall {k} {m} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m)
       (b :: k).
(Representable p, Strong t p, Ob a, Ob b) =>
Act t a (p % b) ~> (p % Act t a b)
strength = p (t % '(a, p % b)) (t % '(a, b))
-> (t % '(a, p % b)) ~> (p % (t % '(a, b)))
forall (a :: k) (b :: k). p a b -> a ~> (p % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @p @a (forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
forall (p :: k +-> k) (a :: k).
(Representable p, Ob a) =>
p (p % a) a
repUniv @p @b))

-- | If a strong profunctor is corepresentable, we get the usual costrength for the representing functor.
costrength
  :: forall {m} t p a b. (Corepresentable p, Strong t p, Ob (a :: m), Ob b) => p %% Act t a b ~> Act t a (p %% b)
costrength :: forall {j} {m} (t :: (m, j) +-> j) (p :: j +-> j) (a :: m)
       (b :: j).
(Corepresentable p, Strong t p, Ob a, Ob b) =>
(p %% Act t a b) ~> Act t a (p %% b)
costrength = p (t % '(a, b)) (t % '(a, p %% b))
-> (p %% (t % '(a, b))) ~> (t % '(a, p %% b))
forall (a :: j) (b :: j). p a b -> (p %% a) ~> b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Corepresentable p =>
p a b -> (p %% a) ~> b
coindex (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (m, j) +-> j) (p :: j +-> j) (a :: m) (x :: j)
       (y :: j).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @t @p @a (forall {j} {k} (p :: j +-> k) (a :: k).
(Corepresentable p, Ob a) =>
p a (p %% a)
forall (p :: j +-> j) (a :: j).
(Corepresentable p, Ob a) =>
p a (p %% a)
corepUniv @p @b))

first'
  :: forall {k} {p :: k +-> k} c a b. (MonStrong p, Ob c) => p a b -> p (a ** c) (b ** c)
first' :: forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (a ** c) (b ** c)
first' p a b
p = ((a ** c) ~> (c ** a))
-> ((c ** b) ~> (b ** c))
-> p (c ** a) (c ** b)
-> p (a ** c) (b ** c)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @c) (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @c @b) (forall (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
second' @c p a b
p) ((Ob a, Ob b) => p (a ** c) (b ** c))
-> p a b -> p (a ** c) (b ** c)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

second'
  :: forall {k} {p :: k +-> k} c a b. (MonStrong p, Ob c) => p a b -> p (c ** a) (c ** b)
second' :: forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
second' p a b
p = forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (k, k) +-> k) (p :: k +-> k) (a :: k) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @Tensor @p @c p a b
p

left'
  :: forall {k} (p :: k +-> k) c a b. (Strong CoprodAction p, HasBinaryCoproducts k, Ob c) => p a b -> p (a || c) (b || c)
left' :: forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k).
(Strong CoprodAction p, HasBinaryCoproducts k, Ob c) =>
p a b -> p (a || c) (b || c)
left' p a b
p = ((a || c) ~> (c || a))
-> ((c || b) ~> (b || c))
-> p (c || a) (c || b)
-> p (a || c) (b || c)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
forall {k} (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapCoprod @a @c) (forall (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
forall {k} (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
(a || b) ~> (b || a)
swapCoprod @c @b) (forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k).
(Strong CoprodAction p, Ob c) =>
p a b -> p (c || a) (c || b)
forall (p :: k +-> k) (c :: k) (a :: k) (b :: k).
(Strong CoprodAction p, Ob c) =>
p a b -> p (c || a) (c || b)
right' @_ @c p a b
p) ((Ob a, Ob b) => p (a || c) (b || c))
-> p a b -> p (a || c) (b || c)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

right' :: forall {k} (p :: k +-> k) c a b. (Strong CoprodAction p, Ob c) => p a b -> p (c || a) (c || b)
right' :: forall {k} (p :: k +-> k) (c :: k) (a :: k) (b :: k).
(Strong CoprodAction p, Ob c) =>
p a b -> p (c || a) (c || b)
right' p a b
p = forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
forall (t :: (COPROD k, k) +-> k) (p :: k +-> k) (a :: COPROD k)
       (x :: k) (y :: k).
(Strong t p, Ob a) =>
p x y -> p (Act t a x) (Act t a y)
act @CoprodAction @p @(COPR c) p a b
p

-- | This is not monoidal ** but premonoidal, i.e. no sliding.
-- So with `premon f g` the effects of f happen before the effects of g.
-- p needs to be a commutative promonad for this to be monoidal **.
premon
  :: forall {k} {p :: CAT k} a b c d. (MonStrong p, Promonad p) => p a b -> p c d -> p (a ** c) (b ** d)
premon :: forall {k} {p :: CAT k} (a :: k) (b :: k) (c :: k) (d :: k).
(MonStrong p, Promonad p) =>
p a b -> p c d -> p (a ** c) (b ** d)
premon p a b
f p c d
g = forall (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
second' @b p c d
g p (b ** c) (b ** d) -> p (a ** c) (b ** c) -> p (a ** c) (b ** d)
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k} (p :: k +-> k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (a ** c) (b ** c)
forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (a ** c) (b ** c)
first' @c p a b
f ((Ob a, Ob b) => p (a ** c) (b ** d))
-> p a b -> p (a ** c) (b ** d)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
f ((Ob c, Ob d) => p (a ** c) (b ** d))
-> p c d -> p (a ** c) (b ** d)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p c d
g

strongId :: forall {k} {p :: k +-> k} a. (MonStrong p, MonoidalProfunctor p, Ob a) => p a a
strongId :: forall {k} {p :: k +-> k} (a :: k).
(MonStrong p, MonoidalProfunctor p, Ob a) =>
p a a
strongId = (a ~> (a ** Unit))
-> ((a ** Unit) ~> a) -> p (a ** Unit) (a ** Unit) -> p a a
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap a ~> (a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv (a ** Unit) ~> a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor (forall (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
forall {k} {p :: k +-> k} (c :: k) (a :: k) (b :: k).
(MonStrong p, Ob c) =>
p a b -> p (c ** a) (c ** b)
second' @a p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one)

-- | A monoidal promonad is automatically strong.
monActDefault :: forall {p} a x y. (MonoidalProfunctor p, Promonad p, Ob a) => p x y -> p (a ** x) (a ** y)
monActDefault :: forall {k} {p :: k +-> k} (a :: k) (x :: k) (y :: k).
(MonoidalProfunctor p, Promonad p, Ob a) =>
p x y -> p (a ** x) (a ** y)
monActDefault p x y
p = forall {k} (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: k +-> k) (a :: k). (Promonad p, Ob a) => p a a
id @p @a p a a -> p x y -> p (a ** x) (a ** y)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** p x y
p

type Costrong :: forall {m} {k}. (m, k) +-> k -> k +-> k -> Constraint
class (MonoidalAction t, Profunctor p) => Costrong t p where
  coact :: forall a x y. (Ob a, Ob x, Ob y) => p (Act t a x) (Act t a y) -> p x y

instance Costrong Tensor (->) where
  coact :: forall a x y.
(Ob a, Ob x, Ob y) =>
(Act Tensor a x -> Act Tensor a y) -> x -> y
coact Act Tensor a x -> Act Tensor a y
f x
x = let (a
u, y
y) = Act Tensor a x -> Act Tensor a y
f (a
u, x
x) in y
y

instance (MonoidalAction t, Costrong t (Hom k)) => Costrong t (Id :: CAT k) where
  coact :: forall (a :: m) (x :: k) (y :: k).
(Ob a, Ob x, Ob y) =>
Id (Act t a x) (Act t a y) -> Id x y
coact @a (Id Act t a x ~> Act t a y
g) = (x ~> y) -> Id x y
forall k (a :: k) (b :: k). (a ~> b) -> Id a b
Id (forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
coact @t @(Hom k) @a Act t a x ~> Act t a y
g)

trace
  :: forall {k} (p :: k +-> k) u x y
   . (Costrong Tensor p, Ob x, Ob y, Ob u, SymMonoidal k) => p (x ** u) (y ** u) -> p x y
trace :: forall {k} (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(Costrong Tensor p, Ob x, Ob y, Ob u, SymMonoidal k) =>
p (x ** u) (y ** u) -> p x y
trace p (x ** u) (y ** u)
p = forall {m} {k} (t :: (m, k) +-> k) (p :: k +-> k) (a :: m) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
forall (t :: (k, k) +-> k) (p :: k +-> k) (a :: k) (x :: k)
       (y :: k).
(Costrong t p, Ob a, Ob x, Ob y) =>
p (Act t a x) (Act t a y) -> p x y
coact @Tensor @p @u @x @y (((u ** x) ~> (x ** u))
-> ((y ** u) ~> (u ** y))
-> p (x ** u) (y ** u)
-> p (u ** x) (u ** y)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @u @x) (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @y @u) p (x ** u) (y ** u)
p) ((Ob (x ** u), Ob (y ** u)) => p x y)
-> p (x ** u) (y ** u) -> p x y
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p (x ** u) (y ** u)
p

class (Costrong Tensor (Hom k), SymMonoidal k) => TracedMonoidal k
instance (Costrong Tensor (Hom k), SymMonoidal k) => TracedMonoidal k