Data.Category.Kleisli

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

Documentation

class Functor m => Pointed m where

Methods

point :: m -> Id (Dom m) :~> m

class Pointed m => Monad m where

Methods

join :: m -> (m :.: m) :~> m

data Kleisli (~>) m a b where

Constructors

Kleisli :: m -> Obj ~> b -> (a ~> (m :% b)) -> Kleisli ~> m a b

Instances

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

data KleisliAdjF (~>) m where

Constructors

KleisliAdjF :: (Category ~>, Monad m, Dom m ~ ~>, Cod m ~ ~>) => m -> KleisliAdjF ~> m

Instances

Functor (KleisliAdjF ~> m)

data KleisliAdjG (~>) m where

Constructors

KleisliAdjG :: (Category ~>, Monad m, Dom m ~ ~>, Cod m ~ ~>) => m -> KleisliAdjG ~> m

Instances

Functor (KleisliAdjG ~> m)

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