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.
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
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.
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!
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.
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.
@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.
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!
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.
@Qin Yuxuan, thank you! Great resources!
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
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 decorated morphisms from Mac Lane are the same thing or not...
I don't remember what Mac Lane writes 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.
@Kevin Carlson I think this calls for a graphic... (stay tuned)
Can someone say (briefly and roughly) what "flatMap" is in computer science?
flatMap
is more traditionally called bind
and also denoted as a terrifying infix operator =<<
. It can be defined as , for a monad .
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») superscript operator.
It is called flatMap
because you first «map» , and then «flatten» with .
Speaking abstractly, flatMap
or is one of the two mutually inverse components of the adjunction between the category for a monad and the category of free algebras of .
John Baez said:
Can someone say (briefly and roughly) what "flatMap" is in computer science?
It's the Kleisli lift / extension operator
Paolo Perrone said:
- I wrote these lecture notes (see section 5 for monads), which later became this book (see chapter 5 for monads and sections 6.4 and 6.5 for strong monads etc.)
Thank you for sharing. The book looks very interesting and accessible.
flatMap=bind=the transpose map in the adjunction here 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 ? Or am I typically using "bind"? Am I operating on things in the image of ? (That's what it seems like, anyway...)
For example, an answer might be along the lines of "you move into the Kleisli category with and do stuff there and come back with ." or something like that. I have no idea if that's the right picture though.
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 and . 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 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.
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.
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!
@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.
Can you give me an example? Like, how does this work practically, not in principle?
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.
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.
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.
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?
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.
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?
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.
This is great! @Alex Kreitzberg Thanks!
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 is going to put types into the image of the object function of , and then on these wrapped types, I bind on functions obtaining a new thing in the image of 's object function?
You could do that, but you do not have to. Say your monad is called . If you have a value and a function , you can do , or you can simply do .
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: . 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.
This syntactic game becomes more interesting when you get access to devices like , where is a special kind of functor which supports this operation, and is a monad. Another way to make this game more interesting is to stack several compatible monads on top of one another.
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?
There is a thing called «distributive law» that is a natural transformation with some equations that ensure is a monad insofar as and 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.
I found that paper of Bauer's quite good at shedding light on the elegant theory! (-:
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".
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.
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.
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.
I thought as soon as you see code written with "effects and handlers" it is by definition algebraic.
I do not have any reason to think so or otherwise. I am really lost on this question.
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?
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
Looking up the effects bibliography I find a paper called Composing monads using coproducts.
Oh, I actually have this article bookmarked. Along with 100 other I should have read a long time ago.
@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 (viewed another way, after coming out of the right adjoint ?) and "Kleisli morphisms" , which leaves you with something in the image of 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.
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:
bind
(λ x. e₁) e₂This is very close to what do
notation gives you. Specifically, we can offer two way syntactic conversions:
do
notation ⇄ κ calculus ⇄ λ calculus
Here:
do
notation is a general syntax for writing imperative programs.
Via do
notation, we can see any imperative program as a program in the κ calculus of the monad characterizing that particular language's input and output facilities. The associativity of the monad is then reflected in that you do not need to group the statements of your imperative program with any parentheses.
Specifically, do
{x ← e₁; e₂} becomes (κ x. do
e₂) (do
e₁) and do
{e} becomes e. η is automatically ascribed where needed in non-pure languages.
λ calculus is a general syntax for writing functional programs.
λ calculus can be inlaid into our κ calculus by interjecting η here and there, like so:
η ((λ x. e₁) e₂) = μ (T (λ x. η e₁) (η e₂)) = (κ x. η e₁) (η e₂)
So:
do
notation.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.
@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...
Well, you cannot possibly be familiar with κ calculus since I just invented it.
@Ignat Insarov Oh? I thought you were referring to this.
Maybe I should start using Chinese characters. There are hardly any Greek left.
I renamed it to ζ calculus, hopefully there is no such calculus in existence yet.
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.
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.
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
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
As the formal composition of , and (edit: I added this line, because the previous line isn't rendering on mobile for me).
Where between and are coordinate transforms. We think of elements of as being described by coordinates in , which we then rewrite in terms of coordinates of elements of which we notate as of .
So that's fine, but what does that then mean in an expression like:
(edit: It seems there's a bug on mobile, that's making this not render for me properly)
The path in , gets taken to a path in , ; but, then the one form gets "pulled back" to .
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.
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:
How often can you do 1)? Can you turn any algebraic gadget modeled with a Monad into a topological space?
Essentially 100% of the time.
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.
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?
The easiest place to learn this stuff might be in my course notes.
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.
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.
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.
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.
I believe you! And am excited by your framing.
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.
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.
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.)
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.
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.
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.
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.
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.
@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?
Very very very roughly, the points in the space are expressions in your algebraic structure (like elements of your ring like and , but also formal unevaluated expressions like ), 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 and taking your algebraic gadget and forming and then and then and so on. The monad here is and there's also a comonad .
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.
(deleted)
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 , you can define an operation to a higher universe by . 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, does not type-check, since lives outside the universe .
Similarly in category theory people call the Yoneda embedding the free cocompletetion, but it's actually a map from small categories to large categories.
Gentlemen do not speak of such things. :shh:
(Just kidding. Relative monads.)
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.
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.)
I audited my understanding of these monad categories a bit, if is the free monoid monad, then
The klesli composition makes sense, because maps from are determined by maps on 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 -Algebra over is the category of monoids. Which inherit limits from per Shulman's note. We do get categorical products and the terminal object in . Which is a good thing for doing category theory!
applied to the terminal object in gives which is just lists of one element, which is isomorphic to the natural numbers. But in particular isn't terminal in the klesli category, there are lots of maps from any set into , 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.
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
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".