Thu 22 May 2008

## Kan Extensions II: Adjunctions, Composition, Lifting

Posted by Edward Kmett under Category Theory , Comonads , Haskell , Kan Extensions , Monads[32] Comments

I want to spend some more time talking about Kan extensions, composition of Kan extensions, and the relationship between a monad and the monad generated by a monad.

But first, I want to take a moment to recall adjunctions and show how they relate to some standard (co)monads, before tying them back to Kan extensions.

**Adjunctions 101**

An adjunction between categories and consists of a pair of functors , and and a natural isomorphism:

We call the left adjoint functor, and the right adjoint functor and an adjoint pair, and write this relationship as

Borrowing a Haskell definition from Dave Menendez, an adjunction from the category of Haskell types (**Hask**) to **Hask** given by a pair of Haskell `Functor`

instances can be defined as follows, where phi is witnessed by = `leftAdjunct`

and = `rightAdjunct`

. [haddock]

class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where unit :: a -> g (f a) counit :: f (g a) -> a leftAdjunct :: (f a -> b) -> a -> g b rightAdjunct :: (a -> g b) -> f a -> b unit = leftAdjunct id counit = rightAdjunct id leftAdjunct f = fmap f . unit rightAdjunct f = counit . fmap f

**Currying and Uncurrying**

The most well known adjunction to a Haskell programmer is between the functors given by `((,)e)`

and `((->)e)`

. (Recall that you can read `((,)e)`

as `(e,)`

and `((->)e)`

as `(e->)`

; however, the latter syntax isn't valid Haskell as you aren't allowed to make `(,)`

and `(->)`

sections. We use this adjunction most every day in the form of the functions `curry`

and `uncurry`

.

curry :: ((a, b) -> c) -> a -> b -> c curry f x y = f (x,y) uncurry :: (a -> b -> c) -> (a, b) -> c uncurry f ~(x,y) = f x y

However the arguments are unfortunately slightly flipped around when we go to define this as an adjunction.

instance Adjunction ((,)e) ((->)e) where leftAdjunct f a e = f (e,a) rightAdjunct f ~(e,a) = f a e

This adjunction defines the relationship between the anonymous reader monad and the anonymous reader comonad (aka the product comonad).

**All Readers are the Same**

As an aside, if you look at the reader arrow, reader monad and reader comonad all side by side you can see that they are all basically the same thing. Kleisli arrows for the anonymous reader monad have the form `a -> e -> b`

. The Reader arrow takes the form `arr (a, e) b`

, which when `arr`

is `(->)`

this reads as `(a,e) -> b`

, which is just a curried Kleisli arrow for the Reader monad. On the other hand the reader comonad is `((,)e)`

, and its CoKleisli arrows have the form `(e,a) -> b`

. So, putting these side by side:

a -> e -> b (a , e) -> b (e , a) -> b

You can clearly see these are all the same thing!

**State and Composing Adjunctions**

Once we define functor composition:

newtype O f g a = Compose { decompose :: f (g a) } instance (Functor f, Functor g) => Functor (f `O` g) where fmap f = Compose . fmap (fmap f) . decompose

We can see that every adjunction gives rise to a monad:

instance Adjunction f g => Monad (g `O` f) where return = Compose . unit m >>= f = Compose . fmap (rightAdjunct (decompose . f)) $ decompose m

and if you happen to have a Comonad typeclass lying around, a comonad:

class Comonad w where extract :: w a -> a duplicate :: w a -> w (w a) extend :: (w a -> b) -> w a -> w b extend f = fmap f . duplicate duplicate = extend id instance Adjunction f g => Comonad (f `O` g) where extract = counit . decompose extend f = Compose . fmap (leftAdjunct (f . Compose)) . decompose

In reality, adjunction composition is of course not the only way you could form a monad by composition, so in practice a single composition constructor leads to ambiguity. Hence why in category-extras there is a base `CompF`

functor, and specialized variations for different desired instances. For simplicity, I'll stick to ``O``

here.

We can compose adjunctions, yielding an adjunction, so long as we are careful to place things in the right order:

instance (Adjunction f1 g1, Adjunction f2 g2) => Adjunction (f2 `O` f1) (g1 `O` g2) where counit = counit . fmap (counit . fmap decompose) . decompose unit = Compose . fmap (fmap Compose . unit) . unit

In fact, if we use the adjunction defined above, we can see that its just the `State`

monad!

instance MonadState e ((->)e `O` (,)e) where get = compose $ \s -> (s,s) put s = compose $ const (s,())

Not that I'd be prone to consider using that representation, but we can also see that we get the context comonad this way:

class Comonad w => ComonadContext s w | w -> s where getC :: w a -> s modifyC :: (s -> s) -> w a -> a instance ComonadContext e ((,)e `O` (->)e) where getC = fst . decompose modifyC f = uncurry (flip id . f) . decompose

**Adjunctions as Kan Extensions**

Unsurprisingly, since pretty much all of category theory comes around to being an observation about Kan extensions in the end, we can find some laws relating left- and right- Kan extensions to adjunctions.

Recall the definitions for right and left Kan extensions over **Hask**:

newtype Ran g h a = Ran { runRan :: forall b. (a -> g b) -> h b } data Lan g h a = forall b. Lan (g b -> a) (h b)

Formally, if and only if the right Kan extension exists and is preserved by . (Saunders Mac Lane, Categories for the Working Mathematician p248). We can use this in Haskell to define a natural isomorphism between `f`

and `Ran g Identity`

witnessed by `adjointToRan`

and `ranToAdjoint`

below:

adjointToRan :: Adjunction f g => f a -> Ran g Identity a adjointToRan f = Ran (\a -> Identity $ rightAdjunct a f) ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a ranToAdjoint r = runIdentity (runRan r unit)

We can construct a similar natural isomorphism for the right adjoint `g`

of a `Functor`

`f`

and `Lan f Identity`

:

adjointToLan :: Adjunction f g => g a -> Lan f Identity a adjointToLan = Lan counit . Identity lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a lanToAdjoint (Lan f v) = leftAdjunct f (runIdentity v)

So, with that in hand we can see that `Ran f Identity -| f -| Lan f Identity`

, presuming `Ran f Identity`

and `Lan f Identity`

exist.

**A More General Connection**

Now, the first isomorphism above can be seen as a special case of a more general law relating functor composition and Kan extensions, where `h = Identity`

in the composition below:

ranToComposedAdjoint :: Adjunction f g => Ran g h a -> (h `O` f) a ranToComposedAdjoint r = Compose (runRan r unit) composedAdjointToRan :: (Functor h, Adjunction f g) => (h `O` f) a -> Ran g h a composedAdjointToRan f = Ran (\a -> fmap (rightAdjunct a) (decompose f))

Similarly , we get the more generalize relationship for `Lan`

:

lanToComposedAdjoint :: (Functor h, Adjunction f g) => Lan f h a -> (h `O` g) a lanToComposedAdjoint (Lan f v) = Compose (fmap (leftAdjunct f) v) composedAdjointToLan :: Adjunction f g => (h `O` g) a -> Lan f h a composedAdjointToLan = Lan counit . decompose

**Composing Kan Extensions**

Using the above with the laws for composing right Kan extensions:

composeRan :: Ran f (Ran g h) a -> Ran (f `O` g) h a composeRan r = Ran (\f -> runRan (runRan r (decompose . f)) id) decomposeRan :: Functor f => Ran (f `O` g) h a -> Ran f (Ran g h) a decomposeRan r = Ran (\f -> Ran (\g -> runRan r (Compose . fmap g . f)))

or the laws for composing left Kan extensions:

composeLan :: Functor f => Lan f (Lan g h) a -> Lan (f `O` g) h a composeLan (Lan f (Lan g h)) = Lan (f . fmap g . decompose) h decomposeLan :: Lan (f `O` g) h a -> Lan f (Lan g h) a decomposeLan (Lan f h) = Lan (f . compose) (Lan id h)

can give you a lot of ways to construct monads:

**Right Kan Extension as (almost) a Monad Transformer**

You can lift many of operations from a monad m to the codensity monad of `m`

. Unfortunately, we don't have quite the right type signature for an instance of `MonadTrans`

, so we'll have to make do with our own methods:

[Edit: this has been since factored out into Control.Monad.Codensity to allow `Codensity`

to actually be an instance of `MonadTrans`

]

liftRan :: Monad m => m a -> Ran m m a liftRan m = Ran (m >>=) lowerRan :: Monad m => Ran m m a -> m a lowerRan a = runRan a return instance MonadReader r m => MonadReader r (Ran m m) where ask = liftRan ask local f m = Ran (\c -> ask >>= \r -> local f (runRan m (local (const r) . c))) instance MonadIO m => MonadIO (Ran m m) where liftIO = liftRan . liftIO instance MonadState s m => MonadState s (Ran m m) where get = liftRan get put = liftRan . put

In fact the list of things you can lift is pretty much the same as what you can lift over the `ContT`

monad transformer due to the similarity in the types. However, just because you lifted the operation into the right or left Kan extension, doesn't mean that it has the same asymptotic performance.

Similarly we can lift many comonadic operations to the `Density`

comonad of a comonad using `Lan`

.

[Edit: Refactored out into Control.Comonad.Density]

**Changing Representation**

Given a `f -| g`

, `g `O` f`

is a monad, and `Ran (g `O` f) (g `O` f)`

is the monad generated by `(g `O` f)`

, described in the previous post. We showed above that this monad can do many of the same things that the original monad could do. From there you can `decomposeRan`

to get `Ran g (Ran f (g `O` f))`

, which you can show to be yet another monad, and you can continue on from there.

Each of these monads may have different operational characteristics and performance tradeoffs. For instance the codensity monad of a monad can offer better asymptotic performance in some usage scenarios.

Similarly the left Kan extension can be used to manipulate the representation of a comonad.

All of this code is encapsulated in category-extras [docs] [darcs] as of release 0.51.0

May 23rd, 2008 at 12:06 am

Update: The current version of category-extras on hackage should now build correctly on ghc 6.8.

May 26th, 2008 at 7:23 pm

[...] Grant B. asked me to post the derivation for the right and left Kan extension formula used in previous Kan Extension posts (1,2). For that we can turn to the definition of Kan extensions in terms of ends, but first we need to take a couple of steps back to find a way to represent (co)ends in Haskell. [...]

June 5th, 2008 at 11:49 am

[...] I’ve had a few people ask me questions about Adjunctions since my recent post and a request for some more introductory material, so I figured I would take a couple of short posts to tie Adjunctions to some other concepts. [...]

June 24th, 2011 at 1:22 am

[...] arise in a subsequent post) on this blog previously, in a series of posts on Kan Extensions. [ 1, 2, [...]

June 30th, 2011 at 10:55 pm

[...] The latter few steps require identities established in my second post on Kan extensions. [...]

November 22nd, 2012 at 1:43 am

[...] , where is enriched in . Provided the above end exists, is a monad regardless of whether has an adjoint, which is the usual way one thinks of functors (in general) giving rise to [...]

May 3rd, 2022 at 7:12 am

cialis without a doctor’s prescription https://online-pharmacies0.yolasite.com/...You definitely made your point….

May 4th, 2022 at 8:50 am

cialis https://deiun.flazio.com/...Beneficial posts. Cheers!…

May 4th, 2022 at 5:24 pm

online canadian pharmacy https://kertyun.flazio.com/...Good info. Regards….

May 5th, 2022 at 12:47 pm

cialis generico https://kerbnt.flazio.com/...This is nicely put. !…

May 5th, 2022 at 6:54 pm

medication without a doctors prescription http://nanos.jp/jmp?url=http://cialisonlinei.com/...Great forum posts. Thanks….

May 6th, 2022 at 10:54 am

online prescriptions without a doctor https://womed7.wixsite.com/pharmacy-online/post/new-ideas-into-canada-pharmacies-never-before-revealed...Nicely put, Thank you!…

May 7th, 2022 at 9:24 am

cialis 20 mg https://kerntyast.flazio.com/...You stated this superbly….

May 7th, 2022 at 4:51 pm

canada pharmacy online https://sekyuna.gonevis.com/three-step-guidelines-for-online-pharmacies/...Thanks! Loads of posts!

…

May 8th, 2022 at 7:29 am

cialis 5mg prix https://gewrt.usluga.me/...Really tons of valuable tips….

May 9th, 2022 at 11:00 am

buy cialis online https://pharmacy-online.webflow.io/...You’ve made your position quite well.!…

May 9th, 2022 at 5:27 pm

tadalafil 20 mg https://canadian-pharmacy.webflow.io/...Regards. An abundance of posts!

…

May 10th, 2022 at 3:35 am

prescriptions from canada without https://site273035107.fo.team/...Regards! Plenty of forum posts!

…

May 10th, 2022 at 11:56 am

canada pharmacy https://site656670376.fo.team/...Useful posts. Kudos!…

May 10th, 2022 at 10:08 pm

cialis tablets australia https://site561571227.fo.team/...Many thanks. A good amount of info!

…

May 11th, 2022 at 4:16 am

most reliable canadian pharmacies https://site102906154.fo.team/...Kudos, Numerous postings.

…

May 11th, 2022 at 10:13 am

cialis 5 mg https://hekluy.ucraft.site/...Truly all kinds of fantastic facts….

May 11th, 2022 at 8:44 pm

cialis 20mg prix en pharmacie https://kawsear.fwscheckout.com/...Nicely put, Cheers….

May 13th, 2022 at 11:09 am

online prescriptions without a doctor https://hertnsd.nethouse.ru/...You expressed that exceptionally well….

May 14th, 2022 at 11:06 am

tadalafil https://uertbx.livejournal.com/402.html...Terrific information. Thank you!…

May 14th, 2022 at 5:22 pm

buy viagra now https://lwerts.livejournal.com/276.html...Cheers! Excellent information!…

May 15th, 2022 at 9:26 am

tadalafil tablets https://avuiom.sellfy.store/...Amazing postings. Regards….

May 16th, 2022 at 10:53 am

tadalafil tablets https://kwersd.mystrikingly.com/...With thanks. Plenty of facts.

…

May 16th, 2022 at 4:53 pm

cialis 20mg https://gewsd.estranky.sk/clanky/drugstore-online.html...Perfectly expressed genuinely! !…

May 17th, 2022 at 1:15 pm

cialis generico online http://site592154748.fo.team/...Seriously lots of beneficial information….

May 18th, 2022 at 6:26 am

tadalafil 20 mg https://lasert.gonevis.com/recommended-canadian-pharmacies-2/...Helpful data. Thanks a lot….

May 18th, 2022 at 2:37 pm

cialis purchase online without prescription http://aonubs.website2.me/...Truly loads of great material!…