Mon 26 May 2008

## Kan Extensions III: As Ends and Coends

Posted by Edward Kmett under Category Theory , Haskell , Kan Extensions , Mathematics[58] Comments

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.

**Dinatural Transformations**

Rather than repeat the definition here, we'll just note we can define a dinatural transformation in Haskell letting polymorphism represent the family of morphisms.

type Dinatural f g = forall a. f a a -> g a a

**Ends**

So what is an end?

An end is a universal dinatural transformation from some object e to some functor s.

Diving into the formal definition:

Given a functor , and end of is a pair where is an object of and omega is a dinatural transformation from e to S such that given any other dinatural transformation to S from another object x in , there exists a unique morphism , such that for every in .

We usually choose to write ends as , and abuse terminology calling the end of .

Note this uses a dinatural transformation from an object in , which we can choose to represent an arbitrary dinatural transformation from an object to a functor in terms of a dinatural transformation from the constant bifunctor:

newtype Const x a b = Const { runConst :: x }

This leaves us with the definition of a dinatural transformation from an object as:

Dinatural (Const x) s ~ forall a. Const x a a -> s a a

but the universal quantification over the `Const`

term is rather useless and the `Const`

bifunctor is supplying no information so we can just specialize that down to:

type DinaturalFromObject x s = x -> forall a. s a a

Now, clearly for any such transformation, we could rewrite it trivially using the definition:

type End s = forall a. s a a

with = id.

```
type DinaturalFromObject x s = x -> End s
```

And so `End`

above fully complies with the definition for an end, and we just say `e = End s`

abusing the terminology as earlier. The function = id is implicit.

For End to be a proper end, we assume that `s`

is contravariant in its first argument and covariant in its second argument.

**Example: Hom**

A good example of this is (->) in Haskell, which is as category theory types would call it the Hom functor for Hask. Then `End (->) = forall a. a -> a`

which has just one inhabitant `id`

if you discard cheating inhabitants involving fix or undefined.

We write or to denote `a -> b`

. Similarly we use to denote an exponential object within a category, and since in Haskell we have first class functions using the same syntax this also translates to `a -> b`

. We'll need these later.

**Example: Natural Transformations**

If we define:

newtype HomFG f g a b = HomFG { runHomFG :: f a -> g b }

then we *could* of course choose to define natural transformations in terms of `End`

as:

type Nat f g = End (HomFG f g) -- forall a. f a -> g a

**Right Kan Extension as an End**

Turning to Wikipedia or Categories for the Working Mathematician you can find the following definition for right Kan extension of along in terms of ends.

Working by rote, we note that is just `c -> K m`

as noted above, and that is then just `(c -> K m) -> T m'`

. So now we just have to take the end over that, and read off:

newtype RanT k t c m m' = (c -> k m) -> t m' type Ran k t c = End (RanT k t c)

Which, modulo newtype noise is the same as the type previously supplied type:

newtype Ran f g c = Ran { runRan :: forall m. (c -> f m) -> g m }

**Coends**

The derivation for the left Kan extension follows similarly from defining coends over **Hask** in terms of existential quantification and copowers as products.

The coend derivation is complicated slightly by Haskell's semantics. Disposing of the constant bifunctor as before we get:

type DinaturalToObject s c = forall a. (s a a -> c)

Which since we want to be able to box up the s a a term separately, we need to use existential quantification.

(forall a. s a a -> c) ~ (exists a. s a a) -> c

We cannot represent this directly in terms of a type annotation in Haskell, but we can do so with a data type:

data Coend f = forall a. Coend (f a a)

Recall that in Haskell, existential quantification is represented by using universal quantification outside of the type constructor.

The main difference is that in our coend the function is now `runCoend`

instead of `id`

, because we have a `Coend`

data constructor around the existential. Technicalities make it a little more complicated than that even, because you can't define a well-typed `runCoend`

and have to use pattern matching on the `Coend`

data constructor to avoid having an existentially quantified type escape the current scope, but the idea is the same.

**Left Kan Extension as a Coend**

Then given the definition for the left Kan extension of along as a coend:

we can read off:

data LanT k t c m m' = LanT (k m -> c) (t m') type Lan k t c = Coend (LanT k t c)

Which is *almost* isomorphic to the previously supplied type:

data Lan k t c = forall m. Lan (k m -> c) (t m)

except for the fact that we had to use two layers of data declarations when using the separate `Coend`

data type, so we introduced an extra place for a to hide.

A `newtype`

isn't allowed to use existential quantification in Haskell, so this form forces a spurious case analysis that we'd prefer to do without. This motivates why category-extras uses a separate definition for `Lan`

rather than the more elaborate definition in terms of `Coend`

.

[Edit: Fixed a typo in the definition of RanT]

May 27th, 2008 at 5:27 am

Awesome! This helped my understanding a lot, thanks.

May 27th, 2008 at 3:45 pm

Hey! Stop writing posts faster than I can read them :-)

June 13th, 2008 at 5:41 pm

I’m curious as to how you would motivate Kan extensions as a functional programming (specifically Haskell) tool. The right Kan extension almost looks like the CPS-transform of “a”, except with variant answer types. Shan’s thesis on page 73 shows how the ordinary function type is modified via the presence of delimited control into something like a right Kan extension.

Care to shed some light on this (and its dual)?

June 14th, 2008 at 8:16 am

Well, you can look at the Codensity monad (Ran m m) of a monad m as a weaker form of ContT which isn’t allowed to use the type of the ultimate return value to ‘pull any tricks’. Consequently, it has fewer inhabitants than ContT and we can say more about them. My favorite example so far is in:

http://wwwtcs.inf.tu-dresden.de/~voigt/mpc08.pdf

That paper shows that you can substitute a reference to the Codensity monad of a free monad in many places where you’d use the original free monad and change the asymptotic performance of the resulting algorithm because the continuation ‘linearizes’ the cost of repeatedly traversing the tree by piling the cost up in the continuation so you only traverse once.

I’d conjecture that the left Kan extension of a cofree comonad should let us pile up the cost of mapping or extending cofree comonads similarly. Though here I have yet to actually generate any performance results here due to other distractions.

We _can_ however definitely do the same thing with the Yoneda and Coyoneda lemmas. The resulting (co)monads fit very closely to the operational characteristics of the base monad.

If you transform a monad with Yoneda you get a monad that has the same overall costs for return and >>=, but where if your monad had a non constant cost for map (such as in the free monad of anything other than the trivial functor that maps everything to _|_), you can fuse the costs of all of your maps together by accumulating them and applying them all at once during the next (>>=) (or when you extract f from the Yoneda f).

Similarly CoYoneda accumulates maps for comonads, which is a win if map is expensive (such as in the cofree comonad case).

You can get a feel for why this works by looking at:

http://comonad.com/haskell/category-extras/src/Control/Functor/Yoneda.hs

and noting what fmap does and how >>= works for Yoneda. and how fmap and extend work for CoYoneda.

In category-extras I have generalized all of the constructive algorithmic morphisms that use the free monad or cofree comonad (histomorphisms, futumorphisms, dynamorphisms, chronomorphisms) to support the codensity monad of the free monad, density comonad of the cofree comonad, Yoneda of the free monad, Coyoneda of the cofree comonad, etc by defining a couple of extra typeclasses that express their ‘Free-Like’ behavior in the spirit of the above linked paper by Voigtlaender in

http://comonad.com/haskell/category-extras/src/Control/Monad/Free.hs

The generalization can be seen in use here:

http://comonad.com/haskell/category-extras/src/Control/Morphism/Futu.hs

and the instances for Codensity here:

http://comonad.com/haskell/category-extras/src/Control/Monad/Codensity.hs

February 25th, 2009 at 7:45 pm

Now that I’ve been thinking about these things I can point out a tiny tiny typo:

data LanT k t c m m’ = LanT (k m -> c) (t m)

should probably be

data LanT k t c m m’ = LanT (k m -> c) (t m’)

though it makes no difference in the definition of Lan.

On a less trivial level, I still don’t know what theorem I could quote to justify that, say,

type DinaturalFromObject x s = x -> forall a. s a a

defines dinaturals from a constant functor. For a specific choice of s dinaturality is a free theorem. But how do you uniformly prove this for all s, implemented in Haskell, with the right c/contravariance in the arguments?

February 25th, 2009 at 9:02 pm

Hey Dan,

Fixed the LanT definition. (Woops!)

Re the dinatural transformation piece, I’m not as deep as I used to be in this area, so I’ll go back and see what I can dig up from whatever notes I still have from when I wrote this. I recall it seeming quite obvious at the time, but now I can only barely remember what dinaturality is. :) I’d be quite surprised (and pleased) if you came up with a counterexample, however. ;)

February 26th, 2009 at 12:29 am

All of the various types of naturality (including dinaturality and extranaturality) seem to arise as free theorems but I’ve not seen a paper spelling this out clearly – at least not in a form I’d recognise. I can’t tell if it’s because nobody has figured it the details, or if the papers are just over my head.

October 17th, 2009 at 11:15 pm

Just a minor typo note:

> newtype RanT f g c m m’ = (c -> K m) -> T m’

Should be:

> newtype RanT k t c m m’ = (c -> k m) -> t m’

right?

October 18th, 2009 at 4:35 pm

Wren: Fixed!

September 9th, 2010 at 1:44 am

Have you ever considered about contributing on additional web sites? You have some great content right here and I’m certain you can share a lot far more when you wrote some content throughout other web sites. You will discover a great deal of associated web-sites to check out. Only one thing to look at. I’m glad I know about it at least.

September 10th, 2010 at 12:28 pm

I have written bits and pieces here and there over the years — I used to write a lot of magazine articles in particular, and I think there is an old column by me still floating around on flipcode.

These days I have a lot less time for writing, however. What makes it to this blog are mostly just the things that I found interesting enough to share. To get the message out I largely rely on syndication through planet haskell and reddit, both of which makes the location of the source content less of an issue these days than it used to be. Those have more overlap with would-be readership for this sort of content than almost any mainstream web site I can know of.

June 24th, 2011 at 3:43 am

[...] I have spoken about this type (and another that will arise in a subsequent post) on this blog previously, in a series of posts on Kan Extensions. [ 1, 2, 3] [...]

July 7th, 2011 at 6:44 pm

Isn’t the type (exists a. f a a) the coproduct rather than the coend? The coend is the coproduct modulo the relation imposed by the commuting square (degenerate hexagon) in the definition of a dinatural transformation.

September 22nd, 2012 at 10:43 pm

[...] the integral notation denotes an end, and the square brackets denote a power, which allows us to take what is essentially an exponential [...]

September 11th, 2014 at 7:10 pm

Dallas Roof Repair…The Comonad.Reader » Kan Extensions III: As Ends and Coends…

September 23rd, 2022 at 3:33 am

Viagra bula https://500px.com/p/skulogovid/?view=groups...You expressed this terrifically!…

September 23rd, 2022 at 7:39 am

Canadian viagra https://500px.com/p/bersavahi/?view=groups...You actually revealed it adequately!…

September 24th, 2022 at 4:22 am

canadian pharmacys https://www.provenexpert.com/canadian-pharmaceuticals-online-usa/...Kudos! Useful stuff….

September 24th, 2022 at 9:29 am

canada pharmacies online https://sanangelolive.com/members/pharmaceuticals...Many thanks, Loads of info!

…

September 26th, 2022 at 8:23 am

prescription drugs without prior prescription https://melaninterest.com/user/canadian-pharmaceuticals-online/?view=likes...Truly a good deal of beneficial information….

September 26th, 2022 at 12:26 pm

drugstore online https://haikudeck.com/canadian-pharmaceuticals-online-personal-presentation-827506e003...Thank you! I appreciate it….

September 26th, 2022 at 4:36 pm

Viagra 20 mg best price https://buyersguide.americanbar.org/profile/420642/0...Excellent knowledge. Thank you….

September 27th, 2022 at 12:18 am

canadian pharmaceuticals online https://experiment.com/users/canadianpharmacy...Regards! A good amount of advice.

…

September 27th, 2022 at 9:53 am

Viagra for sale https://challonge.com/esapenti...Kudos. Quite a lot of tips!

…

September 27th, 2022 at 2:21 pm

Viagra daily https://challonge.com/gotsembpertvil...Wonderful information. Thank you….

September 28th, 2022 at 4:08 am

Canadian viagra https://challonge.com/citlitigolf...You said it nicely.!…

September 28th, 2022 at 7:42 am

Online viagra https://order-stromectol-over-the-counter.estranky.cz/clanky/order-stromectol-over-the-counter.html...Seriously a good deal of good data!…

September 28th, 2022 at 2:09 pm

Viagra dosage https://soncheebarxu.estranky.cz/clanky/stromectol-for-head-lice.html...Thanks. Lots of stuff!

…

September 29th, 2022 at 3:41 am

stromectol dosage table https://lehyriwor.estranky.sk/clanky/stromectol-cream.html...Great material, Cheers….

September 29th, 2022 at 7:28 am

Buy viagra https://dsdgbvda.zombeek.cz/...Seriously tons of excellent material!…

September 29th, 2022 at 1:54 pm

Viagra 5 mg https://inflavnena.zombeek.cz/...This is nicely said. ….

September 30th, 2022 at 8:11 am

Viagra 20mg https://www.myscrsdirectory.com/profile/421708/0...You actually suggested that fantastically….

September 30th, 2022 at 3:20 pm

Tadalafil tablets https://supplier.ihrsa.org/profile/421717/0...Factor certainly applied…..

October 1st, 2022 at 5:43 am

Viagra generico online https://wefbuyersguide.wef.org/profile/421914/0...You have made your stand very well.!…

October 1st, 2022 at 9:43 am

Viagra generico online https://legalmarketplace.alanet.org/profile/421920/0...Regards! I enjoy this!…

October 2nd, 2022 at 3:20 am

Viagra or viagra https://moaamein.nacda.com/profile/422018/0...Very good forum posts. Cheers!…

October 2nd, 2022 at 7:47 am

Viagra daily https://www.audiologysolutionsnetwork.org/profile/422019/0...Valuable advice. Thank you….

October 2nd, 2022 at 11:05 am

Viagra manufacturer coupon https://network.myscrs.org/profile/422020/0...With thanks. Valuable stuff….

October 3rd, 2022 at 4:50 am

Viagra purchasing https://sanangelolive.com/members/canadianpharmaceuticalsonlineusa...Factor effectively applied!!…

October 3rd, 2022 at 8:14 am

Viagra vs viagra https://sanangelolive.com/members/girsagerea...Excellent stuff. Thanks a lot!…

October 4th, 2022 at 6:55 am

Viagra bula https://www.ecosia.org/search?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…Incredible a lot of helpful advice!…

October 4th, 2022 at 10:39 am

Viagra or viagra https://www.mojomarketplace.com/user/Canadianpharmaceuticalsonline-EkugcJDMYH...Seriously loads of beneficial information!…

October 4th, 2022 at 3:04 pm

canadian viagra https://seedandspark.com/user/canadian-pharmaceuticals-online...Lovely forum posts, Thanks!…

October 5th, 2022 at 2:57 am

Generic viagra https://www.giantbomb.com/profile/canadapharmacy/blog/canadian-pharmaceuticals-online/265652/...Tips certainly considered…..

October 5th, 2022 at 11:57 am

online canadian pharmacy https://feeds.feedburner.com/bing/Canadian-pharmaceuticals-online...Appreciate it, A good amount of advice.

…

October 5th, 2022 at 4:46 pm

canadian pharmacy world https://search.gmx.com/web/result?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…Many thanks. Fantastic stuff!…

October 6th, 2022 at 1:53 am

Viagra 20 mg https://search.seznam.cz/?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…Appreciate it! Ample content!

…

October 6th, 2022 at 5:34 am

stromectol posologie https://sanangelolive.com/members/unsafiri...You actually stated it adequately….

October 6th, 2022 at 3:48 pm

trust pharmacy canada https://swisscows.com/en/web?query=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…Excellent material. Thank you….

October 7th, 2022 at 10:12 am

Viagra 20mg …Thanks a lot, Terrific stuff….

October 8th, 2022 at 11:40 am

Viagra uk https://www.bakespace.com/members/profile/Сanadian pharmaceuticals for usa sales/1541108/…You made your point extremely clearly…..

October 9th, 2022 at 4:48 am

Viagra daily …Nicely put. Cheers….

October 9th, 2022 at 9:56 am

Viagra generika https://results.excite.com/serp?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…You’ve made your point quite effectively!!…

October 9th, 2022 at 2:25 pm

Tadalafil 5mg https://www.infospace.com/serp?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…You actually suggested that wonderfully….

October 11th, 2022 at 4:37 am

Tadalafil tablets https://results.excite.com/serp?q=“My Canadian Pharmacy – Extensive Assortment of Medications – 2022″…Terrific advice. Appreciate it!…

October 11th, 2022 at 9:59 am

Viagra dosage https://canadianpharmaceuticalsonline.as.me/schedule.php...Great facts. With thanks!…

October 13th, 2022 at 11:56 am

Viagra 5 mg funziona https://feeds.feedburner.com/bing/stromectolnoprescription...Nicely put, Regards!…

October 14th, 2022 at 4:27 am

Viagra or viagra https://reallygoodemails.com/orderstromectoloverthecounterusa...Awesome material. Cheers!…