Kleisli adjunction

Given monad over a category , let be the Kleisli category of . Given an object in , write to mean viewed as an object of . Given an arrow in , write to mean viewed as an arrow in .

Define a functor by

Further define a functor by

type Kleisli m a b = a -> m b

f :: Monad m => (a -> b) -> Kelsli m a b
f h = return . h

g :: Monad m => Kleisli m a b -> (m a -> m b)
g h = join . fmap h

Then these functors form an adjunction with unit and counit

Furthermore, .

Of course, is a comonad. Explicitly, the comonad is , where

kmap :: Monad m => Kleisli m a b -> Kleisli m (m a) (m b)
kmap = return . (>>= f) -- equivalent to return . join . fmap f

kextract :: Monad m => m (m a) -> m a
kextract = join

kextend :: Monad m => Kleisli (m a) (m (m a))
kextend = return . return