-- | The reversed monoidal category: 'REV' wraps a kind so that @'R' a '**' 'R' b = 'R' (b ** a)@,
-- swapping the tensor's arguments while keeping the same objects and morphisms.
module Proarrow.Category.Monoidal.Rev where

import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Core (CategoryOf (..), Profunctor (..), Promonad (..), WrappedOb, type (+->))
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..), Monoid (..))

type data REV k = R k

-- | Wraps a profunctor between the 'REV'-wrapped kinds: the same values, but the monoidal
-- structure on 'REV' tensors in reverse order.
type Rev :: j +-> k -> REV j +-> REV k
data Rev p a b where
  Rev :: p a b -> Rev p (R a) (R b)

instance (Profunctor p) => Profunctor (Rev p) where
  dimap :: forall (c :: REV k) (a :: REV k) (b :: REV j) (d :: REV j).
(c ~> a) -> (b ~> d) -> Rev p a b -> Rev p c d
dimap (Rev a ~> b
l) (Rev a ~> b
r) (Rev p a b
p) = p a b -> Rev p (R a) (R b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev ((a ~> a) -> (b ~> b) -> p a b -> p a b
forall (c :: k) (a :: k) (b :: j) (d :: j).
(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 ~> b
a ~> a
l a ~> b
b ~> b
r p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: REV k) (b :: REV j) r.
((Ob a, Ob b) => r) -> Rev p a b -> r
\\ Rev p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: j) 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

instance (Promonad p) => Promonad (Rev p) where
  id :: forall (a :: REV j). Ob a => Rev p a a
id = p (UN R a) (UN R a) -> Rev p (R (UN R a)) (R (UN R a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev p (UN R a) (UN R a)
forall (a :: j). Ob a => p a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  Rev p a b
f . :: forall (b :: REV j) (c :: REV j) (a :: REV j).
Rev p b c -> Rev p a b -> Rev p a c
. Rev p a b
g = p a b -> Rev p (R a) (R b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (p a b
f p a b -> p a a -> p a b
forall (b :: j) (c :: j) (a :: j). p b c -> p a b -> p a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a a
p a b
g)

-- | The reverse of the category of @k@, i.e. with the tensor flipped.
instance (CategoryOf k) => CategoryOf (REV k) where
  type (~>) = Rev (~>)
  type Ob a = WrappedOb R a

instance (MonoidalProfunctor p) => MonoidalProfunctor (Rev p) where
  one :: Rev p Unit Unit
one = p Unit Unit -> Rev p (R Unit) (R Unit)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  Rev p a b
f ** :: forall (x1 :: REV k) (x2 :: REV j) (y1 :: REV k) (y2 :: REV j).
Rev p x1 x2 -> Rev p y1 y2 -> Rev p (x1 ** y1) (x2 ** y2)
** Rev p a b
g = p (a ** a) (b ** b) -> Rev p (R (a ** a)) (R (b ** b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (p a b
g p a b -> p a b -> p (a ** a) (b ** b)
forall (x1 :: k) (x2 :: j) (y1 :: k) (y2 :: j).
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 a b
f)

-- | The flipped tensor.
instance (Monoidal k) => Monoidal (REV k) where
  type Unit = R Unit
  type R a ** R b = R (b ** a)
  withOb2 :: forall (a :: REV k) (b :: REV k) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(R a) @(R b) Ob (a ** b) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @b @a r
Ob (UN R b ** UN R a) => r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: REV k). Ob a => (Unit ** a) ~> a
leftUnitor = ((UN R a ** Unit) ~> UN R a)
-> Rev (~>) (R (UN R a ** Unit)) (R (UN R a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (UN R a ** Unit) ~> UN R a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
  leftUnitorInv :: forall (a :: REV k). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN R a ~> (UN R a ** Unit))
-> Rev (~>) (R (UN R a)) (R (UN R a ** Unit))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev UN R a ~> (UN R a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
  rightUnitor :: forall (a :: REV k). Ob a => (a ** Unit) ~> a
rightUnitor = ((Unit ** UN R a) ~> UN R a)
-> Rev (~>) (R (Unit ** UN R a)) (R (UN R a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (Unit ** UN R a) ~> UN R a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  rightUnitorInv :: forall (a :: REV k). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN R a ~> (Unit ** UN R a))
-> Rev (~>) (R (UN R a)) (R (Unit ** UN R a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev UN R a ~> (Unit ** UN R a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  associator :: forall (a :: REV k) (b :: REV k) (c :: REV k).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(R a) @(R b) @(R c) = ((UN R c ** (UN R b ** UN R a)) ~> ((UN R c ** UN R b) ** UN R a))
-> Rev
     (~>)
     (R (UN R c ** (UN R b ** UN R a)))
     (R ((UN R c ** UN R b) ** UN R a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @c @b @a)
  associatorInv :: forall (a :: REV k) (b :: REV k) (c :: REV k).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(R a) @(R b) @(R c) = (((UN R c ** UN R b) ** UN R a) ~> (UN R c ** (UN R b ** UN R a)))
-> Rev
     (~>)
     (R ((UN R c ** UN R b) ** UN R a))
     (R (UN R c ** (UN R b ** UN R a)))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @c @b @a)

instance (SymMonoidal k) => SymMonoidal (REV k) where
  swap :: forall (a :: REV k) (b :: REV k).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(R a) @(R b) = ((UN R b ** UN R a) ~> (UN R a ** UN R b))
-> Rev (~>) (R (UN R b ** UN R a)) (R (UN R a ** UN R b))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @b @a)

instance (Monoid a) => Monoid (R a) where
  mempty :: Unit ~> R a
mempty = (Unit ~> a) -> Rev (~>) (R Unit) (R a)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev Unit ~> a
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  mappend :: (R a ** R a) ~> R a
mappend = ((a ** a) ~> a) -> Rev (~>) (R (a ** a)) (R a)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev (a ** a) ~> a
forall {k} (m :: k). Monoid m => (m ** m) ~> m
mappend

instance (Comonoid a) => Comonoid (R a) where
  counit :: R a ~> Unit
counit = (a ~> Unit) -> Rev (~>) (R a) (R Unit)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev a ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit
  comult :: R a ~> (R a ** R a)
comult = (a ~> (a ** a)) -> Rev (~>) (R a) (R (a ** a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev a ~> (a ** a)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult
instance (CocommutativeComonoid a) => CocommutativeComonoid (R a)

instance (CopyDiscard k) => CopyDiscard (REV k) where
  copy :: forall (a :: REV k). Ob a => a ~> (a ** a)
copy = (UN R a ~> (UN R a ** UN R a))
-> Rev (~>) (R (UN R a)) (R (UN R a ** UN R a))
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev UN R a ~> (UN R a ** UN R a)
forall (a :: k). Ob a => a ~> (a ** a)
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy
  discard :: forall (a :: REV k). Ob a => a ~> Unit
discard = (UN R a ~> Unit) -> Rev (~>) (R (UN R a)) (R Unit)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
p a b -> Rev p (R a) (R b)
Rev UN R a ~> Unit
forall (a :: k). Ob a => a ~> Unit
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard