Sub.hs

-- | __Full subcategories__: the kind @'SUBCAT' ob@ restricts a category to the objects satisfying
-- the predicate @ob@, with 'Sub' wrapping the underlying arrows unchanged. This is how object
-- constraints beyond a kind's own 'Ob' are imposed (e.g. the category of representable profunctors
-- in "Proarrow.Category.Instance.Rep").
module Proarrow.Category.Instance.Sub where

import Data.Kind (Constraint)

import Proarrow.Category.Instance.Prof (Prof (..))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Core (CAT, CategoryOf (..), Kind, OB, Profunctor (..), Promonad (..), UN, WrappedOb, type (+->))
import Proarrow.Functor (FunctorForRep (..))
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..))
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Profunctor.Representable (Representable (..))
import Prelude (type (~))

import Proarrow.Category.Instance.Bool (BOOL (..), Booleans (..))

type SUBCAT :: forall {k}. OB k -> Kind
type data SUBCAT (ob :: OB k) = SUB k

-- | Wraps an arrow whose endpoints satisfy the predicate @ob@: the arrows of the full
-- subcategory 'SUBCAT'.
type Sub :: CAT k -> CAT (SUBCAT (ob :: OB k))
data Sub p a b where
  Sub :: (ob a, ob b) => {unSub :: p a b} -> Sub p (SUB a :: SUBCAT ob) (SUB b)

instance (Profunctor p) => Profunctor (Sub p) where
  dimap (Sub l) (Sub r) (Sub p) = Sub (dimap l r p)
  r \\ Sub p = r \\ p

instance (Promonad p) => Promonad (Sub p) where
  id = Sub id
  Sub f . Sub g = Sub (f . g)

-- | The subcategory with objects with instances of the given constraint `ob`.
instance (CategoryOf k) => CategoryOf (SUBCAT (ob :: OB k)) where
  type (~>) = Sub (~>)
  type Ob (a :: SUBCAT ob) = (WrappedOb SUB a, ob (UN SUB a))

type On :: (k -> Constraint) -> forall (ob :: OB k) -> SUBCAT ob -> Constraint
class (c (UN SUB a)) => (c `On` ob) a
instance (c (UN SUB a)) => (c `On` ob) a

class (ob (a ** b)) => IsObMult (ob :: OB k) a b
instance (ob (a ** b)) => IsObMult (ob :: OB k) a b

-- | The same for the /product/: that the subcategory contains the products of its objects, as a
-- class with a single instance so that it can be the head of a quantified constraint.
class (ob (a && b)) => IsObProd (ob :: OB k) a b

instance (ob (a && b)) => IsObProd (ob :: OB k) a b

-- | A full subcategory has the ambient finite products as soon as it contains them, as the
-- quantified constraint says. The projections and pairing are the ambient ones under 'Sub'.
--
-- There is no exponential at an arbitrary kind: neither @'withObExp'@ nor @curry@ discharges
-- through @'Proarrow.Limit.BinaryProduct.PROD' k@\'s round trip
-- @'Proarrow.Core.UN' PR (PR a '~~>' PR b)@.
-- For subcategories of profunctors see
-- @'Proarrow.Category.Monoidal.Closed.Closed' ('Proarrow.Limit.BinaryProduct.PROD' ('SUBCAT' ob))@
-- in "Proarrow.Profunctor.Instance.Exponential".
instance (HasTerminalObject k, ob (TerminalObject :: k)) => HasTerminalObject (SUBCAT (ob :: OB k)) where
  type TerminalObject @(SUBCAT (ob :: OB k)) = SUB (TerminalObject :: k)
  terminate = Sub terminate

instance
  (HasBinaryProducts k, forall a b. (ob a, ob b) => IsObProd ob a b)
  => HasBinaryProducts (SUBCAT (ob :: OB k))
  where
  type (&&) @(SUBCAT (ob :: OB k)) a b = SUB (UN SUB a && UN SUB b)
  withObProd @(SUB a) @(SUB b) r = withObProd @k @a @b r
  fst @(SUB a) @(SUB b) = Sub (fst @k @a @b)
  snd @(SUB a) @(SUB b) = Sub (snd @k @a @b)
  Sub l &&& Sub r = Sub (l &&& r)

instance (MonoidalProfunctor p, SubMonoidal ob) => MonoidalProfunctor (Sub p :: CAT (SUBCAT (ob :: OB k))) where
  one = Sub one
  Sub f ** Sub g = Sub (f ** g)

class (Monoidal k, ob Unit, forall a b. (ob a, ob b) => IsObMult ob a b) => SubMonoidal (ob :: OB k)
instance (Monoidal k, ob Unit, forall a b. (ob a, ob b) => IsObMult ob a b) => SubMonoidal (ob :: OB k)

instance (SubMonoidal ob) => Monoidal (SUBCAT (ob :: OB k)) where
  type Unit = SUB Unit
  type a ** b = SUB (UN SUB a ** UN SUB b)
  withOb2 @(SUB a) @(SUB b) r = withOb2 @k @a @b r
  leftUnitor = Sub leftUnitor
  leftUnitorInv = Sub leftUnitorInv
  rightUnitor = Sub rightUnitor
  rightUnitorInv = Sub rightUnitorInv
  associator @(SUB a) @(SUB b) @(SUB c) = Sub (associator @_ @a @b @c)
  associatorInv @(SUB a) @(SUB b) @(SUB c) = Sub (associatorInv @_ @a @b @c)

instance (SymMonoidal k, SubMonoidal ob) => SymMonoidal (SUBCAT (ob :: OB k)) where
  swap @(SUB a) @(SUB b) = Sub (swap @k @a @b)

data family Forget :: forall (ob :: OB k) -> SUBCAT ob +-> k
instance (CategoryOf k) => FunctorForRep (Forget (ob :: OB k)) where
  type Forget ob @ a = UN SUB a
  fmap (Sub f) = f

instance (Representable p, forall a. (ob a) => ob (p % a)) => Representable (Sub p :: CAT (SUBCAT (ob :: OB k))) where
  type Sub p % a = SUB (p % UN SUB a)
  index (Sub p) = Sub (index p)
  tabulate (Sub f) = Sub (tabulate f)
  repMap (Sub f) = Sub (repMap @p f)

type FUN j k = SUBCAT (Representable :: OB (j +-> k))

(!) :: forall {j} {k} f g a b. f ~> (g :: FUN j k) -> a ~> b -> UN SUB f % a ~> UN SUB g % b
Sub (Prof n) ! ab = index @(UN SUB g) @_ @b (n (tabulate (repMap @(UN SUB f) ab))) \\ ab

-- | The arrow category of @k@ as functor category from @2@ to @k@.
type ARROW k = FUN BOOL k

commSquare
  :: forall {k} f g a b c d
   . (a ~ f % FLS, b ~ f % TRU, c ~ g % FLS, d ~ g % TRU) => SUB f ~> (SUB g :: ARROW k) -> (a ~> b, b ~> d, a ~> c, c ~> d)
commSquare n = (repMap @f F2T, n ! Tru, n ! Fls, repMap @g F2T) \\ n