Question

In category theory, a monad can be constructed from two adjoint functors. In particular, if C and D are categories and F : C --> D and G : D --> C are adjoint functors, in the sense that there is a bijection

hom(FX,Y) = hom(X,GY)

for each X in C and Y in D then the composition G o F : C --> C is a monad.


One such pair of adjoint functors can be given by fixing a type b and taking F and G to be

data F b a = F (a,b)
data G b a = G (b -> a)

instance Functor (F b) where
  fmap f (F (a,b)) = F (f a, b)

instance Functor (G b) where
  fmap f (G g) = G (f . g)

and the bijection between hom-sets is given (modulo constructors) by currying:

iso1 :: (F b a -> c) -> a -> G b c
iso1 f = \a -> G $ \b -> f (F (a,b))

iso2 :: (a -> G b c) -> F b a -> c
iso2 g = \(F (a,b)) -> let (G g') = g a in g' b

in which case the corresponding monad is

data M b a = M { unM :: b -> (a,b) }

instance Monad (M b) where
    return a    = M (\b -> (a,b))
    (M f) >>= g = M (\r -> let (a,r') = f r in unM (g r') a)

I don't know what the name for this monad should be, except that it seems to be something like a reader monad that carries around a piece of over-writeable information (edit: dbaupp points out in the comments that this is the State monad.)

So the State monad can be "decomposed" as the pair of adjoint functors F and G, and we could write

State = G . F

So far, so good.


I'm now trying to figure out how to decompose other common monads into pairs of adjoint functors - for example Maybe, [], Reader, Writer, Cont - but I can't figure out what the pairs of adjoint functors that we can "decompose" them into are.

The only simple case seems to be the Identity monad, which can be decomposed into any pair of functors F and G such that F is inverse to G (in particularly, you could just take F = Identity and G = Identity).

Can anyone shed some light?

Was it helpful?

Solution

What you're looking for is Kleisli category. It was originally developed to show that every monad can be constructed from two adjoint functors.

The problem is that Haskell Functor is not a generic functor, it's an endo-functor in the Haskell category. So we need something different (AFAIK) to represent functors between other categories:

{-# LANGUAGE FunctionalDependencies, KindSignatures #-}
import Control.Arrow
import Control.Category hiding ((.))
import qualified Control.Category as C
import Control.Monad

class (Category c, Category d) => CFunctor f c d | f -> c d where
    cfmap :: c a b -> d (f a) (f b)

Notice that if we take -> for both c and d we get an endo-functor of the Haskell category, which is just the type of fmap:

cfmap :: (a -> b) -> (f a -> f b)

Now we have explicit type class that represents functors between two given categories c and d and we can express the two adjoint functors for a given monad. The left one maps an object a to just a and maps a morphism f to (return .) f:

-- m is phantom, hence the explicit kind is required
newtype LeftAdj (m :: * -> *) a = LeftAdj { unLeftAdj :: a }
instance Monad m => CFunctor (LeftAdj m) (->) (Kleisli m) where
    cfmap f = Kleisli $ liftM LeftAdj . return . f . unLeftAdj
    -- we could also express it as liftM LeftAdj . (return .) f . unLeftAdj

The right one maps an object a to object m a and maps a morphism g to join . liftM g, or equivalently to (=<<) g:

newtype RightAdj m a = RightAdj { unRightAdj :: m a }
instance Monad m => CFunctor (RightAdj m) (Kleisli m) (->) where
    cfmap (Kleisli g) = RightAdj . join . liftM g . unRightAdj
    -- this can be shortened as RightAdj . (=<<) g . unRightAdj

(If anybody know a better way how to express this in Haskell, please let me know.)

OTHER TIPS

  • Maybe comes from the free functor into the category of pointed sets and the forgetful functor back
  • [] comes from the free functor into the category of monoids and the forgetful functor back

But neither of these categories are subcategories of Hask.

As you observe, every pair of adjoint functors gives rise to a monad. The converse holds too: every monad arises in that way. In fact, it does so in two canonical ways. One is the Kleisli construction Petr describes; the other is the Eilenberg-Moore construction. Indeed, Kleisli is the initial such way and E-M the terminal one, in a suitable category of pairs of adjoint functors. They were discovered independently in 1965. If you want the details, I highly recommend the Catsters videos.

Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top