Stream: Miscellaneous

Topic: Learning category theory as a programmer

vlj (Jun 09 2020 at 18:17):

Is there a good "entry point" to category theory from a software developer background ? I'm trying to learn category theory concept but it's a bit "abstract", I mean there are several good video on youtube, there is the maclane book but I miss a way to "exercise" it and have the result checked

Karl Palmskog (Jun 09 2020 at 18:18):

the best book for programmers to learn about category theory is in my opinion Algebra of Programming by Bird and de Moor

vlj (Jun 09 2020 at 18:19):

will have a look

vlj (Jun 09 2020 at 18:19):

thank for the suggestion

Karl Palmskog (Jun 09 2020 at 18:20):

they focus mostly on (1) the category of sets and total functions and (2) the category of sets and relations, but unless you're doing fancy stuff, these are in my opinion the core ones, where one can actually use category-theoretic results to get work done, e.g., fusion theorems

Karl Palmskog (Jun 09 2020 at 18:23):

Haskell's category of cpos and partial functions is from my view mostly a weird distraction

Karl Palmskog (Jun 09 2020 at 18:24):

Benjamin Pierce's Category theory for computer scientists is usually mentioned when this topic is raised, but I wasn't a big fan...

Reynald Affeldt (Jun 09 2020 at 18:43):

There is a bit of category theory applied to programming in https://github.com/affeldt-aist/monae.

Emilio Jesús Gallego Arias (Jun 09 2020 at 18:53):

Barr and Wells is IMHO very very good [and free] http://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf

vlj (Jun 09 2020 at 19:04):

Thanks will have a look

Kenji Maillard (Jun 09 2020 at 19:06):

@vlj maybe Seven sketches in compositionality
Not specific about computer science, but it looks like it is presenting quite nicely the important categorical ideas rather than emphasizing on the technicalities.

Notification Bot (Jun 10 2020 at 09:40):

This topic was moved here from #Coq users > Learning category theory as a programmer by Théo Zimmermann

Bas Spitters (Jun 10 2020 at 10:42):

We use Steve Awodey's book for the master students here at Aarhus university. It's quite accessible.

Alexander Gryzlov (Jun 10 2020 at 15:18):

There's also a very active category zulip server, where they have entire topics devoted to discussing better introductions for different backgrounds :)

Alexander Gryzlov (Jun 10 2020 at 15:19):

https://categorytheory.zulipchat.com/

vlj (Jun 24 2020 at 16:24):

@Alexander Gryzlov it looks like you need an invitation to join this zulip server (I just tried to join)

vlj (Jul 07 2020 at 21:24):

I have some trouble having the intuition on homset and the set categories. It looks like every categories can be "plunged" inset, there is even the forgetful functor for this. But for instance a monoid seen as a category is a single node and arrows for every element, but it looks like the nature of this node can be arbitrary. One can map the node to the set of all elements of the node to make it set like but it looks like artificially setting a set to something that's basically "nothing special". Same for the graph category, category theory talks about set of node, but itassumes that the node can be part of the set.

vlj (Jul 07 2020 at 21:28):

And about homsets, they are element of set if I understand correctly, but is it always safe to assume this ? I mean there are small categories and big categories to avoid self referential sets inconsistencies so I would expect that putting homset in set is only possible for some categories but not all possibles one.

jco (Jul 08 2020 at 01:28):

Homsets are of course sets, but there are categories for which the homset is not a set, but rather a category

Paolo Giarrusso (Jul 08 2020 at 02:47):

@vlj if you’re familiar with universes in Coq, and with how you have Type@{0} : Type@{1} : Type@{2} : ..., then IIUC you can think of “small” and “big” as “in Type@{0}“ and “in Type@{1}”.

Paolo Giarrusso (Jul 08 2020 at 02:48):

so for large categories, homsets are basically still sets, but instead of being in the Type@{0} universe, they’re in the next universe, Type@{1}.

Paolo Giarrusso (Jul 08 2020 at 02:51):

and you can consider even larger categories in Type@{2}, etc.

Paolo Giarrusso (Jul 08 2020 at 02:51):

(even tho Coq normally hides all that)

Paolo Giarrusso (Jul 08 2020 at 02:53):

(I am not being very precise here, and I haven’t studied a proper treatment of this stuff — “small” and “large” are usually talking about set theory, but you can also set up universes there, if you are willing to use the analogue of Coq’s universe hierarchy — that is,suitable inaccessible cardinals, or in particular Grothendieck universes)

jco (Jul 08 2020 at 05:38):

I am a mathematical dumb dumb, so the resources I've used to try and understand some category theory are for mathematical dumbs dumbs. They may be too basic for you, but I liked them

This book was pretty introductory, but goes into a lot of great detail that is quite lacking in a lot of the stuff on category theory intended for mathematicians. Very well written
https://www.amazon.com/Conceptual-Mathematics-First-Introduction-Categories/dp/052171916X

This is a bit more advanced than the previous, but I found it very well written and it helped me understand things that I didn't really grok from other sources
https://www.amazon.com/Category-Cambridge-Studies-Advanced-Mathematics/dp/1107044243

This book covers a ton of ground. It's good if your goal is to understand the language, and understand things like the Yoneda Lemma, but it won't go too much deeper...mainly it sort of just lays out what is going on in Category theory with some proofs, but definitely not the rigor of something like Awodey's book
https://github.com/hmemcpy/milewski-ctfp-pdf

I think the next step after all that would probably be Awodey's book. I picked it up once, decided that given my current mathematical sophisticated and level of need it was a bit too hard, then put it down. -_-

jco (Jul 08 2020 at 05:39):

I've also read Benjamin Pierce's book, and it is good, but it covers stuff subsumed by the above and I think they do it better (with all respect due to the brilliant Dr Pierce!)

Kenji Maillard (Jul 08 2020 at 08:05):

@vlj I think there is a small (but rather technical) mistunderstanding. Not all categories can be embedded into Set: there is of course a size issue but that can be "solved" up to some point by considering universes of various sizes, but more fundamentally there are categories that just don't embed into set because they are too different (as explained in this paper by Peter Freyd -- not necessarily an easy read). A category that can be embedded into Set is usually said to be concrete, and there are various theorems ensuring that categories built out of Set (such as categories of algebras for a theory or a monad) are concrete.

vlj (Jul 08 2020 at 17:50):

If a category is not concrete then homset are still in set ?

Kenji Maillard (Jul 08 2020 at 18:46):

yes with the standard definition of a category. Things get different once you start talking about enriched and/or higher categories.

Cyril Cohen (Jul 08 2020 at 21:23):

Kenji Maillard said:

yes with the standard definition of a category. Things get different once you start talking about enriched and/or higher categories.

Actually I believe that depends a lot on the reference definition you take. In some cases, these are rather called locally small categories.

Paolo Giarrusso (Jul 08 2020 at 21:28):

right, but if a category isn’t locally small, the homsets are still “collections”, just too large to be sets; in ZFC they are classes, but with a hierarchy of universes, homsets of larger categories are members of bigger universes.

Paolo Giarrusso (Jul 08 2020 at 21:29):

And I also recall, like @Cyril Cohen, that some texts assume all categories to be locally small.

vlj (Aug 31 2020 at 16:50):

Is there a good book/article presenting the Lawvere category for beginner ? It looks like a very important part of category theory but the barr well ebook doen't present it (it just mention Lawvere various papers)

Emilio Jesús Gallego Arias (Aug 31 2020 at 17:28):

@vlj this is not really tailored for programmers / CS but may help https://www.irif.fr/~mellies/mpri/mpri-ens/articles/hyland-power-lawvere-theories-and-monads.pdf

vlj (Sep 01 2020 at 17:14):

thanks

vlj (Sep 30 2020 at 18:33):

Is there a tool/Javascript lib that can be used to create small animations of arrows/points ? I find it easier to explain things in category theory with step by step drawing, and I wonder if there is a tool that allows to create animated diagram quickly

vlj (Oct 04 2020 at 18:16):

Is there a good pdf/book to introduce infinity catégories ?

Kenji Maillard (Oct 04 2020 at 19:29):

Higher Topos Theory by Jacob Lurie maybe ? For a quick glance at what the theory looks like these notes (in french) by Denis-Charles Cisinski might help. And for the model independent approach, there is this ongoing work by Emily Riehl and Dominic Verity.

vlj (Oct 05 2020 at 07:36):

thanks !

vlj (Oct 05 2020 at 07:37):

I don't know if it's relevant for programming, but I'd like to have at list a clue at what is generalised

vlj (Oct 11 2020 at 08:24):

I read that dépendent types can be viewed as fibration but I have troubles making the connections.

vlj (Oct 11 2020 at 08:26):

Afaik a fibration is a functor P from C to D which has cartesian arrows for f in D and point x in C with P(x) = dst(f).

vlj (Oct 11 2020 at 08:28):

If I have a dépendent type forall x:A, B(x) then I'm not sure if B should be viewed as C or D in the fibration definition.

vlj (Oct 11 2020 at 08:29):

Intuitively I would say that B is C since there are several objets that can be projected to a single x in C.

vlj (Oct 11 2020 at 08:31):

But I tend to see functor moving things "above" source category (maybe I have thé wrong picture here) and the traditionnal picture is that the dépendant types lie over the indexing type

Kenji Maillard (Oct 11 2020 at 09:06):

Hi @vlj, I think you can understand the claim "dependent types can be viewed as fibrations" along the following line: there exists models of dependent type theory where types $A$ are interpreted as objects with some structure $\mathcal{S}$ and type families $x : A \vdash B$ as $\mathcal{S}$-fibrations. I think one of the simplest example is to take $\mathcal{S}$ to be groupoids (see this seminal paper), but that also apply to simplicial sets, and at least some variants of cubical sets (of course in each case the precise definition of "fibration" vary).
So the short answer is that $A$ correspond to the base of the "fibration" $D$ and $B$ to the functor $P : C \Rightarrow D$.

Kenji Maillard (Oct 11 2020 at 09:12):

Now, you were trying to view $B$ as a Grothendieck fibration, interpreting types as categories. To my knowledge such an interpretation has never been put on paper formally. The closest thing are problably the ongoing work on directed type theory (for instance Thorsten Altenkrich's slides or Andreas Nuyts's master thesis).

vlj (Oct 11 2020 at 09:15):

Thanks for the references and explanation

vlj (Oct 11 2020 at 10:22):

By the way does the HoTT book assume such interpretation of type as categories ? At least in the chapter 2 they mention the word "fibration" to talk about dependant type iirc, but they assume no prior knowledge of category theory and redefine things like horizontal composition and whiskering without mentionning natural transformation, so actually they don't mention any category at all

vlj (Oct 11 2020 at 10:22):

is there a more general concept of fibration than the one found in category theory ?

Paolo Giarrusso (Oct 11 2020 at 10:34):

@Kenji Maillard If one of the simplest S is groupoids, what’s wrong with taking S to be the category of sets

Paolo Giarrusso (Oct 11 2020 at 10:36):

@vlj There is a _less general_ concept of fibration, which comes before the CT one:

Topologically, the transportation lemma can be viewed as a “path lifting” operation in a fibration.

Paolo Giarrusso (Oct 11 2020 at 10:36):

In classical homotopy theory, a fibration is defined as a map for which there exist liftings of paths; while in contrast, we have just shown that in type theory, every type family comes with a specified “path-lifting function”.

Paolo Giarrusso (Oct 11 2020 at 10:37):

Those sentences hint that the relevant field is “topology” or “homotopy theory”

Paolo Giarrusso (Oct 11 2020 at 10:39):

@vlj To me, the basic answer is that to view x : A |- B as a fibration, intuitively, you need to think of Sigma x : A. B and of its projections

Paolo Giarrusso (Oct 11 2020 at 10:40):

the first projection identifies the fiber, the second produces a point in that fiber

Kenji Maillard (Oct 11 2020 at 10:41):

vlj said:

is there a more general concept of fibration than the one found in category theory ?

One thing I forgot to mention is that the word fibration is employed a lot in algebraic topology as explained by @Paolo Giarrusso , and that abstracting/categorifying it lead in particular to the notion of model category where fibrations are part of the structure (they are a class of maps satisfying some lifting properties).

Kenji Maillard (Oct 11 2020 at 10:42):

Paolo Giarrusso said:

Kenji Maillard If one of the simplest S is groupoids, what’s wrong with taking S to be the category of sets

Nothing is wrong, but I find it weird to insist on the word "fibration" when it's just a plain map between sets without additional data or structure :)

Paolo Giarrusso (Oct 11 2020 at 10:44):

well, it’s useful to instantiate those generic frameworks for models onto Set, to get models in the category of sets.

Paolo Giarrusso (Oct 11 2020 at 10:46):

however, what model is most interesting/appropriate depends on the audience, and I can’t tell if @vlj is a mathematician or a computer scientist ^H^H^H what their goal is

Paolo Giarrusso (Oct 11 2020 at 10:47):

(IMHO, the model in sets is appropriate for most programmers — except that when you want to understand HoTT, there you indeed need _at least_ groupoids)

Paolo Giarrusso (Oct 11 2020 at 10:48):

but to be clear, I’m only a beginner in this material and Kenji understands much more than me; I only contributed to say a few more words on the basics ;-)

vlj (Oct 11 2020 at 10:52):

thanks for the precision

Last updated: Jun 01 2023 at 13:01 UTC