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 :: Monad m -> Obj ~> b -> (a ~> (m :% b)) -> Kleisli ~> m a b

Instances

(Dom m ~ ~>, Cod m ~ ~>, Category ~>, Functor m) => Category (Kleisli ~> m)

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

data KleisliAdjF (~>) m where

Constructors

KleisliAdjF :: Monad m -> KleisliAdjF ~> m

Instances

(Dom m ~ ~>, Cod m ~ ~>, Category ~>, Functor m) => Functor (KleisliAdjF ~> m)

data KleisliAdjG (~>) m where

Constructors

KleisliAdjG :: Monad m -> KleisliAdjG ~> m

Instances

(Dom m ~ ~>, Cod m ~ ~>, Category ~>, Functor m) => Functor (KleisliAdjG ~> m)

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