Stream: general

Kenny Lau (Feb 18 2019 at 10:19):

Would it be useful to have monads on categories instead of always on Types?

Kenny Lau (Feb 18 2019 at 10:21):

that would also require Cartesian-Closed-Categories though

Johannes Hölzl (Feb 18 2019 at 10:22):

Yes, they are also interesting for category theory. An instance I'm interested in is the monad on measurable spaces, i.e. the Giry monad. But keep in mind that they are different beasts than the Type-monads. The latter is very normal in DDT, the former is more involved.

Johannes Hölzl (Feb 18 2019 at 10:22):

Hm, I don't think so. Monads work on arbitrary functors no CCCs are required.

Kenny Lau (Feb 18 2019 at 10:22):

but we also want <*> don't we

Johannes Hölzl (Feb 18 2019 at 10:25):

I'm not sure what the best approach is. Keep in mind that monads in category theory are different, the morphisms are not necessary functions.

Johannes Hölzl (Feb 18 2019 at 10:25):

Often they are a subset of functions, but not in a CCC (at least not in Top or Meas)

Simon Hudon (Feb 18 2019 at 16:28):

I have a draft of those (monads and CCCs) on my drive. I can clean them up and PR them

Simon Hudon (Feb 18 2019 at 16:29):

@Johannes Hölzl Do you think it's a good idea to define monads as their Kleisli category and then derive a monoid from them?

Johan Commelin (Feb 18 2019 at 16:35):

For adjunctions we also had choices, and we came to the conclusion that we just wanted both.

Johan Commelin (Feb 18 2019 at 16:35):

Redundancy of data in definitions seems to be a good thing.

Johannes Hölzl (Feb 18 2019 at 16:38):

@Simon Hudon I think we should focus on what we need. Do you have a case where you get a Kleisli category? Or do you have a functor + monad properties? In my case I currently need the later.

Simon Hudon (Feb 18 2019 at 16:48):

When you say monad properties, do you mean as a monoid? I have a preference for the kleisli category because it does not depend on monoidal catergories (of which there seems to be an endless supply of bad definitions) and it is easier to connect to programming

Reid Barton (Feb 18 2019 at 16:48):

I think this has come up before, but my view is that we certainly want the ordinary definition of a monad at some point (i.e., a functor $T : C \to C$ with a unit $1 \to T$ and multiplication $T \circ T \to T$ such that ...), but monads aren't actually as useful for proving basic things about algebraic categories as books on category theory would have you believe.

Reid Barton (Feb 18 2019 at 16:51):

Because in the monad approach you still have to define the monad and its multiplication from scratch, and the monad is supposed to compute, for example, the free group on a set, and writing that down is most of the work of proving that the category of groups has colimits or whatever. And then you still have to check that algebras for the free group monad are the same as groups defined in the usual way, because your examples are all in the latter form.

Reid Barton (Feb 18 2019 at 16:56):

But there are also more significant applications of monads. Note this is all from a math perspective.

Reid Barton (Feb 18 2019 at 17:04):

The issue related to CCCs is I guess monad extends appllicative, which is supposed to mean a lax closed functor or lax monoidal functor depending on your point of view. That is something specific to the category of types (sets)--actually I'm not sure in what generality it holds. I actually don't see why the category being a CCC should be enough, I think you also need the monad to be a strong functor.
But anyways, that might cause some difficulty if we try to unify monad with the monads from category theory.

Reid Barton (Feb 18 2019 at 17:16):

@Simon Hudon by "the kleisli category" do you mean something like page 35 of http://www.cse.chalmers.se/research/group/logic/Types/Uustalo-lectures.pdf? That is, specifying a monad by giving its Kleisli category

Simon Hudon (Feb 18 2019 at 17:29):

That looks similar. I'm not too well versed in the who adjunction business but I think that's the same. You can specify a monad M on C by giving a category with the same objects as C and which defines a morphism between a --> b iff C has one between a --> M b

Reid Barton (Feb 18 2019 at 17:31):

Okay, but then you need to require something on the new category in order to know that it's the Kleisli category of some monad. (For example, it could also be the co-Kleisli category of a comonad.) Apparently, it's this right adjoint condition

Simon Hudon (Feb 18 2019 at 17:32):

Isn't that automatic?

Reid Barton (Feb 18 2019 at 17:32):

isn't what automatic?

Reid Barton (Feb 18 2019 at 17:33):

If I start with a monad, then I can build a Kleisli category, which has the same objects and a functor from the original category that is the identity on objects. But if I start with any nonsense such category, it might not come from a monad in this way (I already gave a counterexample--I could build other examples from a comonad)

Reid Barton (Feb 18 2019 at 17:35):

You also have to check that the Kleisli category "remembers" the entire monad, but I think that's some easy Yoneda argument

Simon Hudon (Feb 18 2019 at 17:37):

Ok, I see. I think I misunderstood your point. I now see that the comonad was your counterexample.

Simon Hudon (Feb 18 2019 at 17:38):

Does the whole monad have anything more than a monoid in the category of endofunctors?

Reid Barton (Feb 18 2019 at 17:39):

No, those definitions are equivalent

Simon Hudon (Feb 18 2019 at 17:40):

That's curious. I thought my Kleisli construction was sufficient to generate that monoid. I'll have to revisit it to see what I missed

Reid Barton (Feb 18 2019 at 17:41):

I agree trying to literally write "monoid object in the category of endofunctors" using monoidal categories would be a mess, but the definition you get by unraveling "monoid object" is rather simple (and what I think of as the usual one), see https://en.wikipedia.org/wiki/Monad_(category_theory)#Formal_definition

Nice! Thanks!

Reid Barton (Feb 18 2019 at 17:45):

If you start from the Kleisli category, let's call it D, you need some way to show that D(A, B) = C(A, TB) for some functor T on C. If you have that, then the monad laws for T should follow.

Simon Hudon (Feb 18 2019 at 17:49):

Ah! Yes! That's what I did! I start with T and C and the monad instance define bind : (a --> T b) -> (b --> T c) -> (a --> T c and return : a --> T a with morphisms on C together with their laws. The Kleisli category is actually derived from that. I thought of it as the Kleisli category itself because of how close they are.

Reid Barton (Feb 18 2019 at 17:50):

Okay, so you were probably thinking of something like "T : C -> C, together with a category structure on Ob C with hom sets given by A -> TB"

Simon Hudon (Feb 18 2019 at 17:52):

Yes exactly

Last updated: May 17 2021 at 22:15 UTC