Kleisli.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | The __Kleisli category__ of a 'Promonad' @p@: objects are those of the base category (wrapped
-- in 'KL') and a morphism @'KL' a '~>' 'KL' b@ is an element @p a b@, composed with @p@'s own
-- composition. Terminal\/initial objects, (co)products, monoidal and
-- 'Proarrow.Category.Monoidal.CopyDiscard.CopyDiscard' structure lift from the base category when
-- @p@ cooperates (e.g. is a 'Proarrow.Category.Monoidal.MonoidalProfunctor').
module Proarrow.Category.Instance.Kleisli
  ( KLEISLI (..)
  , Kleisli (..)
  , arr
  , KleisliFree (..)
  , KleisliForget (..)
  , LIFTEDF
  , pattern LiftF
  ) where

import Proarrow.Adjunction (Proadjunction)
import Proarrow.Adjunction qualified as Adj
import Proarrow.Category.Enriched.Dagger (DaggerProfunctor (..))
import Proarrow.Category.Enriched.Thin (DecidableProfunctor (..), mapDecision)
import Proarrow.Category.Enriched.Thin qualified as T
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (..), SymMonoidal (..))
import Proarrow.Category.Monoidal.Cartesian (Cartesian)
import Proarrow.Category.Monoidal.CopyDiscard (CopyDiscard (..))
import Proarrow.Category.Monoidal.Distributive (Distributive (..), DistributiveProfunctor)
import Proarrow.Colimit.BinaryCoproduct (Coprod, HasBinaryCoproducts (..), codiag, (++))
import Proarrow.Colimit.Initial (HasInitialObject (..))
import Proarrow.Core
  ( CAT
  , CategoryOf (..)
  , Profunctor (..)
  , Promonad (..)
  , UN
  , WrappedOb
  , dimapDefault
  , lmap
  , rmap
  , type (+->)
  )
import Proarrow.Limit.BinaryProduct (HasBinaryProducts (..), diag)
import Proarrow.Limit.Terminal (HasTerminalObject (..))
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..))
import Proarrow.Object (tgt, pattern Obj, type Obj)
import Proarrow.Profunctor.Instance.Composition ((:.:) (..))
import Proarrow.Profunctor.Representable (RepCostar (..), Representable (..), repUniv)
import Proarrow.Promonad (Comonad, Monad)

type data KLEISLI (p :: CAT k) = KL k

-- | The arrows of the promonad @p@, wrapped as a category on the 'KLEISLI'-wrapped kind.
type Kleisli :: CAT (KLEISLI p)
data Kleisli (a :: KLEISLI p) b where
  Kleisli :: {unKleisli :: p a b} -> Kleisli (KL a :: KLEISLI p) (KL b)

instance (Promonad p) => Profunctor (Kleisli :: CAT (KLEISLI p)) where
  dimap = dimapDefault
  r \\ Kleisli p = r \\ p

arr :: (Promonad p) => a ~> b -> Kleisli (KL a :: KLEISLI p) (KL b)
arr f = Kleisli (rmap f id) \\ f

-- | Every promonad makes a category.
instance (Promonad p) => CategoryOf (KLEISLI p) where
  type (~>) = Kleisli
  type Ob a = WrappedOb KL a

instance (Promonad p) => Promonad (Kleisli :: CAT (KLEISLI p)) where
  id = Kleisli id
  Kleisli f . Kleisli g = Kleisli (f . g)

-- | The terminal object lifts to the co-Kleisli category of a 'Comonad': there @p a b@ is
-- @p '%%' a '~>' b@, so @p a (-)@ is representable and preserves limits. A bare 'Promonad' is not
-- enough. At the constant promonad @'Proarrow.Profunctor.Instance.HaskValue.HaskValue' c@ every
-- element of @c@ is an arrow into the terminal object, so uniqueness fails.
instance (HasTerminalObject k, Comonad p) => HasTerminalObject (KLEISLI (p :: k +-> k)) where
  type TerminalObject @(KLEISLI (p :: k +-> k)) = KL (TerminalObject :: k)
  terminate = arr terminate

-- | Dually, the initial object lifts to the Kleisli category of a 'Monad': there @p a b@ is
-- @a '~>' p '%' b@, so the presheaf @p (-) z@ is representable and takes colimits in @k@ to limits.
instance (HasInitialObject k, Monad p) => HasInitialObject (KLEISLI (p :: k +-> k)) where
  type InitialObject @(KLEISLI (p :: k +-> k)) = KL (InitialObject :: k)
  initiate = arr initiate

-- | Products lift for the same reason as the terminal object: for a 'Comonad' @p a (-)@ is
-- representable, and @'lmap' 'diag' (f '**' g)@ is then the canonical mediating map.
instance (Cartesian k, Comonad p, MonoidalProfunctor p) => HasBinaryProducts (KLEISLI (p :: k +-> k)) where
  type a && b = KL (UN KL a && UN KL b)
  withObProd @(KL a) @(KL b) r = withObProd @k @a @b r
  fst @(KL a) @(KL b) = arr (fst @_ @a @b)
  snd @(KL a) @(KL b) = arr (snd @_ @a @b)
  Kleisli f &&& Kleisli g = Kleisli (lmap diag (f ** g)) \\ f

-- | Coproducts lift for the same reason as the initial object: for a 'Monad' @p (-) z@ is a
-- representable presheaf.
instance
  (HasBinaryCoproducts k, Monad p, MonoidalProfunctor (Coprod p))
  => HasBinaryCoproducts (KLEISLI (p :: k +-> k))
  where
  type a || b = KL (UN KL a || UN KL b)
  withObCoprod @(KL a) @(KL b) r = withObCoprod @k @a @b r
  lft @(KL a) @(KL b) = arr (lft @_ @a @b)
  rgt @(KL a) @(KL b) = arr (rgt @_ @a @b)
  Kleisli f ||| Kleisli g = Kleisli (rmap codiag (f ++ g)) \\ f

instance (Promonad p, MonoidalProfunctor p) => MonoidalProfunctor (Kleisli :: CAT (KLEISLI (p :: k +-> k))) where
  one = Kleisli one
  Kleisli f ** Kleisli g = Kleisli (f ** g)

-- | If the promonad is a monoidal profunctor, then its Kleisli category is a monoidal category.
instance (Promonad p, MonoidalProfunctor p) => Monoidal (KLEISLI (p :: k +-> k)) where
  type Unit @(KLEISLI (p :: k +-> k)) = KL (Unit :: k)
  type a ** b = KL (UN KL a ** UN KL b)
  withOb2 @(KL a) @(KL b) r = withOb2 @k @a @b r
  leftUnitor = arr leftUnitor
  leftUnitorInv = arr leftUnitorInv
  rightUnitor = arr rightUnitor
  rightUnitorInv = arr rightUnitorInv
  associator @(KL a) @(KL b) @(KL c) = arr (associator @k @a @b @c)
  associatorInv @(KL a) @(KL b) @(KL c) = arr (associatorInv @k @a @b @c)

instance (Promonad p, MonoidalProfunctor p, SymMonoidal k) => SymMonoidal (KLEISLI (p :: k +-> k)) where
  swap @(KL a) @(KL b) = arr (swap @k @a @b)
instance (Promonad p, MonoidalProfunctor p, CopyDiscard k, Ob (a :: KLEISLI p)) => Comonoid (a :: KLEISLI (p :: k +-> k)) where
  counit = discard
  comult = copy
instance
  (Promonad p, MonoidalProfunctor p, CopyDiscard k, Ob (a :: KLEISLI p))
  => CocommutativeComonoid (a :: KLEISLI (p :: k +-> k))
instance (Promonad p, MonoidalProfunctor p, CopyDiscard k) => CopyDiscard (KLEISLI (p :: k +-> k)) where
  copy = arr copy
  discard = arr discard

instance (Distributive k, Monad p, DistributiveProfunctor p) => Distributive (KLEISLI (p :: k +-> k)) where
  distL @(KL a) @(KL b) @(KL c) = arr (distL @k @a @b @c)
  distR @(KL a) @(KL b) @(KL c) = arr (distR @k @a @b @c)
  absorbL @(KL a) = arr (absorbL @k @a)
  absorbR @(KL a) = arr (absorbR @k @a)

instance (DaggerProfunctor p, Promonad p) => DaggerProfunctor (Kleisli :: CAT (KLEISLI p)) where
  dagger (Kleisli p) = Kleisli (dagger p)

instance (T.ThinProfunctor p, Promonad p) => T.ThinProfunctor (Kleisli :: CAT (KLEISLI p)) where
  type HasArrow (Kleisli :: CAT (KLEISLI p)) (KL a) (KL b) = T.HasArrow p a b
  arr = Kleisli T.arr
  withArr (Kleisli p) r = T.withArr p r

instance (DecidableProfunctor p, Promonad p) => DecidableProfunctor (Kleisli :: CAT (KLEISLI p)) where
  type Holds (Kleisli :: CAT (KLEISLI p)) (KL a) (KL b) = Holds p a b
  decide @(KL a) @(KL b) = mapDecision Kleisli (decide @p @a @b)
  toHolds (Kleisli p) r = toHolds p r

-- | The Kleisli category has the objects of @k@, numbered the same way, so a Kleisli category of a
-- decidable promonad on an enumerable category is itself enumerable, and so can be searched, or
-- closed ("Proarrow.Category.Enriched.Thin.Composition").
instance (T.Indexed k) => T.Indexed (KLEISLI (p :: CAT k)) where
  type Index (a :: KLEISLI p) = T.Index (UN KL a)
  type At (KLEISLI (p :: CAT k)) i = T.FmapWrap KL (T.At k i)

instance (T.Finite k) => T.Finite (KLEISLI (p :: CAT k)) where
  type Objects (KLEISLI (p :: CAT k)) = T.MapWrap KL (T.Objects k)
  finite = T.wrapFinite @KL
  withAtLookup = T.withWrapAtLookup @KL

instance (T.Enumerable k, Promonad p) => T.Enumerable (KLEISLI (p :: CAT k)) where
  withIndex @(KL a) r = T.withIndex @k @a r
  atOb i = case T.atOb @k i of
    T.AtJust -> T.AtJust
    T.AtNothing -> T.AtNothing

-- | The free half of the Kleisli adjunction ('Proadjunction' below), embedding @k@ into the
-- Kleisli category of @p@.
type KleisliFree :: forall (p :: k +-> k) -> k +-> KLEISLI p
data KleisliFree p a b where
  KleisliFree :: p a b -> KleisliFree p (KL a) b

instance (Promonad p) => Profunctor (KleisliFree p) where
  dimap (Kleisli l) r (KleisliFree p) = KleisliFree (rmap r p . l)
  r \\ KleisliFree p = r \\ p

-- | The forgetful half of the Kleisli adjunction, mapping Kleisli objects back to @k@.
type KleisliForget :: forall (p :: k +-> k) -> KLEISLI p +-> k
data KleisliForget p a b where
  KleisliForget :: p a b -> KleisliForget p a (KL b)

instance (Promonad p) => Profunctor (KleisliForget p) where
  dimap l (Kleisli r) (KleisliForget p) = KleisliForget (r . lmap l p)
  r \\ KleisliForget p = r \\ p

instance (Promonad p) => Proadjunction (KleisliFree p) (KleisliForget p) where
  unit = KleisliForget id :.: KleisliFree id
  counit (KleisliFree p :.: KleisliForget q) = Kleisli (q . p)

-- | Categories lifted by a representable profunctor: @f % a ~> f % b@ are kleisli categories on promonads induced by @f@.
type LIFTEDF (f :: j +-> k) = KLEISLI (RepCostar f :.: f)

unlift :: (Representable f) => Kleisli (KL a :: LIFTEDF f) (KL b) -> (f % a ~> f % b, Obj a, Obj b)
unlift (Kleisli (RepCostar f :.: g)) = (index g . f, Obj, tgt g)

pattern LiftF
  :: (Representable (f :: j +-> k)) => (Ob (a :: j), Ob b) => (f % a ~> f % b) -> Kleisli (KL a :: LIFTEDF f) (KL b)
pattern LiftF f <- (unlift -> (f, Obj, Obj))
  where
    LiftF f = Kleisli (RepCostar f :.: repUniv)

{-# COMPLETE LiftF #-}