Rev.hs

-- | 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 (Rev l) (Rev r) (Rev p) = Rev (dimap l r p)
  r \\ Rev p = r \\ p

instance (Promonad p) => Promonad (Rev p) where
  id = Rev id
  Rev f . Rev g = Rev (f . 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 one
  Rev f ** Rev g = Rev (g ** f)

-- | The flipped tensor.
instance (Monoidal k) => Monoidal (REV k) where
  type Unit = R Unit
  type R a ** R b = R (b ** a)
  withOb2 @(R a) @(R b) r = withOb2 @k @b @a r
  leftUnitor = Rev rightUnitor
  leftUnitorInv = Rev rightUnitorInv
  rightUnitor = Rev leftUnitor
  rightUnitorInv = Rev leftUnitorInv
  associator @(R a) @(R b) @(R c) = Rev (associatorInv @k @c @b @a)
  associatorInv @(R a) @(R b) @(R c) = Rev (associator @k @c @b @a)

instance (SymMonoidal k) => SymMonoidal (REV k) where
  swap @(R a) @(R b) = Rev (swap @k @b @a)

instance (Monoid a) => Monoid (R a) where
  mempty = Rev mempty
  mappend = Rev mappend

instance (Comonoid a) => Comonoid (R a) where
  counit = Rev counit
  comult = Rev comult
instance (CocommutativeComonoid a) => CocommutativeComonoid (R a)

instance (CopyDiscard k) => CopyDiscard (REV k) where
  copy = Rev copy
  discard = Rev discard