{-# 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 :: {forall {k} (p :: CAT k) (b :: k) (b :: k).
Kleisli (KL b) (KL b) -> p b b
unKleisli :: p a b} -> Kleisli (KL a :: KLEISLI p) (KL b)

instance (Promonad p) => Profunctor (Kleisli :: CAT (KLEISLI p)) where
  dimap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: KLEISLI p)
       (d :: KLEISLI p).
(c ~> a) -> (b ~> d) -> Kleisli a b -> Kleisli c d
dimap = (c ~> a) -> (b ~> d) -> Kleisli a b -> Kleisli c d
Kleisli c a -> Kleisli b d -> Kleisli a b -> Kleisli 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 :: KLEISLI p) (b :: KLEISLI p) r.
((Ob a, Ob b) => r) -> Kleisli a b -> r
\\ Kleisli p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

arr :: (Promonad p) => a ~> b -> Kleisli (KL a :: KLEISLI p) (KL b)
arr :: forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr a ~> b
f = p a b -> Kleisli (KL a) (KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli ((a ~> b) -> p a a -> p a b
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap a ~> b
f p a a
forall (a :: k). Ob a => p a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id) ((Ob a, Ob b) => Kleisli (KL a) (KL b))
-> (a ~> b) -> Kleisli (KL a) (KL b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> (a ~> b) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ a ~> b
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 :: forall (a :: KLEISLI p). Ob a => Kleisli a a
id = p (UN KL a) (UN KL a) -> Kleisli (KL (UN KL a)) (KL (UN KL a))
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli p (UN KL a) (UN KL a)
forall (a :: k). Ob a => p a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  Kleisli p a b
f . :: forall (b :: KLEISLI p) (c :: KLEISLI p) (a :: KLEISLI p).
Kleisli b c -> Kleisli a b -> Kleisli a c
. Kleisli p a b
g = p a b -> Kleisli (KL a) (KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli (p a b
f p a b -> p a a -> p a b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a a
p a b
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 :: forall (a :: KLEISLI p). Ob a => a ~> TerminalObject
terminate = (UN KL a ~> TerminalObject)
-> Kleisli (KL (UN KL a)) (KL TerminalObject)
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr UN KL a ~> TerminalObject
forall (a :: k). Ob a => a ~> TerminalObject
forall k (a :: k).
(HasTerminalObject k, Ob a) =>
a ~> TerminalObject
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 :: forall (a :: KLEISLI p). Ob a => InitialObject ~> a
initiate = (InitialObject ~> UN KL a)
-> Kleisli (KL InitialObject) (KL (UN KL a))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr InitialObject ~> UN KL a
forall (a :: k). Ob a => InitialObject ~> a
forall k (a :: k). (HasInitialObject k, Ob a) => InitialObject ~> a
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 :: forall (a :: KLEISLI p) (b :: KLEISLI p) r.
(Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @(KL a) @(KL b) Ob (a && b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryProducts k, Ob a, Ob b) =>
(Ob (a && b) => r) -> r
withObProd @k @a @b r
Ob (UN KL a && UN KL b) => r
Ob (a && b) => r
r
  fst :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b) =>
(a && b) ~> a
fst @(KL a) @(KL b) = ((UN KL a && UN KL b) ~> UN KL a)
-> Kleisli (KL (UN KL a && UN KL b)) (KL (UN KL a))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> a
fst @_ @a @b)
  snd :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b) =>
(a && b) ~> b
snd @(KL a) @(KL b) = ((UN KL a && UN KL b) ~> UN KL b)
-> Kleisli (KL (UN KL a && UN KL b)) (KL (UN KL b))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (forall k (a :: k) (b :: k).
(HasBinaryProducts k, Ob a, Ob b) =>
(a && b) ~> b
snd @_ @a @b)
  Kleisli p a b
f &&& :: forall (a :: KLEISLI p) (x :: KLEISLI p) (y :: KLEISLI p).
(a ~> x) -> (a ~> y) -> a ~> (x && y)
&&& Kleisli p a b
g = p a (b && b) -> Kleisli (KL a) (KL (b && b))
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli ((a ~> (a && a)) -> p (a && a) (b && b) -> p a (b && b)
forall (c :: k) (a :: k) (b :: k). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap a ~> (a && a)
forall {k} (a :: k). (HasBinaryProducts k, Ob a) => a ~> (a && a)
diag (p a b
f p a b -> p a b -> p (a ** a) (b ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** p a b
p a b
g)) ((Ob a, Ob b) => Kleisli (KL a) (KL (b && b)))
-> p a b -> Kleisli (KL a) (KL (b && b))
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
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 :: forall (a :: KLEISLI p) (b :: KLEISLI p) r.
(Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @(KL a) @(KL b) Ob (a || b) => r
r = forall k (a :: k) (b :: k) r.
(HasBinaryCoproducts k, Ob a, Ob b) =>
(Ob (a || b) => r) -> r
withObCoprod @k @a @b r
Ob (UN KL a || UN KL b) => r
Ob (a || b) => r
r
  lft :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b) =>
a ~> (a || b)
lft @(KL a) @(KL b) = (UN KL a ~> (UN KL a || UN KL b))
-> Kleisli (KL (UN KL a)) (KL (UN KL a || UN KL b))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
a ~> (a || b)
lft @_ @a @b)
  rgt :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b) =>
b ~> (a || b)
rgt @(KL a) @(KL b) = (UN KL b ~> (UN KL a || UN KL b))
-> Kleisli (KL (UN KL b)) (KL (UN KL a || UN KL b))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (forall k (a :: k) (b :: k).
(HasBinaryCoproducts k, Ob a, Ob b) =>
b ~> (a || b)
rgt @_ @a @b)
  Kleisli p a b
f ||| :: forall (x :: KLEISLI p) (a :: KLEISLI p) (y :: KLEISLI p).
(x ~> a) -> (y ~> a) -> (x || y) ~> a
||| Kleisli p a b
g = p (a || a) b -> Kleisli (KL (a || a)) (KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli (((b || b) ~> b) -> p (a || a) (b || b) -> p (a || a) b
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap (b || b) ~> b
forall {k} (a :: k). (HasBinaryCoproducts k, Ob a) => (a || a) ~> a
codiag (p a b
f p a b -> p a b -> p (a || a) (b || b)
forall {k1} {k2} (p :: k1 +-> k2) (a :: k2) (b :: k1) (c :: k2)
       (d :: k1).
MonoidalProfunctor (Coprod p) =>
p a b -> p c d -> p (a || c) (b || d)
++ p a b
p a b
g)) ((Ob a, Ob b) => Kleisli (KL (a || a)) (KL b))
-> p a b -> Kleisli (KL (a || a)) (KL b)
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
f

instance (Promonad p, MonoidalProfunctor p) => MonoidalProfunctor (Kleisli :: CAT (KLEISLI (p :: k +-> k))) where
  one :: Kleisli Unit Unit
one = p Unit Unit -> Kleisli (KL Unit) (KL Unit)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli p Unit Unit
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one
  Kleisli p a b
f ** :: forall (x1 :: KLEISLI p) (x2 :: KLEISLI p) (y1 :: KLEISLI p)
       (y2 :: KLEISLI p).
Kleisli x1 x2 -> Kleisli y1 y2 -> Kleisli (x1 ** y1) (x2 ** y2)
** Kleisli p a b
g = p (a ** a) (b ** b) -> Kleisli (KL (a ** a)) (KL (b ** b))
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli (p a b
f p a b -> p a b -> p (a ** a) (b ** b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
** p a b
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 :: forall (a :: KLEISLI p) (b :: KLEISLI p) r.
(Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @(KL a) @(KL b) Ob (a ** b) => r
r = forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @k @a @b r
Ob (UN KL a ** UN KL b) => r
Ob (a ** b) => r
r
  leftUnitor :: forall (a :: KLEISLI p). Ob a => (Unit ** a) ~> a
leftUnitor = ((Unit ** UN KL a) ~> UN KL a)
-> Kleisli (KL (Unit ** UN KL a)) (KL (UN KL a))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (Unit ** UN KL a) ~> UN KL a
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor
  leftUnitorInv :: forall (a :: KLEISLI p). Ob a => a ~> (Unit ** a)
leftUnitorInv = (UN KL a ~> (Unit ** UN KL a))
-> Kleisli (KL (UN KL a)) (KL (Unit ** UN KL a))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr UN KL a ~> (Unit ** UN KL a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv
  rightUnitor :: forall (a :: KLEISLI p). Ob a => (a ** Unit) ~> a
rightUnitor = ((UN KL a ** Unit) ~> UN KL a)
-> Kleisli (KL (UN KL a ** Unit)) (KL (UN KL a))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (UN KL a ** Unit) ~> UN KL a
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor
  rightUnitorInv :: forall (a :: KLEISLI p). Ob a => a ~> (a ** Unit)
rightUnitorInv = (UN KL a ~> (UN KL a ** Unit))
-> Kleisli (KL (UN KL a)) (KL (UN KL a ** Unit))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr UN KL a ~> (UN KL a ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv
  associator :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p).
(Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @(KL a) @(KL b) @(KL c) = (((UN KL a ** UN KL b) ** UN KL c)
 ~> (UN KL a ** (UN KL b ** UN KL c)))
-> Kleisli
     (KL ((UN KL a ** UN KL b) ** UN KL c))
     (KL (UN KL a ** (UN KL b ** UN KL c)))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
((a ** b) ** c) ~> (a ** (b ** c))
associator @k @a @b @c)
  associatorInv :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p).
(Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @(KL a) @(KL b) @(KL c) = ((UN KL a ** (UN KL b ** UN KL c))
 ~> ((UN KL a ** UN KL b) ** UN KL c))
-> Kleisli
     (KL (UN KL a ** (UN KL b ** UN KL c)))
     (KL ((UN KL a ** UN KL b) ** UN KL c))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (forall k (a :: k) (b :: k) (c :: k).
(Monoidal k, Ob a, Ob b, Ob c) =>
(a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv @k @a @b @c)

instance (Promonad p, MonoidalProfunctor p, SymMonoidal k) => SymMonoidal (KLEISLI (p :: k +-> k)) where
  swap :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @(KL a) @(KL b) = ((UN KL a ** UN KL b) ~> (UN KL b ** UN KL a))
-> Kleisli (KL (UN KL a ** UN KL b)) (KL (UN KL b ** UN KL a))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @a @b)
instance (Promonad p, MonoidalProfunctor p, CopyDiscard k, Ob (a :: KLEISLI p)) => Comonoid (a :: KLEISLI (p :: k +-> k)) where
  counit :: a ~> Unit
counit = a ~> Unit
KL (UN KL a) ~> Unit
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
forall (a :: KLEISLI p). Ob a => a ~> Unit
discard
  comult :: a ~> (a ** a)
comult = a ~> (a ** a)
KL (UN KL a) ~> (KL (UN KL a) ** KL (UN KL a))
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
forall (a :: KLEISLI p). Ob a => a ~> (a ** a)
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 :: forall (a :: KLEISLI p). Ob a => a ~> (a ** a)
copy = (UN KL a ~> (UN KL a ** UN KL a))
-> Kleisli (KL (UN KL a)) (KL (UN KL a ** UN KL a))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr UN KL a ~> (UN KL a ** UN KL a)
forall (a :: k). Ob a => a ~> (a ** a)
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> (a ** a)
copy
  discard :: forall (a :: KLEISLI p). Ob a => a ~> Unit
discard = (UN KL a ~> Unit) -> Kleisli (KL (UN KL a)) (KL Unit)
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr UN KL a ~> Unit
forall (a :: k). Ob a => a ~> Unit
forall k (a :: k). (CopyDiscard k, Ob a) => a ~> Unit
discard

instance (Distributive k, Monad p, DistributiveProfunctor p) => Distributive (KLEISLI (p :: k +-> k)) where
  distL :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p).
(Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @(KL a) @(KL b) @(KL c) = ((UN KL a ** (UN KL b || UN KL c))
 ~> ((UN KL a ** UN KL b) || (UN KL a ** UN KL c)))
-> Kleisli
     (KL (UN KL a ** (UN KL b || UN KL c)))
     (KL ((UN KL a ** UN KL b) || (UN KL a ** UN KL c)))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
(a ** (b || c)) ~> ((a ** b) || (a ** c))
distL @k @a @b @c)
  distR :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p).
(Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @(KL a) @(KL b) @(KL c) = (((UN KL a || UN KL b) ** UN KL c)
 ~> ((UN KL a ** UN KL c) || (UN KL b ** UN KL c)))
-> Kleisli
     (KL ((UN KL a || UN KL b) ** UN KL c))
     (KL ((UN KL a ** UN KL c) || (UN KL b ** UN KL c)))
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (forall k (a :: k) (b :: k) (c :: k).
(Distributive k, Ob a, Ob b, Ob c) =>
((a || b) ** c) ~> ((a ** c) || (b ** c))
distR @k @a @b @c)
  absorbL :: forall (a :: KLEISLI p).
Ob a =>
(a ** InitialObject) ~> InitialObject
absorbL @(KL a) = ((UN KL a ** InitialObject) ~> InitialObject)
-> Kleisli (KL (UN KL a ** InitialObject)) (KL InitialObject)
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (forall k (a :: k).
(Distributive k, Ob a) =>
(a ** InitialObject) ~> InitialObject
absorbL @k @a)
  absorbR :: forall (a :: KLEISLI p).
Ob a =>
(InitialObject ** a) ~> InitialObject
absorbR @(KL a) = ((InitialObject ** UN KL a) ~> InitialObject)
-> Kleisli (KL (InitialObject ** UN KL a)) (KL InitialObject)
forall {k} (p :: CAT k) (a :: k) (b :: k).
Promonad p =>
(a ~> b) -> Kleisli (KL a) (KL b)
arr (forall k (a :: k).
(Distributive k, Ob a) =>
(InitialObject ** a) ~> InitialObject
absorbR @k @a)

instance (DaggerProfunctor p, Promonad p) => DaggerProfunctor (Kleisli :: CAT (KLEISLI p)) where
  dagger :: forall (a :: KLEISLI p) (b :: KLEISLI p).
Kleisli a b -> Kleisli b a
dagger (Kleisli p a b
p) = p b a -> Kleisli (KL b) (KL a)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli (p a b -> p b a
forall (a :: k) (b :: k). p a b -> p b a
forall k (p :: k +-> k) (a :: k) (b :: k).
DaggerProfunctor p =>
p a b -> p b a
dagger p a b
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 :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b, HasArrow Kleisli a b) =>
Kleisli a b
arr = p (UN KL a) (UN KL b) -> Kleisli (KL (UN KL a)) (KL (UN KL b))
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli p (UN KL a) (UN KL b)
forall (a :: k) (b :: k). (Ob a, Ob b, HasArrow p a b) => p a b
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(ThinProfunctor p, Ob a, Ob b, HasArrow p a b) =>
p a b
T.arr
  withArr :: forall (a :: KLEISLI p) (b :: KLEISLI p) r.
Kleisli a b -> ((HasArrow Kleisli a b, Ob a, Ob b) => r) -> r
withArr (Kleisli p a b
p) (HasArrow Kleisli a b, Ob a, Ob b) => r
r = p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: k) r.
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
ThinProfunctor p =>
p a b -> ((HasArrow p a b, Ob a, Ob b) => r) -> r
T.withArr p a b
p r
(HasArrow p a b, Ob a, Ob b) => r
(HasArrow Kleisli a b, Ob a, Ob b) => r
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 :: forall (a :: KLEISLI p) (b :: KLEISLI p).
(Ob a, Ob b) =>
Decision Kleisli a b (Holds Kleisli a b)
decide @(KL a) @(KL b) = (p (UN KL a) (UN KL b) -> Kleisli a b)
-> Decision p (UN KL a) (UN KL b) (Holds p (UN KL a) (UN KL b))
-> Decision Kleisli a b (Holds p (UN KL a) (UN KL b))
forall {k1} {j1} {k2} {j2} (p :: k1 -> j1 -> Type) (a :: k1)
       (b :: j1) (q :: k2 -> j2 -> Type) (c :: k2) (d :: j2) (h :: BOOL).
(p a b -> q c d) -> Decision p a b h -> Decision q c d h
mapDecision p (UN KL a) (UN KL b) -> Kleisli a b
p (UN KL a) (UN KL b) -> Kleisli (KL (UN KL a)) (KL (UN KL b))
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli (forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
forall (p :: k +-> k) (a :: k) (b :: k).
(DecidableProfunctor p, Ob a, Ob b) =>
Decision p a b (Holds p a b)
decide @p @a @b)
  toHolds :: forall (a :: KLEISLI p) (b :: KLEISLI p) r.
Kleisli a b -> ((Holds Kleisli a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds (Kleisli p a b
p) (Holds Kleisli a b ~ 'TRU, Ob a, Ob b) => r
r = p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall (a :: k) (b :: k) r.
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
DecidableProfunctor p =>
p a b -> ((Holds p a b ~ 'TRU, Ob a, Ob b) => r) -> r
toHolds p a b
p r
(Holds p a b ~ 'TRU, Ob a, Ob b) => r
(Holds Kleisli a b ~ 'TRU, Ob a, Ob b) => r
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 :: IndexedList (Objects (KLEISLI p))
finite = forall {j} {k} (w :: j -> k).
(Finite j, forall (a :: j). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects j))
forall (w :: k -> KLEISLI p).
(Finite k, forall (a :: k). KnownIndex a => KnownIndex (w a)) =>
IndexedList (MapWrap w (Objects k))
T.wrapFinite @KL
  withAtLookup :: forall (i :: Nat) r.
SNat i
-> ((Lookup (Objects (KLEISLI p)) i ~ At (KLEISLI p) i) => r) -> r
withAtLookup = forall {j} {k} (w :: j -> k) (i :: Nat) r.
Finite j =>
SNat i
-> ((Lookup (MapWrap w (Objects j)) i ~ FmapWrap w (At j i)) => r)
-> r
forall (w :: k -> KLEISLI p) (i :: Nat) r.
Finite k =>
SNat i
-> ((Lookup (MapWrap w (Objects k)) i ~ FmapWrap w (At k i)) => r)
-> r
T.withWrapAtLookup @KL

instance (T.Enumerable k, Promonad p) => T.Enumerable (KLEISLI (p :: CAT k)) where
  withIndex :: forall (a :: KLEISLI p) r. Ob a => (KnownIndex a => r) -> r
withIndex @(KL a) KnownIndex a => r
r = forall k (a :: k) r.
(Enumerable k, Ob a) =>
(KnownIndex a => r) -> r
T.withIndex @k @a r
KnownIndex (UN KL a) => r
KnownIndex a => r
r
  atOb :: forall (i :: Nat). SNat i -> AtOb (KLEISLI p) (At (KLEISLI p) i)
atOb SNat i
i = case forall k (i :: Nat). Enumerable k => SNat i -> AtOb k (At k i)
T.atOb @k SNat i
i of
    AtOb k (At k i)
T.AtJust -> AtOb (KLEISLI p) ('Just (KL a))
AtOb (KLEISLI p) (At (KLEISLI p) i)
forall k (a :: k). (Ob a, KnownIndex a) => AtOb k ('Just a)
T.AtJust
    AtOb k (At k i)
T.AtNothing -> AtOb (KLEISLI p) 'Nothing
AtOb (KLEISLI p) (At (KLEISLI p) i)
forall k. AtOb k 'Nothing
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 :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: j) (d :: j).
(c ~> a) -> (b ~> d) -> KleisliFree p a b -> KleisliFree p c d
dimap (Kleisli p a b
l) b ~> d
r (KleisliFree p a b
p) = p a d -> KleisliFree p (KL a) d
forall {k} (p :: k +-> k) (b :: k) (b :: k).
p b b -> KleisliFree p (KL b) b
KleisliFree ((b ~> d) -> p a b -> p a d
forall (b :: j) (d :: j) (a :: j). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap b ~> d
r p a b
p p a d -> p a a -> p a d
forall (b :: j) (c :: j) (a :: j). p b c -> p a b -> p a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b
p a a
l)
  (Ob a, Ob b) => r
r \\ :: forall (a :: KLEISLI p) (b :: j) r.
((Ob a, Ob b) => r) -> KleisliFree p a b -> r
\\ KleisliFree p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: j) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
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 :: forall (c :: k) (a :: k) (b :: KLEISLI p) (d :: KLEISLI p).
(c ~> a) -> (b ~> d) -> KleisliForget p a b -> KleisliForget p c d
dimap c ~> a
l (Kleisli p a b
r) (KleisliForget p a b
p) = p c b -> KleisliForget p c (KL b)
forall {k} (p :: k +-> k) (a :: k) (b :: k).
p a b -> KleisliForget p a (KL b)
KleisliForget (p a b
p b b
r p b b -> p c b -> p c b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (c ~> a) -> p a b -> p c b
forall (c :: k) (a :: k) (b :: k). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap c ~> a
l p a b
p)
  (Ob a, Ob b) => r
r \\ :: forall (a :: k) (b :: KLEISLI p) r.
((Ob a, Ob b) => r) -> KleisliForget p a b -> r
\\ KleisliForget p a b
p = r
(Ob a, Ob b) => r
(Ob a, Ob b) => r
r ((Ob a, Ob b) => r) -> p a b -> r
forall (a :: k) (b :: k) r. ((Ob a, Ob b) => r) -> p a b -> r
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j) r.
Profunctor p =>
((Ob a, Ob b) => r) -> p a b -> r
\\ p a b
p

instance (Promonad p) => Proadjunction (KleisliFree p) (KleisliForget p) where
  unit :: forall (a :: k).
Ob a =>
(:.:) (KleisliForget p) (KleisliFree p) a a
unit = p a a -> KleisliForget p a (KL a)
forall {k} (p :: k +-> k) (a :: k) (b :: k).
p a b -> KleisliForget p a (KL b)
KleisliForget p a a
forall (a :: k). Ob a => p a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id KleisliForget p a (KL a)
-> KleisliFree p (KL a) a
-> (:.:) (KleisliForget p) (KleisliFree p) a a
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: p a a -> KleisliFree p (KL a) a
forall {k} (p :: k +-> k) (b :: k) (b :: k).
p b b -> KleisliFree p (KL b) b
KleisliFree p a a
forall (a :: k). Ob a => p a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id
  counit :: (KleisliFree p :.: KleisliForget p) :~> (~>)
counit (KleisliFree p a b
p :.: KleisliForget p b b
q) = p a b -> Kleisli (KL a) (KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli (p b b
q p b b -> p a b -> p a b
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. p a b
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 :: forall {k} {k} (f :: k +-> k) (a :: k) (b :: k).
Representable f =>
Kleisli (KL a) (KL b) -> ((f % a) ~> (f % b), Obj a, Obj b)
unlift (Kleisli (RepCostar (f % a) ~> b
f :.: f b b
g)) = (f b b -> b ~> (f % b)
forall (a :: k) (b :: k). f a b -> a ~> (f % b)
forall {j} {k} (p :: j +-> k) (a :: k) (b :: j).
Representable p =>
p a b -> a ~> (p % b)
index f b b
g (b ~> (f % b)) -> ((f % a) ~> b) -> (f % a) ~> (f % b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (f % a) ~> b
(f % a) ~> b
f, Obj a
forall k (a :: k). (CategoryOf k, Ob a) => Obj a
Obj, f b b -> Obj b
forall {k1} {k2} (a :: k2) (b :: k1) (p :: k1 +-> k2).
Profunctor p =>
p a b -> Obj b
tgt f b b
g)

pattern LiftF
  :: (Representable (f :: j +-> k)) => (Ob (a :: j), Ob b) => (f % a ~> f % b) -> Kleisli (KL a :: LIFTEDF f) (KL b)
pattern $bLiftF :: forall j k (f :: j +-> k) (a :: j) (b :: j).
(Representable f, Ob a, Ob b) =>
((f % a) ~> (f % b)) -> Kleisli (KL a) (KL b)
$mLiftF :: forall {r} {j} {k} {f :: j +-> k} {a :: j} {b :: j}.
Representable f =>
Kleisli (KL a) (KL b)
-> ((Ob a, Ob b) => ((f % a) ~> (f % b)) -> r) -> ((# #) -> r) -> r
LiftF f <- (unlift -> (f, Obj, Obj))
  where
    LiftF (f % a) ~> (f % b)
f = (:.:) (RepCostar f) f a b -> Kleisli (KL a) (KL b)
forall {k} (p :: CAT k) (b :: k) (b :: k).
p b b -> Kleisli (KL b) (KL b)
Kleisli (((f % a) ~> (f % b)) -> RepCostar f a (f % b)
forall {k} {j} (a :: k) (p :: k +-> j) (b :: j).
Ob a =>
((p % a) ~> b) -> RepCostar p a b
RepCostar (f % a) ~> (f % b)
f RepCostar f a (f % b) -> f (f % b) b -> (:.:) (RepCostar f) f a b
forall {j} {k} {i} (b :: j) (a :: k) (c :: i) (p :: j +-> k)
       (q :: i +-> j).
p a b -> q b c -> (:.:) p q a c
:.: f (f % b) b
forall (a :: j). Ob a => f (f % a) a
forall {j} {k} (p :: j +-> k) (a :: j).
(Representable p, Ob a) =>
p (p % a) a
repUniv)

{-# COMPLETE LiftF #-}