Safe Haskell	None
Language	GHC2024

Proarrow.Category.Instance.Kleisli

Description

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 CopyDiscard structure lift from the base category when p cooperates (e.g. is a MonoidalProfunctor).

Synopsis

data KLEISLI (p :: CAT k) = KL k
data Kleisli (a :: KLEISLI p) (b :: KLEISLI p) where
- Kleisli :: forall {k} (p :: CAT k) (a1 :: k) (b1 :: k). {..} -> Kleisli ('KL a1 :: KLEISLI p) ('KL b1 :: KLEISLI p)
arr :: forall {k} (p :: CAT k) (a :: k) (b :: k). Promonad p => (a ~> b) -> Kleisli ('KL a :: KLEISLI p) ('KL b :: KLEISLI p)
data KleisliFree (p :: k +-> k) (a :: KLEISLI p) (b :: k) where
- KleisliFree :: forall {k} (p :: k +-> k) (a1 :: k) (b :: k). p a1 b -> KleisliFree p ('KL a1 :: KLEISLI p) b
data KleisliForget (p :: k +-> k) (a :: k) (b :: KLEISLI p) where
- KleisliForget :: forall {k} (p :: k +-> k) (a :: k) (b1 :: k). p a b1 -> KleisliForget p a ('KL b1 :: KLEISLI p)
type LIFTEDF (f :: j +-> k) = KLEISLI (RepCostar f :.: f)
pattern LiftF :: forall j k (f :: j +-> k) (a :: j) (b :: j). Representable f => (Ob a, Ob b) => ((f % a) ~> (f % b)) -> Kleisli ('KL a :: KLEISLI (RepCostar f :.: f)) ('KL b :: KLEISLI (RepCostar f :.: f))

Documentation

data KLEISLI (p :: CAT k) Source Github #

Constructors

KL k

Instances

Instances details

Promonad p => Profunctor (KleisliFree p :: KLEISLI p -> j -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

dimap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> KleisliFree p a b -> KleisliFree p c d Source Github #

lmap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: j). (c ~> a) -> KleisliFree p a b -> KleisliFree p c b Source Github #

rmap :: forall (b :: j) (d :: j) (a :: KLEISLI p). (b ~> d) -> KleisliFree p a b -> KleisliFree p a d Source Github #

(\\) :: forall (a :: KLEISLI p) (b :: j) r. ((Ob a, Ob b) => r) -> KleisliFree p a b -> r Source Github #

Promonad p => Proadjunction (KleisliFree p :: KLEISLI p -> k -> Type) (KleisliForget p :: k -> KLEISLI p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

unit :: forall (a :: k). Ob a => (KleisliForget p :.: KleisliFree p) a a Source Github #

counit :: (KleisliFree p :.: KleisliForget p) :~> ((~>) :: CAT (KLEISLI p)) Source Github #

(Enumerable k, Promonad p) => Enumerable (KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

withIndex :: forall (a :: KLEISLI p) r. Ob a => (KnownIndex a => r) -> r Source Github #

withOb :: forall (a :: KLEISLI p) r. KnownIndex a => (Ob a => r) -> r Source Github #

atOb :: forall (i :: Nat). SNat i -> AtOb (KLEISLI p) (At (KLEISLI p) i) Source Github #

Finite k => Finite (KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Associated Types

type Objects (KLEISLI p)
Instance details Defined in Proarrow.Category.Instance.Kleisli type Objects (KLEISLI p) = MapWrap ('KL :: k -> KLEISLI p) (Objects k)

Methods

finite :: IndexedList (Objects (KLEISLI p)) Source Github #

withAtLookup :: forall (i :: Nat) r. SNat i -> (Lookup (Objects (KLEISLI p)) i ~ At (KLEISLI p) i => r) -> r Source Github #

Indexed k => Indexed (KLEISLI p) Source Github #

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 details

Defined in Proarrow.Category.Instance.Kleisli

(Promonad p, MonoidalProfunctor p) => Monoidal (KLEISLI p) Source Github #

If the promonad is a monoidal profunctor, then its Kleisli category is a monoidal category.

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Instance.Kleisli type Unit = 'KL (Unit :: k) :: KLEISLI p

Methods

withOb2 :: forall (a :: KLEISLI p) (b :: KLEISLI p) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github #

leftUnitor :: forall (a :: KLEISLI p). Ob a => ((Unit :: KLEISLI p) ** a) ~> a Source Github #

leftUnitorInv :: forall (a :: KLEISLI p). Ob a => a ~> ((Unit :: KLEISLI p) ** a) Source Github #

rightUnitor :: forall (a :: KLEISLI p). Ob a => (a ** (Unit :: KLEISLI p)) ~> a Source Github #

rightUnitorInv :: forall (a :: KLEISLI p). Ob a => a ~> (a ** (Unit :: KLEISLI p)) Source Github #

associator :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github #

associatorInv :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github #

(Promonad p, MonoidalProfunctor p, SymMonoidal k) => SymMonoidal (KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

swap :: forall (a :: KLEISLI p) (b :: KLEISLI p). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Github #

Closed (KLEISLI (Cont r)) Source Github #

Instance details

Defined in Proarrow.Promonad.Cont

Methods

withObExp :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)) r0. (Ob a, Ob b) => (Ob (a ~~> b) => r0) -> r0 Source Github #

curry :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)) (c :: KLEISLI (Cont r)). (Ob a, Ob b) => ((a ** b) ~> c) -> a ~> (b ~~> c) Source Github #

apply :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)). (Ob a, Ob b) => ((a ~~> b) ** a) ~> b Source Github #

(^^^) :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)) (x :: KLEISLI (Cont r)) (y :: KLEISLI (Cont r)). (b ~> y) -> (x ~> a) -> (a ~~> b) ~> (x ~~> y) Source Github #

(Promonad p, MonoidalProfunctor p, CopyDiscard k) => CopyDiscard (KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

copy :: forall (a :: KLEISLI p). Ob a => a ~> (a ** a) Source Github #

discard :: forall (a :: KLEISLI p). Ob a => a ~> (Unit :: KLEISLI p) Source Github #

Dialogue (KLEISLI (Cont r)) Source Github #

Instance details

Defined in Proarrow.Promonad.Cont

Methods

withObDual :: forall (a :: KLEISLI (Cont r)) r0. Ob a => (Ob (Dual a) => r0) -> r0 Source Github #

dual :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)). (a ~> b) -> Dual b ~> Dual a Source Github #

linDist :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)) (c :: KLEISLI (Cont r)). (Ob a, Ob b, Ob c) => ((a ** b) ~> Dual c) -> a ~> Dual (b ** c) Source Github #

linDistInv :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)) (c :: KLEISLI (Cont r)). (Ob a, Ob b, Ob c) => (a ~> Dual (b ** c)) -> (a ** b) ~> Dual c Source Github #

doubleNegInv :: forall (a :: KLEISLI (Cont r)). Ob a => a ~> Dual (Dual a) Source Github #

(Distributive k, Monad p, DistributiveProfunctor p) => Distributive (KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

distL :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p). (Ob a, Ob b, Ob c) => (a ** (b || c)) ~> ((a ** b) || (a ** c)) Source Github #

distR :: forall (a :: KLEISLI p) (b :: KLEISLI p) (c :: KLEISLI p). (Ob a, Ob b, Ob c) => ((a || b) ** c) ~> ((a ** c) || (b ** c)) Source Github #

absorbL :: forall (a :: KLEISLI p). Ob a => (a ** (InitialObject :: KLEISLI p)) ~> (InitialObject :: KLEISLI p) Source Github #

absorbR :: forall (a :: KLEISLI p). Ob a => ((InitialObject :: KLEISLI p) ** a) ~> (InitialObject :: KLEISLI p) Source Github #

StarAutonomous (KLEISLI (Cont r)) Source Github #

Instance details

Defined in Proarrow.Promonad.Cont

Methods

dualInv :: forall (a :: KLEISLI (Cont r)) (b :: KLEISLI (Cont r)). (Ob a, Ob b) => (Dual a ~> Dual b) -> b ~> a Source Github #

doubleNeg :: forall (a :: KLEISLI (Cont r)). Ob a => Dual (Dual a) ~> a Source Github #

(HasBinaryCoproducts k, Monad p, MonoidalProfunctor (Coprod p)) => HasBinaryCoproducts (KLEISLI p) Source Github #

Coproducts lift for the same reason as the initial object: for a Monad p (-) z is a representable presheaf.

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

withObCoprod :: forall (a :: KLEISLI p) (b :: KLEISLI p) r. (Ob a, Ob b) => (Ob (a || b) => r) -> r Source Github #

lft :: forall (a :: KLEISLI p) (b :: KLEISLI p). (Ob a, Ob b) => a ~> (a || b) Source Github #

rgt :: forall (a :: KLEISLI p) (b :: KLEISLI p). (Ob a, Ob b) => b ~> (a || b) Source Github #

(|||) :: forall (x :: KLEISLI p) (a :: KLEISLI p) (y :: KLEISLI p). (x ~> a) -> (y ~> a) -> (x || y) ~> a Source Github #

(+++) :: forall (a :: KLEISLI p) (b :: KLEISLI p) (x :: KLEISLI p) (y :: KLEISLI p). (a ~> x) -> (b ~> y) -> (a || b) ~> (x || y) Source Github #

(HasInitialObject k, Monad p) => HasInitialObject (KLEISLI p) Source Github #

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 details

Defined in Proarrow.Category.Instance.Kleisli

Associated Types

type InitialObject
Instance details Defined in Proarrow.Category.Instance.Kleisli type InitialObject = 'KL (InitialObject :: k) :: KLEISLI p

Methods

initiate :: forall (a :: KLEISLI p). Ob a => (InitialObject :: KLEISLI p) ~> a Source Github #

Promonad p => CategoryOf (KLEISLI p) Source Github #

Every promonad makes a category.

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Instance.Kleisli type (~>) = Kleisli :: KLEISLI p -> KLEISLI p -> Type

(Cartesian k, Comonad p, MonoidalProfunctor p) => HasBinaryProducts (KLEISLI p) Source Github #

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 details

Defined in Proarrow.Category.Instance.Kleisli

Methods

withObProd :: forall (a :: KLEISLI p) (b :: KLEISLI p) r. (Ob a, Ob b) => (Ob (a && b) => r) -> r Source Github #

fst :: forall (a :: KLEISLI p) (b :: KLEISLI p). (Ob a, Ob b) => (a && b) ~> a Source Github #

snd :: forall (a :: KLEISLI p) (b :: KLEISLI p). (Ob a, Ob b) => (a && b) ~> b Source Github #

(&&&) :: forall (a :: KLEISLI p) (x :: KLEISLI p) (y :: KLEISLI p). (a ~> x) -> (a ~> y) -> a ~> (x && y) Source Github #

(***) :: forall (a :: KLEISLI p) (b :: KLEISLI p) (x :: KLEISLI p) (y :: KLEISLI p). (a ~> x) -> (b ~> y) -> (a && b) ~> (x && y) Source Github #

(HasTerminalObject k, Comonad p) => HasTerminalObject (KLEISLI p) Source Github #

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 HaskValue c every element of c is an arrow into the terminal object, so uniqueness fails.

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Associated Types

type TerminalObject
Instance details Defined in Proarrow.Category.Instance.Kleisli type TerminalObject = 'KL (TerminalObject :: k) :: KLEISLI p

Methods

terminate :: forall (a :: KLEISLI p). Ob a => a ~> (TerminalObject :: KLEISLI p) Source Github #

(Promonad p, MonoidalProfunctor p, CopyDiscard k, Ob a) => CocommutativeComonoid (a :: KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

(Promonad p, MonoidalProfunctor p, CopyDiscard k, Ob a) => Comonoid (a :: KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

counit :: a ~> (Unit :: KLEISLI p) Source Github #

comult :: a ~> (a ** a) Source Github #

Promonad p => Profunctor (KleisliForget p :: k -> KLEISLI p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

dimap :: forall (c :: k) (a :: k) (b :: KLEISLI p) (d :: KLEISLI p). (c ~> a) -> (b ~> d) -> KleisliForget p a b -> KleisliForget p c d Source Github #

lmap :: forall (c :: k) (a :: k) (b :: KLEISLI p). (c ~> a) -> KleisliForget p a b -> KleisliForget p c b Source Github #

rmap :: forall (b :: KLEISLI p) (d :: KLEISLI p) (a :: k). (b ~> d) -> KleisliForget p a b -> KleisliForget p a d Source Github #

(\\) :: forall (a :: k) (b :: KLEISLI p) r. ((Ob a, Ob b) => r) -> KleisliForget p a b -> r Source Github #

(DaggerProfunctor p, Promonad p) => DaggerProfunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

dagger :: forall (a :: KLEISLI p) (b :: KLEISLI p). Kleisli a b -> Kleisli b a Source Github #

Promonad p => Promonad (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

id :: forall (a :: KLEISLI p). Ob a => Kleisli a a Source Github #

(.) :: forall (b :: KLEISLI p) (c :: KLEISLI p) (a :: KLEISLI p). Kleisli b c -> Kleisli a b -> Kleisli a c Source Github #

(DecidableProfunctor p, Promonad p) => DecidableProfunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

decide :: forall (a :: KLEISLI p) (b :: KLEISLI p). (Ob a, Ob b) => Decision (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b (Holds (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b) Source Github #

toHolds :: forall (a :: KLEISLI p) (b :: KLEISLI p) r. Kleisli a b -> ((Holds (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #

(ThinProfunctor p, Promonad p) => ThinProfunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

arr :: forall (a :: KLEISLI p) (b :: KLEISLI p). (Ob a, Ob b, HasArrow (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b) => Kleisli a b Source Github #

withArr :: forall (a :: KLEISLI p) (b :: KLEISLI p) r. Kleisli a b -> ((HasArrow (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b, Ob a, Ob b) => r) -> r Source Github #

(Promonad p, MonoidalProfunctor p) => MonoidalProfunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

one :: Kleisli (Unit :: KLEISLI p) (Unit :: KLEISLI p) Source Github #

(**) :: forall (x1 :: KLEISLI p) (x2 :: KLEISLI p) (y1 :: KLEISLI p) (y2 :: KLEISLI p). Kleisli x1 x2 -> Kleisli y1 y2 -> Kleisli (x1 ** y1) (x2 ** y2) Source Github #

Promonad p => Profunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

Methods

dimap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: KLEISLI p) (d :: KLEISLI p). (c ~> a) -> (b ~> d) -> Kleisli a b -> Kleisli c d Source Github #

lmap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: KLEISLI p). (c ~> a) -> Kleisli a b -> Kleisli c b Source Github #

rmap :: forall (b :: KLEISLI p) (d :: KLEISLI p) (a :: KLEISLI p). (b ~> d) -> Kleisli a b -> Kleisli a d Source Github #

(\\) :: forall (a :: KLEISLI p) (b :: KLEISLI p) r. ((Ob a, Ob b) => r) -> Kleisli a b -> r Source Github #

type Objects (KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type Objects (KLEISLI p) = MapWrap ('KL :: k -> KLEISLI p) (Objects k)

type Unit Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type Unit = 'KL (Unit :: k) :: KLEISLI p

type InitialObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type InitialObject = 'KL (InitialObject :: k) :: KLEISLI p

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type (~>) = Kleisli :: KLEISLI p -> KLEISLI p -> Type

type TerminalObject Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type TerminalObject = 'KL (TerminalObject :: k) :: KLEISLI p

type At (KLEISLI p) i Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type At (KLEISLI p) i = FmapWrap ('KL :: k -> KLEISLI p) (At k i)

type Index (a :: KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type Index (a :: KLEISLI p) = Index (UN ('KL :: k -> KLEISLI p) a)

type Ob (a :: KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type Ob (a :: KLEISLI p) = WrappedOb ('KL :: k -> KLEISLI p) a

type (a :: KLEISLI p) ** (b :: KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type (a :: KLEISLI p) ** (b :: KLEISLI p) = 'KL (UN ('KL :: k -> KLEISLI p) a ** UN ('KL :: k -> KLEISLI p) b) :: KLEISLI p

type (a :: KLEISLI (Cont r)) ~~> (b :: KLEISLI (Cont r)) Source Github #

Instance details

Defined in Proarrow.Promonad.Cont

type (a :: KLEISLI (Cont r)) ~~> (b :: KLEISLI (Cont r)) = ExpSA a b

type (a :: KLEISLI p) || (b :: KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type (a :: KLEISLI p) || (b :: KLEISLI p) = 'KL (UN ('KL :: k -> KLEISLI p) a || UN ('KL :: k -> KLEISLI p) b) :: KLEISLI p

type (a :: KLEISLI p) && (b :: KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type (a :: KLEISLI p) && (b :: KLEISLI p) = 'KL (UN ('KL :: k -> KLEISLI p) a && UN ('KL :: k -> KLEISLI p) b) :: KLEISLI p

type HasArrow (Kleisli :: KLEISLI p -> KLEISLI p -> Type) ('KL a :: KLEISLI p) ('KL b :: KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type HasArrow (Kleisli :: KLEISLI p -> KLEISLI p -> Type) ('KL a :: KLEISLI p) ('KL b :: KLEISLI p) = HasArrow p a b

type Holds (Kleisli :: KLEISLI p -> KLEISLI p -> Type) ('KL a :: KLEISLI p) ('KL b :: KLEISLI p) Source Github #

Instance details

Defined in Proarrow.Category.Instance.Kleisli

type Holds (Kleisli :: KLEISLI p -> KLEISLI p -> Type) ('KL a :: KLEISLI p) ('KL b :: KLEISLI p) = Holds p a b

type Dual ('KL a :: KLEISLI (Cont r)) Source Github #

Instance details

Defined in Proarrow.Promonad.Cont

type Dual ('KL a :: KLEISLI (Cont r)) = 'KL (a ~~> r) :: KLEISLI (Cont r)

data Kleisli (a :: KLEISLI p) (b :: KLEISLI p) where Source Github #

The arrows of the promonad p, wrapped as a category on the KLEISLI-wrapped kind.

Constructors

Kleisli
Fields :: forall {k} (p :: CAT k) (a1 :: k) (b1 :: k). { unKleisli :: p a1 b1 } -> Kleisli ('KL a1 :: KLEISLI p) ('KL b1 :: KLEISLI p)

Instances

Instances details

(DaggerProfunctor p, Promonad p) => DaggerProfunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods dagger :: forall (a :: KLEISLI p) (b :: KLEISLI p). Kleisli a b -> Kleisli b a Source Github #
Promonad p => Promonad (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods id :: forall (a :: KLEISLI p). Ob a => Kleisli a a Source Github # (.) :: forall (b :: KLEISLI p) (c :: KLEISLI p) (a :: KLEISLI p). Kleisli b c -> Kleisli a b -> Kleisli a c Source Github #
(DecidableProfunctor p, Promonad p) => DecidableProfunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods decide :: forall (a :: KLEISLI p) (b :: KLEISLI p). (Ob a, Ob b) => Decision (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b (Holds (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b) Source Github # toHolds :: forall (a :: KLEISLI p) (b :: KLEISLI p) r. Kleisli a b -> ((Holds (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b ~ 'TRU, Ob a, Ob b) => r) -> r Source Github #
(ThinProfunctor p, Promonad p) => ThinProfunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods arr :: forall (a :: KLEISLI p) (b :: KLEISLI p). (Ob a, Ob b, HasArrow (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b) => Kleisli a b Source Github # withArr :: forall (a :: KLEISLI p) (b :: KLEISLI p) r. Kleisli a b -> ((HasArrow (Kleisli :: KLEISLI p -> KLEISLI p -> Type) a b, Ob a, Ob b) => r) -> r Source Github #
(Promonad p, MonoidalProfunctor p) => MonoidalProfunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods one :: Kleisli (Unit :: KLEISLI p) (Unit :: KLEISLI p) Source Github # () :: forall (x1 :: KLEISLI p) (x2 :: KLEISLI p) (y1 :: KLEISLI p) (y2 :: KLEISLI p). Kleisli x1 x2 -> Kleisli y1 y2 -> Kleisli (x1 y1) (x2 ** y2) Source Github #
Promonad p => Profunctor (Kleisli :: KLEISLI p -> KLEISLI p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods dimap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: KLEISLI p) (d :: KLEISLI p). (c ~> a) -> (b ~> d) -> Kleisli a b -> Kleisli c d Source Github # lmap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: KLEISLI p). (c ~> a) -> Kleisli a b -> Kleisli c b Source Github # rmap :: forall (b :: KLEISLI p) (d :: KLEISLI p) (a :: KLEISLI p). (b ~> d) -> Kleisli a b -> Kleisli a d Source Github # (\\) :: forall (a :: KLEISLI p) (b :: KLEISLI p) r. ((Ob a, Ob b) => r) -> Kleisli a b -> r Source Github #
type HasArrow (Kleisli :: KLEISLI p -> KLEISLI p -> Type) ('KL a :: KLEISLI p) ('KL b :: KLEISLI p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli type HasArrow (Kleisli :: KLEISLI p -> KLEISLI p -> Type) ('KL a :: KLEISLI p) ('KL b :: KLEISLI p) = HasArrow p a b
type Holds (Kleisli :: KLEISLI p -> KLEISLI p -> Type) ('KL a :: KLEISLI p) ('KL b :: KLEISLI p) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli type Holds (Kleisli :: KLEISLI p -> KLEISLI p -> Type) ('KL a :: KLEISLI p) ('KL b :: KLEISLI p) = Holds p a b

arr :: forall {k} (p :: CAT k) (a :: k) (b :: k). Promonad p => (a ~> b) -> Kleisli ('KL a :: KLEISLI p) ('KL b :: KLEISLI p) Source Github #

data KleisliFree (p :: k +-> k) (a :: KLEISLI p) (b :: k) where Source Github #

The free half of the Kleisli adjunction (Proadjunction below), embedding k into the Kleisli category of p.

Constructors

KleisliFree :: forall {k} (p :: k +-> k) (a1 :: k) (b :: k). p a1 b -> KleisliFree p ('KL a1 :: KLEISLI p) b

Instances

Instances details

Promonad p => Profunctor (KleisliFree p :: KLEISLI p -> j -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods dimap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> KleisliFree p a b -> KleisliFree p c d Source Github # lmap :: forall (c :: KLEISLI p) (a :: KLEISLI p) (b :: j). (c ~> a) -> KleisliFree p a b -> KleisliFree p c b Source Github # rmap :: forall (b :: j) (d :: j) (a :: KLEISLI p). (b ~> d) -> KleisliFree p a b -> KleisliFree p a d Source Github # (\\) :: forall (a :: KLEISLI p) (b :: j) r. ((Ob a, Ob b) => r) -> KleisliFree p a b -> r Source Github #
Promonad p => Proadjunction (KleisliFree p :: KLEISLI p -> k -> Type) (KleisliForget p :: k -> KLEISLI p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods unit :: forall (a :: k). Ob a => (KleisliForget p :.: KleisliFree p) a a Source Github # counit :: (KleisliFree p :.: KleisliForget p) :~> ((~>) :: CAT (KLEISLI p)) Source Github #

data KleisliForget (p :: k +-> k) (a :: k) (b :: KLEISLI p) where Source Github #

The forgetful half of the Kleisli adjunction, mapping Kleisli objects back to k.

Constructors

KleisliForget :: forall {k} (p :: k +-> k) (a :: k) (b1 :: k). p a b1 -> KleisliForget p a ('KL b1 :: KLEISLI p)

Instances

Instances details

Promonad p => Proadjunction (KleisliFree p :: KLEISLI p -> k -> Type) (KleisliForget p :: k -> KLEISLI p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods unit :: forall (a :: k). Ob a => (KleisliForget p :.: KleisliFree p) a a Source Github # counit :: (KleisliFree p :.: KleisliForget p) :~> ((~>) :: CAT (KLEISLI p)) Source Github #
Promonad p => Profunctor (KleisliForget p :: k -> KLEISLI p -> Type) Source Github #
Instance details Defined in Proarrow.Category.Instance.Kleisli Methods dimap :: forall (c :: k) (a :: k) (b :: KLEISLI p) (d :: KLEISLI p). (c ~> a) -> (b ~> d) -> KleisliForget p a b -> KleisliForget p c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: KLEISLI p). (c ~> a) -> KleisliForget p a b -> KleisliForget p c b Source Github # rmap :: forall (b :: KLEISLI p) (d :: KLEISLI p) (a :: k). (b ~> d) -> KleisliForget p a b -> KleisliForget p a d Source Github # (\\) :: forall (a :: k) (b :: KLEISLI p) r. ((Ob a, Ob b) => r) -> KleisliForget p a b -> r Source Github #

type LIFTEDF (f :: j +-> k) = KLEISLI (RepCostar f :.: f) Source Github #

Categories lifted by a representable profunctor: f % a ~> f % b are kleisli categories on promonads induced by f.

pattern LiftF :: forall j k (f :: j +-> k) (a :: j) (b :: j). Representable f => (Ob a, Ob b) => ((f % a) ~> (f % b)) -> Kleisli ('KL a :: KLEISLI (RepCostar f :.: f)) ('KL b :: KLEISLI (RepCostar f :.: f)) Source Github #