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?
Having an adjoint tells you that the functor commutes with (either) limits or colimits. If a functor has a left adjoint, then it commutes with colimits, while if it has a right adjoint, it commutes with limits. For nice categories, one can sometimes conclude the converse.
The left adjoint or right adjoint to a functor (Def. 1.1), if it exists, is unique up to natural isomorphism.
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.)
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 backBut neither of these categories are subcategories of Hask.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With