-- | A monoid as a one-object category: the single object 'M', with the monoid's elements
-- @'Unit' ~> m@ as the morphisms. For a commutative monoid the tensor is the monoid operation
-- itself, making it symmetric monoidal, 'Closed', 'StarAutonomous' and 'CompactClosed', with a
-- cocommutative comonoid on @M@ and hence 'CopyDiscard'.
--
-- It is deliberately /not/ cartesian or cocartesian. A one-object category has a terminal object
-- only when its hom-set is a singleton, and likewise has binary products only when @'fst' . (f
-- '&&&' g) = f@ forces @'combine' f g = f@ -- both hold only for the trivial monoid. The
-- corresponding instances would be unlawful for every other @m@, so they are omitted rather than
-- given a definition that type-checks.
module Proarrow.Category.Instance.Monoid where

import Data.Type.Nat (Nat (..))
import Prelude qualified as P

import Proarrow.Category.Enriched.Thin (Enumerable (..), Finite (..), Indexed (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Closed (Closed (..))
import Proarrow.Category.Monoidal.CompactClosed (CompactClosed (..))
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard)
import Proarrow.Category.Monoidal.StarAutonomous (StarAutonomous (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), dimapDefault)
import Proarrow.Monoid (CocommutativeComonoid, CommutativeMonoid, Comonoid (..), Monoid (..), combine)

type data MONOID (m :: k) = M
data Mon a b where
  Mon :: Unit ~> m -> Mon (M :: MONOID m) M
instance (Monoid m) => Profunctor (Mon :: CAT (MONOID m)) where
  dimap :: forall (c :: MONOID m) (a :: MONOID m) (b :: MONOID m)
       (d :: MONOID m).
(c ~> a) -> (b ~> d) -> Mon a b -> Mon c d
dimap = (c ~> a) -> (b ~> d) -> Mon a b -> Mon c d
Mon c a -> Mon b d -> Mon a b -> Mon c d
forall {k} (p :: CAT k) (c :: k) (a :: k) (b :: k) (d :: k).
Promonad p =>
p c a -> p b d -> p a b -> p c d
dimapDefault
  (Ob a, Ob b) => r
r \\ :: forall (a :: MONOID m) (b :: MONOID m) r.
((Ob a, Ob b) => r) -> Mon a b -> r
\\ Mon{} = r
(Ob a, Ob b) => r
r
instance (Monoid m) => Promonad (Mon :: CAT (MONOID m)) where
  id :: forall (a :: MONOID m). Ob a => Mon a a
id = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  Mon Unit ~> m
f . :: forall (b :: MONOID m) (c :: MONOID m) (a :: MONOID m).
Mon b c -> Mon a b -> Mon a c
. Mon Unit ~> m
g = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon ((Unit ~> m) -> (Unit ~> m) -> Unit ~> m
forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g)

-- | A monoid as a one object category.
instance (Monoid m) => CategoryOf (MONOID m) where
  type (~>) = Mon
  type Ob a = a P.~ M

instance (CommutativeMonoid m) => MonoidalProfunctor (Mon :: CAT (MONOID m)) where
  one :: Mon Unit Unit
one = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  Mon Unit ~> m
f ** :: forall (x1 :: MONOID m) (x2 :: MONOID m) (y1 :: MONOID m)
       (y2 :: MONOID m).
Mon x1 x2 -> Mon y1 y2 -> Mon (x1 ** y1) (x2 ** y2)
** Mon Unit ~> m
g = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon ((Unit ~> m) -> (Unit ~> m) -> Unit ~> m
forall {k} (m :: k).
Monoid m =>
(Unit ~> m) -> (Unit ~> m) -> Unit ~> m
combine Unit ~> m
f Unit ~> m
g)
instance (CommutativeMonoid m) => Monoidal (MONOID m) where
  type Unit = M
  type M ** M = M
  withOb2 :: forall (a :: MONOID m) (b :: MONOID m) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 Ob (a ** b) => r
r = r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: MONOID m). Ob a => (Unit ** a) ~> a
leftUnitor = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  leftUnitorInv :: forall (a :: MONOID m). Ob a => a ~> (Unit ** a)
leftUnitorInv = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  rightUnitor :: forall (a :: MONOID m). Ob a => (a ** Unit) ~> a
rightUnitor = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  rightUnitorInv :: forall (a :: MONOID m). Ob a => a ~> (a ** Unit)
rightUnitorInv = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  associator :: forall (a :: MONOID m) (b :: MONOID m) (c :: MONOID m).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  associatorInv :: forall (a :: MONOID m) (b :: MONOID m) (c :: MONOID m).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
instance (CommutativeMonoid m) => SymMonoidal (MONOID m) where
  swap :: forall (a :: MONOID m) (b :: MONOID m).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty

instance (CommutativeMonoid m) => StarAutonomous (MONOID m) where
  type Dual (M :: MONOID m) = M
  withObDual :: forall (a :: MONOID m) r. Ob a => (Ob (Dual a) => r) -> r
withObDual Ob (Dual a) => r
r = r
Ob (Dual a) => r
r
  dual :: forall (a :: MONOID m) (b :: MONOID m).
(a ~> b) -> Dual b ~> Dual a
dual f :: a ~> b
f@Mon{} = a ~> b
Dual b ~> Dual a
f
  dualInv :: forall (a :: MONOID m) (b :: MONOID m).
(Ob a, Ob b) =>
(Dual a ~> Dual b) -> b ~> a
dualInv Dual a ~> Dual b
f = b ~> a
Dual a ~> Dual b
f
  linDist :: forall (a :: MONOID m) (b :: MONOID m) (c :: MONOID m).
(Ob a, Ob b, Ob c) =>
((a ** b) ~> Dual c) -> a ~> Dual (b ** c)
linDist (a ** b) ~> Dual c
_ = a ~> Dual (b ** c)
Mon M M
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MONOID m). Ob a => Mon a a
id
  linDistInv :: forall (a :: MONOID m) (b :: MONOID m) (c :: MONOID m).
(Ob a, Ob b, Ob c) =>
(a ~> Dual (b ** c)) -> (a ** b) ~> Dual c
linDistInv a ~> Dual (b ** c)
_ = (a ** b) ~> Dual c
Mon M M
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (a :: MONOID m). Ob a => Mon a a
id
instance (CommutativeMonoid m) => CompactClosed (MONOID m) where
  distribDual :: forall (a :: MONOID m) (b :: MONOID m).
(Ob a, Ob b) =>
Dual (a ** b) ~> (Dual a ** Dual b)
distribDual = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  dualUnit :: Dual Unit ~> Unit
dualUnit = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
instance (CommutativeMonoid m) => Closed (MONOID m) where
  type a ~~> b = M
  withObExp :: forall (a :: MONOID m) (b :: MONOID m) r.
(Ob a, Ob b) =>
(Ob (a ~~> b) => r) -> r
withObExp Ob (a ~~> b) => r
r = r
Ob (a ~~> b) => r
r
  curry :: forall (a :: MONOID m) (b :: MONOID m) (c :: MONOID m).
(Ob a, Ob b) =>
((a ** b) ~> c) -> a ~> (b ~~> c)
curry (Mon Unit ~> m
m) = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
m
  apply :: forall (a :: MONOID m) (b :: MONOID m).
(Ob a, Ob b) =>
((a ~~> b) ** a) ~> b
apply = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty

instance (CommutativeMonoid m) => Comonoid (M :: MONOID m) where
  counit :: M ~> Unit
counit = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
  comult :: M ~> (M ** M)
comult = (Unit ~> m) -> Mon M M
forall {k} {k} {m :: k} (m :: k). (Unit ~> m) -> Mon M M
Mon Unit ~> m
forall {k} (m :: k). Monoid m => Unit ~> m
mempty
instance (CommutativeMonoid m) => CocommutativeComonoid (M :: MONOID m)
instance (CommutativeMonoid m) => CopyDiscard (MONOID m)

-- | A monoid is a one-object category, so its kind has one inhabitant, at index zero. Said directly
-- rather than left to the 'Objects' default, so that it reduces for a not-yet-known inhabitant --
-- which is how 'withOb' learns there is only @'M'@.
instance Indexed (MONOID m) where
  type Index (a :: MONOID m) = 'Z

instance Finite (MONOID m) where type Objects (MONOID m) = '[M]

instance (Monoid m) => Enumerable (MONOID m) where
  withIndex :: forall (a :: MONOID m) r. Ob a => (KnownIndex a => r) -> r
withIndex KnownIndex a => r
r = r
KnownIndex a => r
r
  withOb :: forall (a :: MONOID m) r. KnownIndex a => (Ob a => r) -> r
withOb Ob a => r
r = r
Ob a => r
r