Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: learning: reading & references

Topic: Introduction to Monads


view this post on Zulip Pierre R (Jan 29 2025 at 19:54):

Hello,

For my research in Applied Category Theory for AI, I will need to understand Monads.

I am a newcomer and my background in CT is Leinster's Basic Category Theory. What would be a good book that introduces Monads?

Thank you

view this post on Zulip Joe Moeller (Jan 29 2025 at 20:54):

What is your mathematical background like? Books like Mac Lane's "Categories for the Working Mathematician" and Riehl's "Category Theory in Context" are aimed at people who know a bit of abstract algebra and topology. For that audience, they're great.

view this post on Zulip Paolo Perrone (Jan 29 2025 at 21:08):

What are you using monads for? Is it probability?

In my work I've often needed monads, mostly to model probability. In the past few years this led me to produce introductory material on monads with this motivation and background in mind. In particular:

I hope this helps!

view this post on Zulip Pierre R (Jan 30 2025 at 14:15):

Joe Moeller said:

What is your mathematical background like? Books like Mac Lane's "Categories for the Working Mathematician" and Riehl's "Category Theory in Context" are aimed at people who know a bit of abstract algebra and topology. For that audience, they're great.

Hello @Joe Moeller, I am a computer scientist. But I am in my second year of a Master's in Mathematics. I think that I have a good algebra background. My topology background is the one needed for analysis, mostly.

view this post on Zulip Pierre R (Jan 30 2025 at 14:36):

Hello @Paolo Perrone

Part of my thesis work is to understand and work through the details of Position: Categorical Deep Learning is an Algebraic Theory of All Architectures. There, the authors use Monads and Algebra of Monads to generalize Geometric Deep Learning.

Additionally, thank you very much for your suggestions. I will try to obtain your book through my university library.

Moreover, I am intrigued by your work. I will take a look at it.

Thank you.

view this post on Zulip Patrick Nicodemus (Jan 31 2025 at 15:37):

@Pierre R Monads can be understood from many different points of view, each of which I think gives a different view. Monads arise in homological algebra, universal algebra and the theory of programming languages, for different reasons.

view this post on Zulip Pierre R (Jan 31 2025 at 20:16):

Patrick Nicodemus said:

Pierre R Monads can be understood from many different points of view, each of which I think gives a different view. Monads arise in homological algebra, universal algebra and the theory of programming languages, for different reasons.

Thank you Patrick for the insight!

view this post on Zulip Qin Yuxuan (Feb 02 2025 at 09:47):

You may be interested in the wiki page Monad (in Computer Science) on nLab.

I think the book Category Theory for Computing Science by Michael Barr and Charles Wells may be helpful as well, particularly Chapter 14 Section 3, "Triple" (another name of monad).

Finally there is a long series about monad on https://stringdiagram.com.

view this post on Zulip Pierre R (Feb 07 2025 at 20:54):

@Qin Yuxuan, thank you! Great resources!

view this post on Zulip JR Learnstomath (Feb 13 2025 at 10:00):

Hi Pierre,

You might also want to look at Bartosz Milewski's Category Theory for Computer Programmers (the monads part starts here: https://bartoszmilewski.com/2016/11/21/monads-programmers-definition/).

Best,
JR

view this post on Zulip Ryan Schwiebert (Jun 30 2025 at 18:54):

I've also got a solid grip on Leinster's book, and am currently using Mac Lane, nLab, and "monad tutorials" one commonly finds online.

One problem I'm having with monads is that I "get" the explanation given in Mac Lane, but have a lot of trouble convincing myself why they're the same as what I encounter in these monad tutorials.

That's when I ran across What we talk about when we talk about monads which was pretty helpful. Using this and these articles on nLab 1, 2 I feel like I'm on the brink of understanding... right now I'm trying to figure out if the flatMap from computer science and the \flat decorated morphisms from Mac Lane are the same thing or not...

view this post on Zulip Kevin Carlson (Jun 30 2025 at 21:23):

I don't remember what Mac Lane writes \flat for off the top of my head but I'd be happy to try to help if you wanted to remind us of how that vs flatMap work, maybe in examples.

view this post on Zulip Ryan Schwiebert (Jul 01 2025 at 02:37):

@Kevin Carlson I think this calls for a graphic... (stay tuned)

view this post on Zulip John Baez (Jul 01 2025 at 05:37):

Can someone say (briefly and roughly) what "flatMap" is in computer science?

view this post on Zulip Ignat Insarov (Jul 01 2025 at 05:41):

flatMap is more traditionally called bind and also denoted as a terrifying infix operator =<<. It can be defined as flatMapTf=μTTf\mathrm{flatMap}^T f = μ^T ∘ Tf, for a monad TT.

view this post on Zulip Ignat Insarov (Jul 01 2025 at 05:46):

flatMap is introduced in Categories for the Working Mathematician, on page 147, section VI.5 «Free Algebras for a Monad» (in second edition), as the \flat («flat») superscript operator.

view this post on Zulip Ignat Insarov (Jul 01 2025 at 05:47):

It is called flatMap because you first «map» fTff ↦ Tf, and then «flatten» with μTμ^T.

view this post on Zulip Ignat Insarov (Jul 01 2025 at 05:55):

Speaking abstractly, flatMap or \flat is one of the two mutually inverse components of the adjunction between the category C\mathcal C for a monad T:CCT: \mathcal C → \mathcal C and the category of free algebras of TT.

view this post on Zulip Nathan Corbyn (Jul 01 2025 at 06:00):

John Baez said:

Can someone say (briefly and roughly) what "flatMap" is in computer science?

It's the Kleisli lift / extension operator

view this post on Zulip Ignat Insarov (Jul 01 2025 at 08:02):

Paolo Perrone said:

Thank you for sharing. The book looks very interesting and accessible.

view this post on Zulip Ryan Schwiebert (Jul 01 2025 at 11:44):

flatMap=bind=the transpose map in the adjunction here X(x,GT(yT))XT(FT(x),yT)X(x,G_T(y_T))\overset{\flat}\to X_T(F_T(x),y_T) was coming in my next post :sweat_smile: I'll still try to complete the infographic...

The first place I found the phrase "Kleisli extension" was at nLab. I think one of the things I'm seeking clarity on is "what does the Kleisli category formulation of monads bring to the table, as compared to the older "map-join" formulation?"

The other thing I was trying to get straight in my head was going to be "when programming with monads, what am I handling? Am I using T,μ,ηT,\mu,\eta? Or am I typically using "bind"? Am I operating on things in the image of TT? (That's what it seems like, anyway...)

view this post on Zulip Ryan Schwiebert (Jul 01 2025 at 12:05):

For example, an answer might be along the lines of "you move into the Kleisli category with FTF_T and do stuff there and come back with GTG_T." or something like that. I have no idea if that's the right picture though.

view this post on Zulip Ignat Insarov (Jul 01 2025 at 12:58):

You are typically using bind and ηη. Ideally you even have a special notation called do that kind of integrates bind with λ calculus, but do notation is only available in fancy languages. I do not think the mindset of practical computer programming is helped in any way by FTF_T and GTG_T. In my experience, it is all about syntactic and typological thinking. For example: «I need a function of such and such type, how can I build it out of the stuff I have?» And the stuff you have includes the action map of TT on arrows, the bind thing, and other devices. In functional programming, the problem is always to construct an arrow of a certain type, possibly verifying certain equations. Imperative and object oriented programming is much more complicated, involves all kinds of temporal and dynamic reasoning, and is not helped much by monads or other categorial formalities.

view this post on Zulip Alex Kreitzberg (Jul 01 2025 at 14:01):

I respectfully disagree with "Monads aren't useful for imperative languages".

When designing an API, you want it to be resistant to changes in the implementation, and a nice way to do that is use APIs that are more general than particular applications.

To me it seems this clarity over the really fundamental interfaces helped Rust make nice choices with their error system for example.

view this post on Zulip Ignat Insarov (Jul 01 2025 at 14:10):

Can you explain to me how exactly monads are useful for imperative languages? I do not see the picture you have in mind. How do you use your knowledge of monads when designing API that are resistant to changes in the implementation? I am not familiar with Rust's error system, so this example does not help.

I readily agree that it is possible to think about an imperative program as a functional program with a suitable monad. I am not sure but possibly we can even claim that any imperative environment can be modelled by a suitable monad. What I meant to express is that the problems of the kind you solve in the practice of imperative programming do not lend themselves to categorial reasoning. I shall be happy to be shown wrong about this!

view this post on Zulip Zoltan A. Kocsis (Z.A.K.) (Jul 01 2025 at 14:44):

@Ignat Insarov Cutting down on repetitive and error-prone boilerplate is a pretty big use case for monads in software development (e.g. this is the main purpose of the Monad instance for Haskell's Maybe).

Since imperative languages suffer from error-prone repetitive boilerplate just as often, monads have plenty of useful applications in imperative programming.

Of course, monads won't make imperative programs _in general_ amenable to equational reasoning (much less categorial reasoning), but a well-chosen monad can certainly make reasoning about the parts of the program using the monad easier and more compositional.

view this post on Zulip Ignat Insarov (Jul 01 2025 at 14:45):

Can you give me an example? Like, how does this work practically, not in principle?

view this post on Zulip Zoltan A. Kocsis (Z.A.K.) (Jul 01 2025 at 15:51):

Ignat Insarov said:

Can you give me an example? Like, how does this work practically, not in principle?

Not sure what sort of example you're looking for, but the classic example for when you'd use a monad in an imperative language is backtracking search.

I attach a self-contained C# example of implementing backtracking search using the List monad: C# list monad.

Of course, you will find monads in almost any commercial C# program, under the name LINQ.

view this post on Zulip Alex Kreitzberg (Jul 01 2025 at 17:48):

I like Zoltan's example, but here's the example I had in mind.

Stroustrup has nice discussion on the motivations for exceptions, in his book "C++ programming language". He goes over many pros and cons of various error handling mechanisms.

One of his examples of bad code you're forced to write without access to exceptions was the following

 if(g(1))
    if(g(2))
        return true;
    else return false;
else return false;

With the warning being, that you can't assume all programmers will be this systematic in addressing their errors, and few programmers want to write code like this anyways.

Most people want to write, and read, the following instead:

g(1)
g(2)  //If either of these fail, this fact is communicated automatically by the computer if exceptions are used.

An implicit monadic interface allows the programmer to abstract over the pattern Stroustrup doesn't like without adding a dedicated language feature.

A common situation, is a systems programmer asks for memory to be allocated, but there's some chance there isn't enough, or there's some other error, so a null pointer may be returned instead. And typically we have to compose these one after another. Then something like the following is workable:

template<typename A, typename F>
auto bind(F f, G g){
    return [=](auto x){
        auto out = f(x);
        if(out != nullptr){
            return g(&out);
        } else return nullptr;
    };
}

The simple idea is to put the pattern Stroustrup doesn't like behind a function call, but is that actually a good idea? It being one operation of a Monad makes it much more likely this is a reasonable thing to do. Optional has a version of this implemented as and_then.

Rust runs with this, Rust has disjoint unions and commonly returns errors via these. Further Rust requires you define your functions on all of the cases. Consequently, you're forced to write code in the style Stroustrup says is bad, except because we know these are monads, we know everything should be fine if we simply have the error return the first occurance of an error in the signature of our function.

So rust provides sugar, and methods for this plumbing.

So a program that you'd be forced to write like this (what Stroustrup doesn't like):

use std::fs::File;
use std::io::ErrorKind;

fn main() {
    let greeting_file_result = File::open("hello.txt");

    let greeting_file = match greeting_file_result {
        Ok(file) => file,
        Err(error) => match error.kind() {
            ErrorKind::NotFound => match File::create("hello.txt") {
                Ok(fc) => fc,
                Err(e) => panic!("Problem creating the file: {e:?}"),
            },
            _ => {
                panic!("Problem opening the file: {error:?}");
            }
        },
    };
}

can instead be written like this (using properly defined methods, and sugar via ?):

use std::fs::File;
use std::io::{self, Read};

fn read_username_from_file() -> Result<String, io::Error> {
    let mut username = String::new();

    File::open("hello.txt")?.read_to_string(&mut username)?;

    Ok(username)
}

The question mark syntax is like C#'s nullable, where failed outputs propagate automatically to the return.

That said, I'm not a Rust programmer, so I don't understand the nuance of their choices, and I know they're a pragmatic bunch so I'm sure their choices don't match perfectly with my intuition for this. I recommend you read their take on this stuff in detail if you want a more authoritative perspectives (https://doc.rust-lang.org/book/ch09-02-recoverable-errors-with-result.html)

Note, this is just one example, again the big win for me with this stuff is when Zoltan says LINQ stuff are Monads, immediately I have a lot of information about what that implies about the interface. Whereas if someone says an interface is "applyable" or something, I have very little idea of what that entails, or what that means. The categorical language is extremely useful when I need to work with multiple libraries, or one library over a long period of time.

view this post on Zulip Alex Kreitzberg (Jul 01 2025 at 17:54):

When someone says the natural numbers are a monoid over addition, then you know they added zero, and have some sense why this is a good thing to do. When someone calls something a Monad, you know they're adding dummy wrappers and such, and again, have some sense why this makes life easier.

view this post on Zulip Ignat Insarov (Jul 01 2025 at 18:10):

I see, so, as far as imperative languages go, we are talking, more often than not, about a pre-determined set of monads, provided by language designers. Examples: LINQ, exceptions. Right?

I am still not sure I understand how exceptions work in Rust. They have a sum type with two variants that signal success and error. The Result type. Is it hard-wired into the compiler?

view this post on Zulip Alex Kreitzberg (Jul 01 2025 at 19:11):

C++'s optional is not built into the language, and technically the language has a form of higher kinded types with template templates. But the committee didn't build around it because they felt those features were hard to use.

But they could be used in principle.

C++ Futures don't match a monadic interface, even though they could, which Bartosz argued about extensively a bit ago. So it's meaningful to talk about a designed interface supporting monadic operations.

So no, I don't think there's a meaningful sense in which the only Monads present are the ones provided by the language, with respect to C++.

But even if that were true, the question at issue is whether Monads are useful for imperative programming. Even if they were only provided by the language, they would still be useful.

My understanding is Result is not hardwired into the compiler.

view this post on Zulip Ignat Insarov (Jul 01 2025 at 20:50):

Oh, so C++ joins JavaScript among the languages that failed to make futures / promises aligned with the monad interface. Sad.

C++ Futures don't match a monadic interface, even though they could,
which Bartosz argued about extensively a bit ago. So it's meaningful to
talk about a designed interface supporting monadic operations.

Can you link me to this extensive argument?

view this post on Zulip Alex Kreitzberg (Jul 01 2025 at 21:25):

In these links you see Bartosz grappling with the issues, but not using monad terminology yet
https://bartoszmilewski.com/2009/03/03/broken-promises-c0x-futures/,

https://bartoszmilewski.com/2009/03/10/futures-done-right/

And here he's loudly asking for a monadic interface:
https://bartoszmilewski.com/2014/02/26/c17-i-see-a-monad-in-your-future/

Across his blog you can see him thinking about concurrency and multi-threading for years.

I believe I saw a tweet of his at some point where he explicitly said this (or some other similar interface), got him to understand the deeper significance of the categorical ideas behind these imperative interfaces.

Reading between the lines of your frustration a bit, I'm also partial to this video of Eric meijer's discussion on the way these ideas help one understand language specifications:

https://youtu.be/JMP6gI5mLHc?si=DiDZBCUzcZWuAZn5

Specifically, two half's of an adjunction can be seen in Java's language specification, my understanding of Meijer's view is that therefore the monads are hiding in the spec "unintentionally". Ergo, monads help one understand what the language is doing, because they occur "in the wild", not because they're designed into the language.

Anyways, I hope this felt useful and not redundant. There's something about software that makes programmers extremely particular about definitions like this, and I'm no exception. But I hope I collected something here that's fun to think about.

view this post on Zulip Ignat Insarov (Jul 01 2025 at 21:37):

This is great! @Alex Kreitzberg Thanks!

view this post on Zulip Ryan Schwiebert (Jul 01 2025 at 22:22):

Ignat Insarov said:

You are typically using bind and ηη.

It's probably time for me to immerse myself in examples. The environment I'm working in is Kotlin, and there's a library for it called Arrow that should be my starting point. Regarding the snippet of your comment I've quoted: So, is it right to say that η\eta is going to put types into the image of the object function of TT, and then on these wrapped types, I bind on functions obtaining a new thing in the image of TT's object function?

view this post on Zulip Ignat Insarov (Jul 01 2025 at 22:41):

You could do that, but you do not have to. Say your monad is called MM. If you have a value x:Xx: X and a function f:XMYf: X → MY, you can do f(η(x))f^\flat (η (x)), or you can simply do f(x)f (x).

Rather, ηη is used in more complicated situations, as a syntactic convenience. For example, say you want to read a file, bind the contents to a variable, and then count the characters. You can do it like so: read(file)>>=λx.η(countx)\mathrm {read} (\mathrm{file}) {\small >>=} λ x. η (\mathrm {count} x). This is convenient when you use do notation, but is not necessary, because ηη is natural, so you can always move it next to a μμ and simplify your code.

I am not sure if there are any situations where ηη is unavoidable.

view this post on Zulip Ignat Insarov (Jul 01 2025 at 22:46):

This syntactic game becomes more interesting when you get access to devices like sequence:FMMF\mathrm{sequence}: FM → MF, where FF is a special kind of functor which supports this operation, and MM is a monad. Another way to make this game more interesting is to stack several compatible monads on top of one another.

view this post on Zulip Ryan Schwiebert (Jul 01 2025 at 23:24):

Ignat Insarov said:

stack several compatible monads

I had that thought not long ago: it seems like it would be common for different monadic operations to interleave in complex ways. When the goal is to use monads to reason about the behavior, is it still possible to keep this straight when several monads are in play? Maybe with sufficient compatibility between them?

view this post on Zulip Ignat Insarov (Jul 02 2025 at 08:26):

There is a thing called «distributive law» that is a natural transformation MNNMMN → NM with some equations that ensure NMNM is a monad insofar as NN and MM are. We can also safely get a composite monad by composing a monad and an adjunction. Both of these tasks are only a little bit technical. But monads so composed can get rather baroque in practice. The earliest reference for distributive laws is Distributive Laws by John Beck, in Lecture Notes in Mathematics, No. 80, Springer-Verlag, 1969.

Then, there is a whole cottage industry of algebraic and even, I guess, «non-algebraic» effects and handlers. It seems to be in deep weeds right now. I expect there is an elegant theory underneath, and I am waiting for a hero that will unearth it and shed the light of certainty on it. What Is Algebraic about Algebraic Effects and Handlers by Andrej Bauer is a source I used as a reference more than once.

view this post on Zulip Mike Shulman (Jul 02 2025 at 08:34):

I found that paper of Bauer's quite good at shedding light on the elegant theory! (-:

view this post on Zulip Mike Shulman (Jul 02 2025 at 08:36):

I think the short answer to how algebraic effects allow you to combine monads cleanly is that when all the monads are finitary, you can just take their coproduct in the category of monads. That gives you a way to put them together without any "interaction".

view this post on Zulip Mike Shulman (Jul 02 2025 at 08:36):

If you need nontrivial interaction, you can often get that with handlers. Those are admittedly harder to understand from a category-theoretic viewpoint, but from a programming standpoint I think they're pretty easy to explain: an effect is like a "resumable exception" and a handler is like an exception handler except it can return a value to the raiser.

view this post on Zulip Ignat Insarov (Jul 02 2025 at 08:40):

Andrej's article is great, but I do not feel like I have the instruments needed to investigate real world programs after reading it. It is possible that I was not able to understand some more advanced parts of it completely.

view this post on Zulip Ignat Insarov (Jul 02 2025 at 08:42):

For instance, given some code with effects and handlers, I find it hard to state what needs to be checked before I can conclude or refute that these effects are algebraic.

view this post on Zulip Mike Shulman (Jul 02 2025 at 08:45):

I thought as soon as you see code written with "effects and handlers" it is by definition algebraic.

view this post on Zulip Ignat Insarov (Jul 02 2025 at 08:45):

I do not have any reason to think so or otherwise. I am really lost on this question.

view this post on Zulip Ignat Insarov (Jul 02 2025 at 08:46):

when all the monads are finitary, you can just take their coproduct in the category of monads

Was this in Andrej's article? Sounds like great news, although I need to scribble for some time before I understand what a «sum of monads» could be.

By the way, is it a sin to call co-limits without equations «sums» instead of that long word you are using?

view this post on Zulip Mike Shulman (Jul 02 2025 at 08:48):

Ignat Insarov said:

is it a sin to call co-limits without equations «sums» instead of that long word you are using?

No. Although "that long word you are using" is even longer than "coproduct". (-:O

view this post on Zulip Mike Shulman (Jul 02 2025 at 08:53):

Looking up the effects bibliography I find a paper called Composing monads using coproducts.

view this post on Zulip Ignat Insarov (Jul 02 2025 at 08:59):

Oh, I actually have this article bookmarked. Along with 100 other I should have read a long time ago.

view this post on Zulip Ryan Schwiebert (Jul 02 2025 at 22:36):

@Ignat Insarov What I think unsettles me the most is not knowing what exactly is being handled or used. If I consider "bind" as the main operation, it sounds like I'd usually be handling objects in the image of TT (viewed another way, after coming out of the right adjoint GTG_T?) and "Kleisli morphisms" xTyx\to Ty, which leaves you with something in the image of TT again. Is that the interaction every time? Maybe the thing I'm missing is how this works well with "do" which I currently probably don't have an appreciation of.

view this post on Zulip Ignat Insarov (Jul 04 2025 at 10:42):

I have come up with another approach to explaining the use of monads in software engineering.

Imagine something like λ calculus but with a special syntax for abstractions, say κ x. e, where (κ x. e₁) e₂ is defined in one of these trivially equivalent ways:

This is very close to what do notation gives you. Specifically, we can offer two way syntactic conversions:

do notation ⇄ κ calculus ⇄ λ calculus

Here:

So:

Of course, industrial imperative languages must throw a wrench or two into our elegant clockwork. For instance, in C you can use curly braces to denote variable scoping, and this means our do notation for C will not be associative «out of the box». We can always do away with variable scoping by removing curly braces and coming up with fresh names for shadowed variables, so in this instance we can reaffirm that C can be described by a monad. We shall also need to deal with references and pointers, but this should not be too hard.

Does this explanation make sense?

There are other notations for (perhaps more fanciful) monads, like the LINQ notation mentioned above and its mathematically styled predecessor called «list comprehension». I wonder if we can take this parallel as far as to claim that SQL is a syntax for a certain kind of monads.

view this post on Zulip Ryan Schwiebert (Jul 04 2025 at 11:56):

@Ignat Insarov It's another helpful perspective (although my lack of familiarity with lambda/kappa calculus and functional programming in general is an issue).

I've also been finding this blog post extremely helpful. The Bartosz Milewski youtube lectures I had seen before this never got to the depth I needed, but if this is any indication, I should be reading his blog to get that information...

view this post on Zulip Ignat Insarov (Jul 05 2025 at 02:03):

Well, you cannot possibly be familiar with κ calculus since I just invented it.

view this post on Zulip Ryan Schwiebert (Jul 05 2025 at 02:16):

@Ignat Insarov Oh? I thought you were referring to this.

view this post on Zulip Ignat Insarov (Jul 05 2025 at 02:17):

Maybe I should start using Chinese characters. There are hardly any Greek left.

view this post on Zulip Ignat Insarov (Jul 05 2025 at 02:24):

I renamed it to ζ calculus, hopefully there is no such calculus in existence yet.

view this post on Zulip Ryan Schwiebert (Jul 05 2025 at 15:22):

I'm getting a better appreciation for how they're being used in programming, and I find the ideas of a monad, its E-M and Kleisli categories, and relationship with adjunctions, and T-algebras very interesting in themselves, but let me ask this in all seriousness:

What does one accomplish using this handful of methods in category theory? Is it mainly a unifying tool?

I can imagine at any given juncture we may have an adjunction, or perhaps a T algebra, and then one goes through motions to inspect this family of related things. Maybe an example of what sorts of insights this process gives would be helpful.

view this post on Zulip John Baez (Jul 05 2025 at 16:45):

What does one accomplish using this handful of methods in category theory? Is it mainly a unifying tool?

Are you asking what computer scientists accomplish this way? Or are you asking what mathematicians accomplish?

I think these are quite different questions.

I have no real understanding of the former, since I don't really program. The latter is something I understand.

view this post on Zulip Alex Kreitzberg (Jul 05 2025 at 17:11):

I still feel like a relative novice, so I'm curious how the pros would answer that question.

But that said, learning category theory feels very strange. For me, it requires an enormous amount of energy, but then when something finally makes sense, it seems very simple in retrospect, but not vacuously so. A math mentor of mine once described algebra as "a lot of little results" vs analysis's "a few big results".

Learning category starts like "oh it's a lot of little results!" But then it transitions to feel like "It's a few little results, applied over and over again?" And what I mean by that, is category theory is more self reinforcing than any other math subject I've learned. When you've learned a critical mass of category theory, what you learned feels self evident, and what's left feels forced. After this ball gets rolling, you see it all over the place in mathematics, proving simple stuff over and over and over again.

It's as if you get a couple new programming language features, and suddenly, everything needs half as many clever tricks to write, it's very strange.

Less abstractly though I find Dan Piponi's application of Commutative Monads here very fun, there's a video link at the bottom of https://dl.acm.org/doi/abs/10.1145/1631687.1596553

view this post on Zulip Alex Kreitzberg (Jul 05 2025 at 18:54):

After I wrote that I came up with a personal concrete example.

I'm a bit embarrassed with how difficult "change of variables" or "coordinate transformations" have been for me. Recently I've been reviewing them in "mathematics form and function" and it's been fun to "fill in" the category theory Mac Lane implies.

In it he gives a diagram [0,1]lCϕDfR[0, 1] \xrightarrow{l} C \xrightarrow{\phi} D \xrightarrow{f} \mathbb{R}

As the formal composition of l:[0,1]Cl : [0, 1] \rightarrow C, ϕ:CD \phi : C \rightarrow D and f:DRf : D \rightarrow \mathbb{R} (edit: I added this line, because the previous line isn't rendering on mobile for me).

Where ϕ\phi between DD and CC are coordinate transforms. We think of elements of CC as being described by coordinates in xx, which we then rewrite in terms of coordinates of elements of DD which we notate as qiq^i of qq.

So that's fine, but what does that then mean in an expression like:

ϕlω=lϕω\int_{\phi \circ l} \omega = \int_l \phi^{*}\omega
(edit: It seems there's a bug on mobile, that's making this not render for me properly)

The path in CC, l:[0,1]Cl : [0, 1] \rightarrow C gets taken to a path in DD, ϕl:[0,1]D\phi \circ l : [0, 1] \rightarrow D; but, then the one form ω:TDTR\omega : T D \rightarrow T\mathbb{R} gets "pulled back" to ϕω:TCTR\phi^{*} \omega: T C \rightarrow T\mathbb{R}.

So by adding "type signatures" we can see this coordinate transformation playing dual opposing roles to carry out a change of variables for an integral. In one context it acts as a covariant functor, and in the other a contravariant one.

If I only worked with the formula for the integral when making sense of change of variables, I would lose the opportunity to notice these dual relationships between the spaces these functions operate between.

The rules of the signatures are "simple" enough to be automatic to carry out mentally when you understand how they work. Acting as guard rails for my calculations and my understanding. In this case they've clarified the multifaceted character of how change of variables is used, which helps me be a bit less confused by change of variables, and honestly helps me feel less bad about being confused.

One thing I see category theory doing is elevating these guard rails to a full blown theory, and getting creative with them. Monads are a present you get once this story is clarified. And they let you, as one of many examples, indicate the presence of side effects - giving you a chance to notice when side effects compose in strange ways.

view this post on Zulip John Baez (Jul 05 2025 at 19:53):

I'm still wondering what Ryan meant when he asked what monads were good for. If I were an expert Haskell programmer I'd say one thing; as a mathematician I'd say something completely different, since I've used monads at various points in my work in mathematics, for various reasons. After hearing Alex's long answer, I no longer resist mentioning that I've used monads

1) To understand the foundations of cohomology for algebraic gadgets (e.g. group cohomology and Lie algebra cohomology), since every kind of algebraic gadget has a monad that describes it, and these monads can be used to turn algebraic gadgets into topological spaces, that we can take the cohomology of. This is old stuff: it's one of the reasons monads were invented. I'm just wanted to understand it.

2) To prove theorems about PROPs (which are a kind of algebraic gadget described by a monad), in order to prove theorems about various specific PROPs, especially categories of electrical circuits.

3) To prove theorems about plethysm, which is a method of getting new representations of symmetric groups from old ones.

I should admit that in all three of these projects I relied heavily on @Todd Trimble's expertise in monads. So I'd say I'm a beginner when it comes to monads, but at least I now have a sense about when I'll need to ask Todd more questions about them to accomplish a specific task! :sweat_smile:

view this post on Zulip Alex Kreitzberg (Jul 05 2025 at 20:42):

How often can you do 1)? Can you turn any algebraic gadget modeled with a Monad into a topological space?

view this post on Zulip John Baez (Jul 05 2025 at 20:47):

Essentially 100% of the time.

view this post on Zulip John Baez (Jul 05 2025 at 20:49):

I'm saying "essentially" because my summary of cohomology and monads was so incredibly sketchy that I don't want you to draw some wacky conclusions based on that.

view this post on Zulip Alex Kreitzberg (Jul 05 2025 at 20:53):

Would a discussion about this merit a thread? I don't really want to derail this one. Is there a good word to look this up, or does this all get sorted in a classical treatment of algebraic topology?

view this post on Zulip John Baez (Jul 05 2025 at 20:55):

The easiest place to learn this stuff might be in my course notes.

view this post on Zulip John Baez (Jul 05 2025 at 21:04):

A lot of special cases are treated in Cartan and Eilenberg's 1958 book Homological Algebra, and then Mac Lane's 1963 book Homology. The slick approach based on monads goes back to Godement in 1958, but I feel it was really clearly developed only in Beck's 1967 thesis Triples, algebras and cohomology. At this time monads were called "triples".

I feel that nobody has brought this stuff down to earth and explained how simple it all is. Todd brought it to the level where I can understand it, and my course explained it in a way that students could maybe understand it... but someday I should take those course notes and really expand them.

view this post on Zulip Mike Shulman (Jul 05 2025 at 21:11):

However, most people don't talk about the process as "turning an algebraic gadget into a topological space". Usually the closest they come is turning it into a simplicial set.

view this post on Zulip John Baez (Jul 05 2025 at 21:14):

Right, but I'm trying to make this stuff seem less scary. If I said "simplicial set", I doubt Alex would be quite as interested.

view this post on Zulip John Baez (Jul 05 2025 at 21:21):

But anyway, Alex, I wasn't lying to you: you can take an algebraic gadget and turn it into a simplicial set, which is a bunch of simplices stuck together, and then you can think of that as a topological space.... and this connects topology to the theory of algebraic gadgets in a wonderful way. This is why people invented monads in the first place, and it's still one of the most beautiful and powerful applications.

view this post on Zulip Alex Kreitzberg (Jul 05 2025 at 21:23):

I believe you! And am excited by your framing.

view this post on Zulip Ryan Schwiebert (Jul 05 2025 at 21:26):

John Baez said:

what mathematicians accomplish?

I mean that I now have a picture of what programmers accomplish, and that I want to appreciate more what it buys me as a mathematician. Just some perspective would do.

view this post on Zulip John Baez (Jul 05 2025 at 21:43):

Okay, great. I've by now sketched why monads were invented in the first place: any algebraic gadget described by a monad - and that's most things I consider "algebraic gadgets", like groups and rings and monoids and modules but not fields - can be turned into a topological space using a wonderful trick called the [[bar construction]], and this lets you study the gadget using ideas from topology, e.g. you can use cohomology to study the 'holes' in that gadget.

view this post on Zulip John Baez (Jul 05 2025 at 21:48):

But also, there are so many kinds of algebraic gadgets that it's often helpful to prove general theorems about monads and then instantly know they apply to whatever wacky algebraic gadget you happen to be studying right now, whether it be a Jordan algebra or a rectangular band. (I mention these just as examples of weird algebraic gadgets that people like to study.)

view this post on Zulip Alex Kreitzberg (Jul 05 2025 at 21:55):

Do you know cool applications of the Klesli-categories of Monads for math? The examples you've mentioned so far typically use Eilenberg-Moore categories right? Or do both play a role in the above?

CS people typically see Klesli-categories first, it's almost synonymous to monads for them.

view this post on Zulip John Baez (Jul 05 2025 at 22:03):

I find that in math the Eilenberg-Moore category of a monad is typically more important, e.g. the "monad for groups" is the one whose Eilenberg-Moore category is the category of groups.

However, if you start with a finitary monad and want to extract a Lawvere theory from it, you consider its Kleisli category, and find sitting inside there the category of finitely generated free algebras of the monad, and then take its opposite. For example, the Lawvere theory for groups is the opposite of the category of finitely generated free groups!

I used to really hate the terms "Eilenberg-Moore category" and "Kleisli category" for a monad because they sounded so intimidating, and I could never remember which was which. I would still prefer to call them the "category of algebras" and the "category of free algebras" of the monad. But I am now such a jaded veteran that I can say "Eilenberg-Moore category" without blushing.

view this post on Zulip Mike Shulman (Jul 05 2025 at 23:01):

John Baez said:

Right, but I'm trying to make this stuff seem less scary. If I said "simplicial set", I doubt Alex would be quite as interested.

Yes, that makes sense. But I thought if he was going to start looking into the literature, it might also be useful to know the words that most people use.

view this post on Zulip Mike Shulman (Jul 05 2025 at 23:05):

John Baez said:

I find that in math the Eilenberg-Moore category of a monad is typically more important

I suspect one reason for that is that mathematicians like to work in categories that have limits and colimits, and EM-categories inherit limits from the base category and usually also colimits, while Kleisli categories don't.

view this post on Zulip Mike Shulman (Jul 05 2025 at 23:07):

John Baez said:

But also, there are so many kinds of algebraic gadgets that it's often helpful to prove general theorems about monads and then instantly know they apply to whatever wacky algebraic gadget you happen to be studying right now

This is probably the most common way that I've used monads in my research. Often in the guise of 2-monads, specifically that whenever you have a kind of 2-dimensional algebraic gadget that can be described as the algebras for a 2-monad, you automatically get well-behaved notions of pseudoalgebra, pseudomorphism, lax morphism, and colax morphism.

view this post on Zulip Ryan Schwiebert (Jul 06 2025 at 00:45):

@John Baez Well I'm happy to learn anything new about dealing with algebraic gadgets since I'm essentially a ring and module theorist. And I don't mind the topology either: that was my sub-specialty...

I've never properly learned homology or cohomology though. I have learned some of the picture about simplices and "holes" during my dip into geometric mechanics. What form does the "hole" information take for something like a ring or a module? Is that all there is, just an abstracted notion of some hole-of-some-dimension? Or can one tie it to something more recognizable?

view this post on Zulip John Baez (Jul 06 2025 at 02:24):

Very very very roughly, the points in the space are expressions in your algebraic structure (like elements of your ring like rr and ss, but also formal unevaluated expressions like rs1r s^{-1} ), and paths are ways of going from an expression to a more evaluated expression. So holes detected by the first cohomology group reflect the fact that can be two fundamentally different paths from one point to another: that is, two fundamentally different ways to evaluate the same expression.

A bit less roughly, your space comes from a simplicial set, and 0-simplices come from formal expressions in your algebraic gadget, and 1-simplices come from formal expressions in formal expressions in your algebraic gadget, and 2-simplices come from formal expressions in formal expressions in formal expressions in your algebraic gadget, and so on. You should be thinking about an adjunction L,RL, R and taking your algebraic gadget XX and forming RXR X and then RLRXR L R X and then RLRLXR L R L X and so on. The monad here is RLR L and there's also a comonad LRL R.

view this post on Zulip John Baez (Jul 06 2025 at 02:28):

The key facts underlying this business are that

(I said "just" in order to comply with the meme.)

The details are explained in my notes. If anyone wants to get paid for turning these notes into LaTeX with pictures, please let me know.

view this post on Zulip Patrick Nicodemus (Jul 06 2025 at 10:55):

(deleted)

view this post on Zulip Zoltan A. Kocsis (Z.A.K.) (Jul 06 2025 at 11:46):

While gentlemen would not bring this up in a learning thread at all, if it ever made sense to mention it, now works better than any other time. :top_hat:

There is a slight technicality in that functional programming monads do not always correspond to monoid objects in categories of endofunctors.

For example, given a type universe U\mathcal{U}, you can define an operation F:UUF: \mathcal{U} \rightarrow \mathcal{U}' to a higher universe U\mathcal{U}' by F[X]:=UXF[X] := \mathcal{U} \rightarrow X. This comes equipped with the expected eta and bind operations, but does not correspond to a monoid object in an endomorphism category in any straightforward sense. In particular, F[F[X]]F[F[X]] does not type-check, since F[X]F[X] lives outside the universe U\mathcal{U}.

view this post on Zulip Oscar Cunningham (Jul 06 2025 at 11:58):

Similarly in category theory people call the Yoneda embedding the free cocompletetion, but it's actually a map from small categories to large categories.

view this post on Zulip John Baez (Jul 06 2025 at 12:05):

Gentlemen do not speak of such things. :shh:

(Just kidding. Relative monads.)

view this post on Zulip Nathanael Arkor (Jul 06 2025 at 12:25):

It's not inaccurate to call the Yoneda embedding of a small category the free cocompletion; it's just that "free constructions" do not always correspond to monads, but rather to [[relative monads]], as John says.

view this post on Zulip Paolo Perrone (Jul 06 2025 at 18:45):

There is also the embedding of a (possibly) large, locally small category into its category of small presheaves. That is the free cocompletion under colimits of small diagrams. Very often small colimits are all you need. (Not always: adjoint functor theorem, etc.)

view this post on Zulip Alex Kreitzberg (Jul 06 2025 at 21:39):

I audited my understanding of these monad categories a bit, if TT is the free monoid monad, then

The klesli composition f:ATBg:BTCf : A \rightarrow TB \circ g : B \rightarrow TC makes sense, because maps from TBT B are determined by maps on BB by the universal property of the free monoid. So Klesli composition is consistent with those arrows being arrows in the category of free monoids.

The TT-Algebra over SetSet is the category of monoids. Which inherit limits from SetSet per Shulman's note. We do get categorical products and the terminal object in MonMon. Which is a good thing for doing category theory!

TT applied to the terminal object in SetSet gives T{}T\{*\} which is just lists of one element, which is isomorphic to the natural numbers. But in particular N\mathbb{N} isn't terminal in the klesli category, there are lots of maps from any set into N\mathbb{N}, so the limits aren't preserved in an obvious way.

I've noted to myself, that in a language with side effects, the standard universal properties don't really work, every homset has lots of arrows for example, so you don't have initial and terminal objects. Klesli categories seem to faithfully reflect this disadvantage. Which I saw as an advantage of them for modeling and understanding standard side effecting imperative languages.

I'm surprised this specific disadvantage is likely a key reason why klesli categories are less popular than eilenberg moore categories. Because imperative languages seem popular, in spite of sharing the same disadvantage. I'm curious "why" but I'm not sure it'd be easy to give a good simple reason for this.

Something that strikes me, is I've always found it somewhat strange that programmers are drawn to very free structures like free-monoids - whereas mathematicians try to stick with somewhat nicer structures like groups. Klesli-categories being categories of free algebras, vs the mathematically preferred categories of algebras, seems to reflect this "cultural" preference at a deeper level.

Is there a simple reason for this?

I find myself trying to articulate questions like "Are there more well behaved type systems than Klesli categories for effects systems, that also look like contemporary imperative languages?" to poke at this distinction - but if somebody thinks they know why programmers prefer free stuff, I'd love to hear their take.

view this post on Zulip John Baez (Jul 06 2025 at 21:47):

I believe the reason programmers are drawn to free algebras is that free algebras naturally arise when you study syntax. That is, when you have a bunch of operations and you write down a formula involving these operations and maybe some variables, like

a(b+(c(e+f)))g a \cdot (b + (c \cdot (e + f))) \cdot g

you are giving an element in a free algebra of some monad. Programmers are drawn to syntax because syntax is what you type into a computer.

There's a sense in which "Kleisli categories are to syntax as Eilenberg-Moore categories are to semantics".