Span.hs

-- | The category of __spans__ in @k@: objects are those of @k@ (wrapped in 'SP'), and a morphism
-- @a '~>' b@ is a span @a <- x -> b@, composed by pullback. With the product of @k@ as tensor every
-- object is a Frobenius monoid, giving the hypergraph\/dagger structure dual to
-- "Proarrow.Category.Instance.Cospan".
module Proarrow.Category.Instance.Span where

import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
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.Hypergraph (ExpHG, Frobenius, Hypergraph, applyHG, cap, cup, curryHG)
import Proarrow.Category.Monoidal.StarAutonomous (StarAutonomous (..))
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), WrappedOb, dimapDefault, src)
import Proarrow.Limit.BinaryProduct
  ( HasBinaryProducts (..)
  , HasProducts
  , associatorProd
  , associatorProdInv
  , leftUnitorProd
  , leftUnitorProdInv
  , rightUnitorProd
  , rightUnitorProdInv
  , swapProd
  )
import Proarrow.Limit.Pullback (HasPullbacks (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (CocommutativeComonoid, CommutativeMonoid, Comonoid (..), Monoid (..))

type data SPAN k = SP k

type Span :: CAT (SPAN k)
data Span a b where
  Span :: forall c a b. c ~> a -> c ~> b -> Span (SP a) (SP b)

arr :: (CategoryOf k) => (a :: k) ~> b -> Span (SP a) (SP b)
arr f = Span (src f) f

coarr :: (CategoryOf k) => (a :: k) ~> b -> Span (SP b) (SP a)
coarr f = Span f (src f)

instance (HasPullbacks k) => Profunctor (Span :: CAT (SPAN k)) where
  dimap = dimapDefault
  r \\ Span f g = r \\ f \\ g
instance (HasPullbacks k) => Promonad (Span :: CAT (SPAN k)) where
  id = Span id id
  Span f g . Span h i = pullback i f \l r -> Span (h . l) (g . r)

-- | The category of spans in @k@: an arrow @'SP' a '~>' 'SP' b@ is a pair of arrows @x '~>' a@
-- and @x '~>' b@ out of a common object, and composition glues along a pullback.
instance (HasPullbacks k) => CategoryOf (SPAN k) where
  type (~>) = Span
  type Ob a = WrappedOb SP a

instance (HasPullbacks k, HasProducts k) => MonoidalProfunctor (Span :: CAT (SPAN k)) where
  one = id
  Span l1 l2 ** Span r1 r2 = Span (l1 *** r1) (l2 *** r2)
instance (HasPullbacks k, HasProducts k) => Monoidal (SPAN k) where
  type SP a ** SP b = SP (a && b)
  type Unit = SP TerminalObject
  withOb2 @(SP a) @(SP b) r = withObProd @k @a @b r
  leftUnitor = arr leftUnitorProd
  leftUnitorInv = arr leftUnitorProdInv
  rightUnitor = arr rightUnitorProd
  rightUnitorInv = arr rightUnitorProdInv
  associator @(SP a) @(SP b) @(SP c) = arr (associatorProd @a @b @c)
  associatorInv @(SP a) @(SP b) @(SP c) = arr (associatorProdInv @a @b @c)
instance (HasPullbacks k, HasProducts k) => SymMonoidal (SPAN k) where
  swap @(SP a) @(SP b) = arr (swapProd @a @b)

instance (HasPullbacks k, HasProducts k, Ob a) => Monoid (SP (a :: k)) where
  mempty = coarr terminate
  mappend = coarr (id &&& id)
instance (HasPullbacks k, HasProducts k, Ob a) => CommutativeMonoid (SP (a :: k))
instance (HasPullbacks k, HasProducts k, Ob a) => Comonoid (SP (a :: k)) where
  counit = arr terminate
  comult = arr (id &&& id)
instance (HasPullbacks k, HasProducts k, Ob a) => CocommutativeComonoid (SP (a :: k))
instance (HasPullbacks k, HasProducts k, Ob a) => Frobenius (SP (a :: k))
instance (HasPullbacks k, HasProducts k) => Hypergraph (SPAN k)
instance (HasPullbacks k, HasProducts k) => CopyDiscard (SPAN k)

instance (HasPullbacks k, HasProducts k) => Closed (SPAN k) where
  type a ~~> b = ExpHG a b
  withObExp @(SP a) @(SP b) r = withObProd @k @a @b r
  curry @a @b = curryHG @a @b
  apply @b @c = applyHG @b @c

instance (HasPullbacks k, HasProducts k) => StarAutonomous (SPAN k) where
  type Dual a = a
  withObDual r = r
  dual (Span f g) = Span g f
  dualInv (Span f g) = Span g f
  linDist @(SP a) @(SP b) (Span f g) = Span (fst @k @a @b . f) (snd @k @a @b . f &&& g)
  linDistInv @_ @(SP b) @(SP c) (Span f g) = Span (f &&& fst @k @b @c . g) (snd @k @b @c . g)
  doubleNeg = id
  doubleNegInv = id
instance (HasPullbacks k, HasProducts k) => CompactClosed (SPAN k) where
  distribDual @(SP a) @(SP b) = withObProd @k @a @b id
  dualUnit = id
  dualityUnit @a = cup @a
  dualityCounit @a = cap @a

instance (HasPullbacks k, HasProducts k) => DaggerProfunctor (Span :: CAT (SPAN k)) where
  dagger = dual

-- Spans over @k@ do /not/ inherit binary products, coproducts or biproducts from @k@'s
-- coproducts alone. That construction is valid only when @k@ is extensive (its coproducts
-- disjoint and stable under pullback), which 'HasPullbacks' plus 'HasBinaryCoproducts' does not
-- imply. Over BOOL, which satisfies both, @snd . (s &&& t)@ collapses to @s@ where the product
-- law demands @t@. The instances are therefore omitted; the monoidal, compact-closed and
-- hypergraph structure above needs no such condition and is unaffected.