Strength.hs

{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Profunctor strength for a monoidal action: @'Strong' t p@ lets @p@ absorb the action of @t@
-- via 'act', with 'MonStrong' the self-action (tensor) case; 'Costrong' is the dual, and a
-- 'TracedMonoidal' category is one whose hom-profunctor is costrong for its own tensor.
module Proarrow.Category.Monoidal.Strength where

import Data.Kind (Constraint)

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..), Tensor)
import Proarrow.Category.Monoidal.Action (Act, CoprodAction, MonoidalAction, ProdAction, actHom)
import Proarrow.Colimit.BinaryCoproduct (COPROD (..), HasBinaryCoproducts (..), swapCoprod)
import Proarrow.Core (CAT, CategoryOf (..), Hom, Kind, Profunctor (..), Promonad (..), obj, ($), type (+->))
import Proarrow.Profunctor.Corepresentable (Corepresentable (..), corepUniv)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Instance.Coproduct ((:+:) (..))
import Proarrow.Profunctor.Instance.Identity (Id (..))
import Proarrow.Profunctor.Instance.Product ((:*:) (..))
import Proarrow.Profunctor.Representable (Representable (..), repUniv)
import Proarrow.Tools.Laws (Law (..), Laws (..), ProLaw (..), ProLaws (..), (=:=), (===))

-- | Profunctorial strength for a monoidal action.
-- 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 @a (p :*: q) = act @t @_ @a p :*: act @t @_ @a q

instance (Strong t p, Strong t q) => Strong t (p :+: q) where
  act @a (InjL p) = InjL (act @t @_ @a p)
  act @a (InjR q) = InjR (act @t @_ @a q)

instance (MonoidalAction t) => Strong t (Id :: CAT k) where
  act @a (Id g) = Id (actHom @t (obj @a) g)

instance (Strong t p, Strong t q) => Strong t (p :.: q) where
  act @x (p :.: q) = act @t @_ @x p :.: act @t @_ @x q

instance (CategoryOf j, CategoryOf k) => Strong ProdAction (Prof :: CAT (j +-> k)) where
  act (Prof n) = Prof \(p :*: q) -> p :*: n q

-- | The laws of strength for the tensor acting on its own category: acting by the 'Unit' does
-- nothing and acting by a tensor is acting twice, up to the unitor and the associator, and 'act' is
-- natural in the element and dinatural in the acting object.
instance ProLaws (Strong Tensor) where
  proLaws =
    [ ProLaw "act unit" \ @p @a @b p _ _ -> p =:= dimap (leftUnitorInv @_ @a) (leftUnitor @_ @b) (act @Tensor @p @Unit p)
    , ProLaw "act tensor" \ @p @a @b @c @d p _ _ ->
        withOb2 @_ @c @d $
          act @Tensor @p @(c ** d) p
            =:= dimap (associator @_ @c @d @a) (associatorInv @_ @c @d @b) (act @Tensor @p @c (act @Tensor @p @d p))
    , ProLaw "act naturality" \ @p @a @b @c @d @e p morK morJ -> do
        g <- morK @c @a "g"
        h <- morJ @b @d "h"
        act @Tensor @p @e (dimap g h p) =:= dimap (obj @e ** g) (obj @e ** h) (act @Tensor @p @e p)
    , ProLaw "act dinaturality" \ @p @a @b @c @_ @e p morK _ -> do
        g <- morK @e @c "g"
        lmap (g ** obj @a) (act @Tensor @p @c p) =:= rmap (g ** obj @b) (act @Tensor @p @e p)
    ]

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 = index (act @t @p @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 = coindex (act @t @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' p = dimap (swap @k @a @c) (swap @k @c @b) (second' @c p) \\ p

second'
  :: forall {k} {p :: k +-> k} c a b. (MonStrong p, Ob c) => p a b -> p (c ** a) (c ** b)
second' p = act @Tensor @p @c 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' p = dimap (swapCoprod @a @c) (swapCoprod @c @b) (right' @_ @c p) \\ p

right' :: forall {k} (p :: k +-> k) c a b. (Strong CoprodAction p, Ob c) => p a b -> p (c || a) (c || b)
right' p = act @CoprodAction @p @(COPR c) 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 f g = second' @b g . first' @c f \\ f \\ g

strongId :: forall {k} {p :: k +-> k} a. (MonStrong p, MonoidalProfunctor p, Ob a) => p a a
strongId = dimap rightUnitorInv rightUnitor (second' @a 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 p = id @p @a ** 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 f x = let (u, y) = f (u, x) in y

instance (MonoidalAction t, Costrong t (Hom k)) => Costrong t (Id :: CAT k) where
  coact @a (Id g) = Id (coact @t @(Hom k) @a g)

-- | The laws of costrength for the tensor acting on its own category: 'coact' is natural in the
-- element and dinatural in the acting object (sliding), and coacting by the 'Unit' or by a tensor
-- is doing nothing or coacting twice (vanishing). An element with tensored endpoints is made from
-- the drawn element @p@ with arbitrary arrows into and out of it.
instance ProLaws (Costrong Tensor) where
  proLaws =
    [ ProLaw "coact unit" \ @p @a @b p _ _ ->
        withOb2 @_ @Unit @a $
          withOb2 @_ @Unit @b $
            p =:= coact @Tensor @p @Unit (dimap (leftUnitor @_ @a) (leftUnitorInv @_ @b) p)
    , ProLaw "coact tensor" \ @p @a @b @c @d @e @f p morK _ ->
        withOb2 @_ @c @e $
          withOb2 @_ @(c ** e) @d $
            withOb2 @_ @(c ** e) @f $
              withOb2 @_ @e @d $
                withOb2 @_ @e @f $
                  withOb2 @_ @c @(e ** d) $ withOb2 @_ @c @(e ** f) do
                    g <- morK @((c ** e) ** d) @a "g"
                    h <- morK @b @((c ** e) ** f) "h"
                    let q = dimap g h p
                    coact @Tensor @p @(c ** e) q
                      =:= coact @Tensor @p @e @d @f (coact @Tensor @p @c (dimap (associatorInv @_ @c @e @d) (associator @_ @c @e @f) q))
    , ProLaw "coact naturality" \ @p @a @b @c @d @e @f p morK _ ->
        withOb2 @_ @c @d $ withOb2 @_ @c @f $ withOb2 @_ @c @e do
          g <- morK @(c ** d) @a "g"
          h <- morK @b @(c ** f) "h"
          g' <- morK @e @d "g'"
          h' <- morK @f @e "h'"
          let q = dimap g h p
          coact @Tensor @p @c (dimap (obj @c ** g') (obj @c ** h') q) =:= dimap g' h' (coact @Tensor @p @c q)
    , ProLaw "coact sliding" \ @p @a @b @c @d @e @f p morK _ ->
        withOb2 @_ @c @d $ withOb2 @_ @c @f $ withOb2 @_ @e @d $ withOb2 @_ @e @f do
          g <- morK @(c ** d) @a "g"
          h <- morK @b @(e ** f) "h"
          k <- morK @e @c "k"
          let q = dimap g h p
          coact @Tensor @p @e @d @f (lmap (k ** obj @d) q) =:= coact @Tensor @p @c @d @f (rmap (k ** obj @f) q)
    ]

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 p = coact @Tensor @p @u @x @y (dimap (swap @k @u @x) (swap @k @y @u) p) \\ p

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

-- | The structures the laws of a traced monoidal category are stated for.
type TracedStructures :: [Kind -> Constraint]
type TracedStructures = '[Monoidal, SymMonoidal, TracedMonoidal]

-- | The trace laws, for 'trace' over @u@ of @f : x ** u ~> y ** u@: natural in @x@ and @y@,
-- dinatural in @u@ (sliding), trivial over the unit and iterated over a tensor (vanishing),
-- compatible with tensoring on the left (superposing), and the trace of a swap is the identity
-- (yanking).
instance Laws TracedStructures where
  laws =
    [ Law "naturality" \ @x @y @u @d @e mor -> withOb2 @_ @x @u $ withOb2 @_ @y @u $ withOb2 @_ @e @u $ withOb2 @_ @d @u do
        f <- mor @(x ** u) @(y ** u) "f"
        g <- mor @y @d "g"
        h <- mor @e @x "h"
        g . trace @(~>) @u @x @y f . h === trace @(~>) @u @e @d ((g ** obj @u) . f . (h ** obj @u))
    , Law "sliding" \ @x @y @u @v mor -> withOb2 @_ @x @u $ withOb2 @_ @y @u $ withOb2 @_ @x @v $ withOb2 @_ @y @v do
        f <- mor @(x ** v) @(y ** u) "f"
        g <- mor @u @v "g"
        trace @(~>) @u @x @y (f . (obj @x ** g)) === trace @(~>) @v @x @y ((obj @y ** g) . f)
    , Law "vanishing (unit)" \ @x @y mor -> withOb2 @_ @x @Unit $ withOb2 @_ @y @Unit do
        f <- mor @(x ** Unit) @(y ** Unit) "f"
        trace @(~>) @Unit @x @y f === rightUnitor @_ @y . f . rightUnitorInv @_ @x
    , Law "vanishing (tensor)" \ @x @y @u @v mor ->
        withOb2 @_ @u @v $
          withOb2 @_ @x @(u ** v) $
            withOb2 @_ @y @(u ** v) $
              withOb2 @_ @x @u $
                withOb2 @_ @y @u $
                  withOb2 @_ @(x ** u) @v $
                    withOb2 @_ @(y ** u) @v do
                      f <- mor @(x ** (u ** v)) @(y ** (u ** v)) "f"
                      trace @(~>) @(u ** v) @x @y f
                        === trace @(~>) @u @x @y (trace @(~>) @v @(x ** u) @(y ** u) (associatorInv @_ @y @u @v . f . associator @_ @x @u @v))
    , Law "superposing" \ @x @y @u @w mor ->
        withOb2 @_ @x @u $
          withOb2 @_ @y @u $
            withOb2 @_ @w @x $
              withOb2 @_ @w @y $
                withOb2 @_ @w @(x ** u) $
                  withOb2 @_ @w @(y ** u) do
                    f <- mor @(x ** u) @(y ** u) "f"
                    obj @w
                      ** trace @(~>) @u @x @y f
                      === trace @(~>) @u @(w ** x) @(w ** y) (associatorInv @_ @w @y @u . (obj @w ** f) . associator @_ @w @x @u)
    , Law "yanking" \ @u _ -> withOb2 @_ @u @u (obj @u === trace @(~>) @u @u @u (swap @_ @u @u))
    ]