Data.Category.Kleisli

This is an attempt at the Kleisli category, and the construction of an adjunction for each monad.

Documentation

data Kleisli m a b where

Constructors

Kleisli :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b

Instances

Category (Kleisli m)

The category of Kleisli arrows.

Methods

src :: Kleisli m a b -> Obj (Kleisli m) a

tgt :: Kleisli m a b -> Obj (Kleisli m) b

(.) :: Kleisli m b c -> Kleisli m a b -> Kleisli m a c

kleisliId :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj k a -> Kleisli m a a

data KleisliAdjF m

Constructors

KleisliAdjF (Monad m)

Instances

(Functor m, (~) (* -> * -> *) (Dom m) k, (~) (* -> * -> *) (Cod m) k) => Functor (KleisliAdjF m)

Associated Types

type Dom (KleisliAdjF m) :: * -> * -> *

type Cod (KleisliAdjF m) :: * -> * -> *

type (KleisliAdjF m) :% a :: *

Methods

(%) :: KleisliAdjF m -> Dom (KleisliAdjF m) a b -> Cod (KleisliAdjF m) (KleisliAdjF m :% a) (KleisliAdjF m :% b)

type Dom (KleisliAdjF m)

type Dom (KleisliAdjF m) = Dom m

type Cod (KleisliAdjF m)

type Cod (KleisliAdjF m) = Kleisli m

type (KleisliAdjF m) :% a

type (KleisliAdjF m) :% a = a

data KleisliAdjG m

Constructors

KleisliAdjG (Monad m)

Instances

(Functor m, (~) (* -> * -> *) (Dom m) k, (~) (* -> * -> *) (Cod m) k) => Functor (KleisliAdjG m)

Associated Types

type Dom (KleisliAdjG m) :: * -> * -> *

type Cod (KleisliAdjG m) :: * -> * -> *

type (KleisliAdjG m) :% a :: *

Methods

(%) :: KleisliAdjG m -> Dom (KleisliAdjG m) a b -> Cod (KleisliAdjG m) (KleisliAdjG m :% a) (KleisliAdjG m :% b)

type Dom (KleisliAdjG m)

type Dom (KleisliAdjG m) = Kleisli m

type Cod (KleisliAdjG m)

type Cod (KleisliAdjG m) = Dom m

type (KleisliAdjG m) :% a

type (KleisliAdjG m) :% a = (:%) m a

kleisliAdj :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Adjunction (Kleisli m) k (KleisliAdjF m) (KleisliAdjG m)