{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Action where

import Data.Kind (Constraint)
import Prelude (type (~))

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CAT, CategoryOf (..), Kind, Profunctor (..), Promonad (..), obj, type (+->))

-- | Profuntorial strength for a monoidal action.
-- Gives functorial strength for Star, and functorial costrength for Costar.
type Strong :: forall {j} {k}. Kind -> j +-> k -> Constraint
class (MonoidalAction m c, MonoidalAction m d, Profunctor p) => Strong m (p :: c +-> d) where
  act :: forall (a :: m) b x y. a ~> b -> p x y -> p (Act a x) (Act b y)

class (Monoidal m, CategoryOf k, Strong m ((~>) :: CAT k)) => MonoidalAction m k where
  -- I would like to default Act to `**`, but that doesn't seem possible without GHC thinking `m` and `k` are the same.
  type Act (a :: m) (x :: k) :: k
  withObAct :: (Ob (a :: m), Ob (x :: k)) => ((Ob (Act a x)) => r) -> r
  unitor :: (Ob (x :: k)) => Act (Unit :: m) x ~> x
  unitorInv :: (Ob (x :: k)) => x ~> Act (Unit :: m) x
  multiplicator :: (Ob (a :: m), Ob (b :: m), Ob (x :: k)) => Act a (Act b x) ~> Act (a ** b) x
  multiplicatorInv :: (Ob (a :: m), Ob (b :: m), Ob (x :: k)) => Act (a ** b) x ~> Act a (Act b x)

class (Act a b ~ a ** b) => ActIsTensor a b
instance (Act a b ~ a ** b) => ActIsTensor a b
class (Act a (Act b c) ~ a ** (b ** c), a ** (Act b c) ~ a ** (b ** c), Act a (b ** c) ~ a ** (b ** c)) => ActIsTensor3 a b c
instance (Act a (Act b c) ~ a ** (b ** c), a ** (Act b c) ~ a ** (b ** c), Act a (b ** c) ~ a ** (b ** c)) => ActIsTensor3 a b c
class
  ( MonoidalAction k k
  , SymMonoidal k
  , forall (a :: k) (b :: k). ActIsTensor a b
  , forall (a :: k) (b :: k) (c :: k). ActIsTensor3 a b c
  ) =>
  SelfAction k
instance
  ( MonoidalAction k k
  , SymMonoidal k
  , forall (a :: k) (b :: k). ActIsTensor a b
  , forall (a :: k) (b :: k) (c :: k). ActIsTensor3 a b c
  )
  => SelfAction k

composeActs
  :: forall {m} {k} (x :: m) y (c :: k) a b
   . (MonoidalAction m k, Ob x, Ob y, Ob c)
  => a ~> Act x b
  -> b ~> Act y c
  -> a ~> Act (x ** y) c
composeActs :: forall {m} {k} (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(a ~> Act x b) -> (b ~> Act y c) -> a ~> Act (x ** y) c
composeActs a ~> Act x b
f b ~> Act y c
g = forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act a (Act b x) ~> Act (a ** b) x
multiplicator @m @k @x @y @c (Act x (Act y c) ~> Act (x ** y) c)
-> (a ~> Act x (Act y c)) -> a ~> Act (x ** y) c
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x ~> x) -> (b ~> Act y c) -> Act x b ~> Act x (Act y c)
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x) b ~> Act y c
g (Act x b ~> Act x (Act y c))
-> (a ~> Act x b) -> a ~> Act x (Act y c)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. a ~> Act x b
f

decomposeActs
  :: forall {m} {k} (x :: m) y (c :: k) a b
   . (MonoidalAction m k, Ob x, Ob y, Ob c)
  => Act y c ~> b
  -> Act x b ~> a
  -> Act (x ** y) c ~> a
decomposeActs :: forall {m} {k} (x :: m) (y :: m) (c :: k) (a :: k) (b :: k).
(MonoidalAction m k, Ob x, Ob y, Ob c) =>
(Act y c ~> b) -> (Act x b ~> a) -> Act (x ** y) c ~> a
decomposeActs Act y c ~> b
f Act x b ~> a
g = Act x b ~> a
g (Act x b ~> a)
-> (Act (x ** y) c ~> Act x b) -> Act (x ** y) c ~> a
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (x ~> x) -> (Act y c ~> b) -> Act x (Act y c) ~> Act x b
forall (a :: m) (b :: m) (x :: k) (y :: k).
(a ~> b) -> (x ~> y) -> Act a x ~> Act b y
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: m). (CategoryOf m, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @x) Act y c ~> b
f (Act x (Act y c) ~> Act x b)
-> (Act (x ** y) c ~> Act x (Act y c)) -> Act (x ** y) c ~> Act x b
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: PRO k k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall m k (a :: m) (b :: m) (x :: k).
(MonoidalAction m k, Ob a, Ob b, Ob x) =>
Act (a ** b) x ~> Act a (Act b x)
multiplicatorInv @m @k @x @y @c

first' :: forall {k} {p :: CAT k} c a b. (SelfAction k, Strong k p, Ob c) => p a b -> p (a ** c) (b ** c)
first' :: forall {k} {p :: CAT k} (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k 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 :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
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).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (c ** a) (c ** b)
forall {k} {p :: CAT k} (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k 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 :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

second' :: forall {k} {p :: CAT k} c a b. (SelfAction k, Strong k p, Ob c) => p a b -> p (c ** a) (c ** b)
second' :: forall {k} {p :: CAT k} (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (c ** a) (c ** b)
second' p a b
p = (c ~> c) -> p a b -> p (Act c a) (Act c b)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c) p a b
p

-- | This is not monoidal `par` but premonoidal, i.e. no sliding.
-- So with `prepar f g` the effects of f happen before the effects of g.
-- p needs to be a commutative promonad for this to be monoidal `par`.
prepar :: forall {k} {p :: CAT k} a b c d. (SelfAction k, Strong k p, Promonad p) => p a b -> p c d -> p (a ** c) (b ** d)
prepar :: forall {k} {p :: CAT k} (a :: k) (b :: k) (c :: k) (d :: k).
(SelfAction k, Strong k p, Promonad p) =>
p a b -> p c d -> p (a ** c) (b ** d)
prepar p a b
f p c d
g = forall (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (c ** a) (c ** b)
forall {k} {p :: CAT k} (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k 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 :: PRO 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).
(SelfAction k, Strong k p, Ob c) =>
p a b -> p (a ** c) (b ** c)
forall {k} {p :: CAT k} (c :: k) (a :: k) (b :: k).
(SelfAction k, Strong k 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 :: PRO j k) (a :: j) (b :: k) 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 :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p c d
g

strongPar0 :: forall {k} {p :: CAT k} a. (SelfAction k, Strong k p, MonoidalProfunctor p, Ob a) => p a a
strongPar0 :: forall {k} {p :: CAT k} (a :: k).
(SelfAction k, Strong k p, MonoidalProfunctor p, Ob a) =>
p a a
strongPar0 = (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 :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
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 ((a ~> a) -> p Unit Unit -> p (Act a Unit) (Act a Unit)
forall (a :: k) (b :: k) (x :: k) (y :: k).
(a ~> b) -> p x y -> p (Act a x) (Act b y)
forall {c} {d} m (p :: c +-> d) (a :: m) (b :: m) (x :: d)
       (y :: c).
Strong m p =>
(a ~> b) -> p x y -> p (Act a x) (Act b y)
act (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
par0)

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

trace :: forall {k} (p :: k +-> k) u x y. (SelfAction k, Costrong k p, Ob x, Ob y, Ob u) => p (x ** u) (y ** u) -> p x y
trace :: forall {k} (p :: k +-> k) (u :: k) (x :: k) (y :: k).
(SelfAction k, Costrong k p, Ob x, Ob y, Ob u) =>
p (x ** u) (y ** u) -> p x y
trace p (x ** u) (y ** u)
p = forall {c} {d} m (p :: c +-> d) (a :: m) (x :: d) (y :: c).
(Costrong m p, Ob a, Ob x, Ob y) =>
p (Act a x) (Act a y) -> p x y
forall m (p :: k +-> k) (a :: m) (x :: k) (y :: k).
(Costrong m p, Ob a, Ob x, Ob y) =>
p (Act a x) (Act a y) -> p x y
coact @k @p @u @x @y ((Act u x ~> (x ** u))
-> ((y ** u) ~> Act u y)
-> p (x ** u) (y ** u)
-> p (Act u x) (Act 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 :: PRO j k) (c :: j) (a :: j) (b :: k) (d :: k).
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 :: PRO j k) (a :: j) (b :: k) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p (x ** u) (y ** u)
p

class (SelfAction k, Costrong k ((~>) :: CAT k), SymMonoidal k) => TracedMonoidal k
instance (SelfAction k, Costrong k ((~>) :: CAT k), SymMonoidal k) => TracedMonoidal k