Tue 20 May 2008
Kan Extensions
Posted by Edward Kmett under Category Theory , Comonads , Haskell , Kan Extensions , Mathematics , Monads[85] Comments
I think I may spend a post or two talking about Kan extensions.
They appear to be black magic to Haskell programmers, but as Saunders Mac Lane said in Categories for the Working Mathematician:
All concepts are Kan extensions.
So what is a Kan extension? They come in two forms: right- and left- Kan extensions.
First I'll talk about right Kan extensions, since Haskell programmers have a better intuition for them.
Introducing Right Kan Extension
If we observe the type for a right Kan extension over the category of Haskell types:
newtype Ran g h a = Ran { runRan :: forall b. (a -> g b) -> h b }
This is defined in category-extras under Control.Functor.KanExtension along with a lot of the traditional machinery for working with them.
We say that Ran g h
is the right Kan extension of h
along g
. and mathematicians denote it . It has a pretty diagram associated with it, but thats as deep as I'll let the category theory go.
This looks an awful lot like the type of a continuation monad transformer:
newtype ContT r m a = ContT { runContT :: (a -> m r) -> m r }
The main difference is that we have two functors involved and that the body of the Kan extension is universally quantified over the value it contains, so the function it carries can't just hand you back an m r
it has lying around unless the functor it has closed over doesn't depend at all on the type r
.
Interestingly we can define an instance of Functor
for a right Kan extension without even knowing that g
or h
are functors! Anything of kind * -> * will do.
instance Functor (Ran g h) where fmap f m = Ran (\\k -> runRan m (k . f))
The monad generated by a functor
We can take the right Kan extension of a functor f
along itself (this works for any functor in Haskell) and get what is known as the monad generated by f
or the codensity monad of f
:
instance Monad (Ran f f) where return x = Ran (\\k -> k x) m >>= k = Ran (\\c -> runRan m (\\a -> runRan (k a) c))
This monad is mentioned in passing in Opmonoidal Monads by Paddy McCrudden and dates back further to Ross Street's "The formal theory of monads" from 1972. The term codensity seems to date back at least to Dubuc's thesis in 1974.
Again, this monad doesn't care one whit about the fact that f
is a Functor in the Haskell sense.
This monad provides a useful opportunity for optimization. For instance Janis Voigtländer noted in Asymptotic improvement of functions over Free Monads that a particular monad could be used to improve performance -- Free monads as you'll recall are the tool used in Wouter Sweirstra's Data Types á la Carte, and provide an approach for, among other things, decomposing the IO
monad into something more modular, so this is by no means a purely academic exercise!
Voigtländer's monad,
newtype C m a = C (forall b. (a -> m b) -> m b)
turns out to be just the right Kan extension of another monad along itself, and can equivalently be thought of as a ContT
that has been universally quantified over its result type.
The improvement results from the fact that the continuation passing style transformation it applies keeps you from traversing back and forth over the entire tree when performing substitution in the free monad.
The Yoneda Lemma
Heretofore we've only used right Kan extensions where we have extended a functor along itself. Lets change that:
Dan Piponi posted a bit about the Yoneda lemma a couple of years back, which ended with the observation that the Yoneda lemma says that check and uncheck are inverses:
> check :: Functor f => f a -> (forall b . (a -> b) -> f b) > check a f = fmap f a > uncheck :: (forall b . (a -> b) -> f b) -> f a > uncheck t = t id
We can see that this definition for a right Kan extension just boxes up that universal quantifier in a newtype
and that we could instantiate:
> type Yoneda = Ran Identity
and we can define check
and uncheck
as:
check' :: Functor f => f a -> Yoneda f a check' a = Ran (\\f -> fmap (runIdentity . f) a) uncheck' :: Yoneda f a -> f a uncheck' t = runRan t Identity
Limits
We can go on and define categorical limits in terms of right Kan extensions using the Trivial
functor that maps everything to a category with a single value and function. In Haskell, this is best expressed by:
data Trivial a = Trivial instance Functor Trivial where fmap f _ = Trivial trivialize :: a -> Trivial b trivialize _ = Trivial type Lim = Ran Trivial
Now, in Haskell, this gives us a clear operational understanding of categorical limits.
Lim f a ~ forall b. (a -> Trivial b) -> f b
This says that we can't use any information of the value a
we supply, or given by the function (a -> Trivial b)
when constructing f b
, but we have to be able to define an f b
for any type b
requested. However, we have no way to get any b
to plug into the functor! So the only (non-cheating) member of Lim Maybe a
is Nothing
, of Lim [] a
is []
, etc.
Left Kan extensions
Left Kan extensions are a bit more obscure to a Haskell programmer, because where right Kan extensions relate to the well-known ContT
monad transformer, the left Kan extension is related to a less well known comonad transformer.
First, the a Haskell type for the Left Kan extension of h
along g
:
data Lan g h a = forall b. Lan (g b -> a) (h b)
This is related to the admittedly somewhat obscure state-in-context comonad transformer, which I constructed for category-extras.
newtype ContextT s w a = ContextT { runContextT :: (w s -> a, w s) }
However, the left Kan extension provides no information about the type b
contained inside of its h
functor and g
and h
are not necessarily the same functor.
As before we get that Lan g h
is a Functor regardless of what g
and h
are, because we only have to map over the right hand side of the contained function:
instance Functor (Lan f g) where fmap f (Lan g h) = Lan (f . g) h
The comonad generated by a functor
We can also see that the left Kan extension of any functor f
along itself is a comonad, even if f is not a Haskell Functor
. This is of course known as the comonad generated by f
, or the density comonad of f
.
instance Comonad (Lan f f) where extract (Lan f a) = f a duplicate (Lan f ws) = Lan (Lan f) ws
Colimits
Finally we can derive colimits, by:
type Colim = Lan Trivial
then Colim f a ~ exists b. (Trivial b -> a, f b)
, and we can see that operationally, we have an f
of some unknown type b
and for all intents and purposes a value of type a
since we can generate a Trivial b from thin air, so while limits allow only structures without values, colimits allow arbitrary structures, but keep you from inspecting the values in them by existential quantification. So for instance you could apply a length function to a Colim [] a
, but not add up its values.
You can also build up a covariant analog of the traditional Yoneda lemma using Lan Identity
, but I leave that as an exercise for the reader.
I've barely scratched the surface of what you can do with Kan extensions, but I just wanted to shine a little light on this dark corner of category theory.
For more information feel free to explore category-extras. For instance, both right and left Kan extensions along a functor are higher-order functors, and hence so are Yoneda, Lim, and Colim as defined above.
Thats all I have time for now.
Code for right and left Kan extensions, limits, colimits and the Yoneda lemma are all available from category-extras on hackage.
[Edit: the code has since been refactored to treat Yoneda, CoYoneda, Density and Codensity as separate newtypes to allow for instance both Yoneda and Codensity to be different monads]
May 22nd, 2008 at 5:01 pm
Neat!
One question: can you explain how you converted the definition of the Kan extension and its universal property into the Haskell datatype above?
It should be unambiguous, correct? I’m confused as to why Johann and Ghani’s GADT paper in POPL 2008 here gives a different encoding of the left Kan extension.
Any help would be appreciated.
May 22nd, 2008 at 7:13 pm
[...] 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. [...]
May 23rd, 2008 at 12:33 am
The left Kan extension used in that paper is taken along a functor with domain |Hask| rather than Hask. Where |C| maps a category to its underlying discrete category, discarding all non-identity arrows. Their Lan only needs to support this discrete category, because that is all that is necessary to faithfully model GADTs.
They don’t need it since their only arrows are the identities. Since they only need concern themselves with identities, an equality GADT serves them in better stead.
This is also why their definition of an HFunctor drops ffmap. It eases their derivation. For instance in http://comonad.com/haskell/category-extras/src/Control/Functor/HigherOrder/Composition.hs
I have to deal with a lot of newtype noise to implement ffmap, since they don’t need it at all, they don’t have to cram that into the paper.
If you look at Johann and Ghani’s earlier paper “Initial Semantics is Enough!” at http://crab.rutgers.edu/~pjohann/tlca07-rev.pdf you’ll find the exact definition above (modulo the choice of newtyping a tuple vs. using a data type.
As for the derivations I was planning to do a post on that at some point, but the short answer is they are based on the definition of Kan extensions as (co)ends, which can be found readily in the Wikipedia article on Kan extensions or more formally in Categories for the Working Mathematician.
May 26th, 2008 at 7:22 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 23rd, 2011 at 11:00 pm
[...] will arise in a subsequent post) on this blog previously, in a series of posts on Kan Extensions. [ 1, 2, [...]
June 23rd, 2011 at 11:53 pm
[...] covered it briefly in my initial article on Kan extensions, but the inestimable Dan Piponi wrote a much nicer article on how it implies in Haskell that given [...]
June 27th, 2012 at 1:50 pm
Can you make the constraint Kan extension? Such as (forall b. Monoid b => (a -> g b) -> h b) and so on. Or use the constraint kind to allow it a parameter.
February 19th, 2014 at 5:58 pm
[...] understood. So there’s the Haskell-as-semi-formal-notation approach in Kmett’s posts (starting here) that give lots of examples, but for me to understand something I really need to see it in more [...]
May 4th, 2014 at 6:14 pm
Great article! Thanks!
Typographical remark: Several of your lambdas have extra backslashes at the start.
May 3rd, 2022 at 4:12 am
Squidproxies…
I found a great……
May 3rd, 2022 at 7:11 am
tadalafil generic https://online-pharmacies0.yolasite.com/...
Nicely put, Kudos….
May 3rd, 2022 at 2:27 pm
canadian pharmacies https://6270e49a4db60.site123.me/blog/the-untold-secret-to-mastering-aspirin-in-just-7-days-1...
Cheers! Useful information….
May 4th, 2022 at 8:50 am
tadalafil 5mg https://deiun.flazio.com/...
Kudos, I like it….
May 4th, 2022 at 5:23 pm
tadalafil without a doctor’s prescription https://kertyun.flazio.com/...
Nicely put. Appreciate it!…
May 5th, 2022 at 6:51 am
online cialis https://kerntyas.gonevis.com/the-mafia-guide-to-online-pharmacies/...
You actually mentioned it effectively!…
May 5th, 2022 at 12:47 pm
cialis purchase online without prescription https://kerbnt.flazio.com/...
Nicely put, Thanks a lot!…
May 5th, 2022 at 6:53 pm
canadian discount pharmacies http://nanos.jp/jmp?url=http://cialisonlinei.com/...
Awesome content. Cheers!…
May 6th, 2022 at 5:28 am
tadalafil 20mg http://ime.nu/cialisonlinei.com...
Useful material. Thanks a lot….
May 6th, 2022 at 6:44 am
Web Hostings Discounts…
I found a great……
May 6th, 2022 at 10:53 am
cialis online https://womed7.wixsite.com/pharmacy-online/post/new-ideas-into-canada-pharmacies-never-before-revealed...
Beneficial material. Regards!…
May 7th, 2022 at 9:23 am
canadian pharmacies shipping to usa https://kerntyast.flazio.com/...
Regards! Loads of stuff.
…
May 7th, 2022 at 4:51 pm
drugstore online https://sekyuna.gonevis.com/three-step-guidelines-for-online-pharmacies/...
This is nicely put! ….
May 8th, 2022 at 7:29 am
buy cialis without a doctor’s prescription https://gewrt.usluga.me/...
Thanks, I appreciate it!…
May 8th, 2022 at 1:48 pm
Free Hostings Coupons…
I found a great……
May 9th, 2022 at 11:00 am
cialis uk https://pharmacy-online.webflow.io/...
Many thanks. Numerous facts.
…
May 9th, 2022 at 5:26 pm
tadalafil tablets https://canadian-pharmacy.webflow.io/...
Kudos, A good amount of postings!
…
May 10th, 2022 at 3:34 am
cialis online https://site273035107.fo.team/...
Very good information. Many thanks….
May 10th, 2022 at 5:42 am
Hostings Coupons Deals…
I found a great……
May 10th, 2022 at 7:03 am
Hostings Coupons Sales…
I found a great……
May 10th, 2022 at 11:56 am
cialis 5mg https://site656670376.fo.team/...
Wonderful facts, Thanks!…
May 10th, 2022 at 10:08 pm
pharmacy canada https://site561571227.fo.team/...
Awesome material. Cheers….
May 11th, 2022 at 4:15 am
canada pharmacies online prescriptions https://site102906154.fo.team/...
Thanks, Valuable information….
May 11th, 2022 at 5:36 am
New Hostings Coupons…
I found a great……
May 11th, 2022 at 8:01 am
Hostings Coupons…
I found a great……
May 11th, 2022 at 10:12 am
cialis 20 mg best price https://hekluy.ucraft.site/...
Wonderful write ups, With thanks….
May 11th, 2022 at 8:43 pm
cialis without a doctor’s prescription https://kawsear.fwscheckout.com/...
Many thanks. Plenty of info!
…
May 13th, 2022 at 11:08 am
cialis 5mg prix https://hertnsd.nethouse.ru/...
You have made your position extremely effectively!!…
May 14th, 2022 at 11:05 am
canada online pharmacy https://uertbx.livejournal.com/402.html...
Useful tips. Appreciate it….
May 14th, 2022 at 5:22 pm
cialis lowest price https://lwerts.livejournal.com/276.html...
Useful material. Thanks!…
May 15th, 2022 at 9:26 am
tadalafil 10 mg https://avuiom.sellfy.store/...
Thanks a lot! I value it!…
May 15th, 2022 at 9:25 pm
cialis 5mg https://pharmacies.bigcartel.com/...
Thank you, A lot of tips!
…
May 16th, 2022 at 10:52 am
online canadian pharmacy https://kwersd.mystrikingly.com/...
Nicely put, Appreciate it!…
May 16th, 2022 at 4:52 pm
tadalafil 20mg https://gewsd.estranky.sk/clanky/drugstore-online.html...
Kudos. Helpful information!…
May 17th, 2022 at 1:15 pm
cialis pills http://site592154748.fo.team/...
Regards, Fantastic information….
May 18th, 2022 at 6:25 am
cialis canada https://lasert.gonevis.com/recommended-canadian-pharmacies-2/...
Cheers, An abundance of stuff!
…
May 18th, 2022 at 2:37 pm
canadian pharmacies that ship to us http://aonubs.website2.me/...
You actually said this very well!…
May 20th, 2022 at 11:08 am
canadian drugs https://dkyubn.bizwebs.com/...
Thanks! Fantastic information!…
May 21st, 2022 at 4:16 am
cialis 5 mg https://asebg.bigcartel.com/canadian-pharmacy...
Factor clearly regarded…..
May 22nd, 2022 at 7:32 am
cialis 20mg prix en pharmacie https://medicine-online.estranky.sk/clanky/understand-covid-19-and-know-the-tricks-to-avoid-it-from-spreading—–medical-services.html...
Cheers! Very good stuff!…
May 23rd, 2022 at 7:50 am
cialis 20 mg best price https://kertvbs.webgarden.com/...
Cheers, Terrific stuff….
May 25th, 2022 at 8:15 am
cialis from canada https://swenqw.company.site/...
Nicely put. Thanks a lot….
May 26th, 2022 at 10:26 am
cialis tablets australia https://kewburet.wordpress.com/2022/04/27/how-to-keep-your-workers-healthy-during-covid-19-health-regulations/...
Fantastic material. Regards….
May 26th, 2022 at 4:45 pm
canadian cialis https://kaswesa.nethouse.ru/...
You suggested it terrifically!…
May 27th, 2022 at 1:07 pm
tadalafil without a doctor’s prescription https://628f789e5ce03.site123.me/blog/what-everybody-else-does-when-it-comes-to-canadian-pharmacies...
With thanks, Very good stuff!…
June 1st, 2022 at 11:44 am
online cialis https://canadian-pharmaceutical.webflow.io/...
Regards! Ample posts.
…
June 1st, 2022 at 6:35 pm
buy cialis without a doctor’s prescription http://pamelaliggins.website2.me/...
Thanks! I enjoy this!…
June 4th, 2022 at 12:17 pm
canada drugs online https://hub.docker.com/r/gserv/pharmacies...
You revealed that perfectly….
June 5th, 2022 at 1:10 pm
cialis from canada https://hertb.mystrikingly.com/...
Thanks a lot! I appreciate it….
June 6th, 2022 at 4:59 am
The Comonad.Reader …
https://arabprizes.org/د-محمد-الربيع/…
June 6th, 2022 at 4:59 am
The Comonad.Reader …
https://cpstrojans.org/7th-grade-build-towers-in-science/…
June 6th, 2022 at 6:26 am
The Comonad.Reader …
https://www.tunisipweb.com/creation-graphique/…
June 6th, 2022 at 6:54 am
The Comonad.Reader …
https://www.halu.sk/kontakt/…
June 6th, 2022 at 8:15 am
most reliable canadian pharmacies https://kedmnx.estranky.sk/clanky/online-medicine-tablets-shopping-the-best-manner.html...
This is nicely put! !…
June 6th, 2022 at 4:57 pm
discount canadian pharmacies https://selera.mystrikingly.com/...
Fantastic material. With thanks….
June 7th, 2022 at 7:31 am
best canadian pharmacy https://ksorvb.estranky.sk/clanky/why-online-pharmacies-is-good-friend-to-small-business.html...
Nicely put, Cheers….
June 8th, 2022 at 7:46 am
best canadian mail order pharmacies https://gevcaf.estranky.cz/clanky/safe-canadian-online-pharmacies.html...
Incredible lots of useful tips!…
June 9th, 2022 at 5:55 am
buy generic cialis https://kwersv.proweb.cz/...
Seriously plenty of terrific info….
June 10th, 2022 at 7:38 am
perfect…
thank you for a very good article…
June 10th, 2022 at 8:38 am
cialis 5mg prix https://kwervb.estranky.cz/clanky/canadian-government-approved-pharmacies.html...
Regards! I appreciate this!…
June 13th, 2022 at 5:08 am
buy cialis without a doctor’s prescription https://kwsde.zombeek.cz/...
Wow a lot of valuable advice….
June 14th, 2022 at 11:18 am
cialis https://heklrs.wordpress.com/2022/06/14/canadian-government-approved-pharmacies/...
You actually stated that terrifically!…
June 15th, 2022 at 8:40 am
cialis from canada https://iercvsw.wordpress.com/2022/06/14/canadian-pharmacies-the-fitting-manner/...
Terrific info, Kudos!…
June 19th, 2022 at 1:56 am
1festivals…
…
June 19th, 2022 at 11:33 am
The Comonad.Reader …
https://www.crywolfmovie.com/a-few-words/…
June 21st, 2022 at 9:16 am
Cheap cialis https://site955305180.fo.team/...
Superb write ups. Regards!…
June 22nd, 2022 at 9:51 am
cialis canadian pharmacy http://site841934642.fo.team/...
You mentioned that perfectly!…
June 22nd, 2022 at 9:16 pm
canadadrugs https://62b2f636ecec4.site123.me/blog/canadian-pharmaceuticals-online...
Wonderful facts. Thank you!…
June 23rd, 2022 at 7:34 am
canadian pharmacy viagra https://62b2ffff12831.site123.me/blog/canadian-pharmaceuticals-for-usa-sales...
You actually revealed that superbly!…
June 27th, 2022 at 1:09 pm
canada drugs https://thefencefilm.co.uk/community/profile/hswlux/...
Really loads of helpful tips….
June 28th, 2022 at 10:28 am
cialis 20 mg best price https://anewearthmovement.org/community/profile/mefug/...
Regards. Awesome stuff….
June 28th, 2022 at 8:06 pm
cialis 20mg http://sandbox.autoatlantic.com/community/profile/kawxvb/...
You explained that effectively….
June 29th, 2022 at 10:36 am
cialis generic http://lwerfa.iwopop.com/...
Kudos. Very good information….
June 29th, 2022 at 4:09 pm
tadalafil 20 mg http://herbsd.iwopop.com/...
Thanks a lot! Wonderful information….
June 30th, 2022 at 3:00 pm
Nga Stancill…
I found a great……
July 3rd, 2022 at 11:04 am
canadian medications https://www.reddit.com/user/dotijezo/comments/9xlg6g/online_pharmacies/...
Thanks a lot. Numerous data.
…