{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Category.Monoidal.Action where

import Data.Kind (Constraint)

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

-- | Weighted strength for a monoidal action. Usually this is used unweighted, where @w@ is an arrow.
type Strong :: forall {m} {m'} {j} {k}. m +-> m' -> j +-> k -> Constraint
class (MonoidalAction m c, MonoidalAction m' d, Profunctor p) => Strong (w :: m +-> m') (p :: c +-> d) where
  act :: w a b -> p x y -> p (Act a x) (Act b y)

class (Monoidal m, CategoryOf k, Strong ((~>) :: CAT 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
  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)

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 {m} {m'} {c} {d} (w :: m +-> m') (p :: c +-> d) (a :: m')
       (b :: m) (x :: d) (y :: c).
Strong w p =>
w 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 {m} {m'} {c} {d} (w :: m +-> m') (p :: c +-> d) (a :: m')
       (b :: m) (x :: d) (y :: c).
Strong w p =>
w 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