Zulip Chat Archive

Stream: Is there code for X?

Topic: Morphisms of monads


view this post on Zulip Adam Topaz (Aug 10 2020 at 18:10):

Does mathlib have morphisms of monads? For now, I'm mostly interested in monads on Type*.

view this post on Zulip Simon Hudon (Aug 10 2020 at 18:31):

Mathlib has two definitions of monads. The one in category theory and the one we use for programming. Which one do you need?

view this post on Zulip Adam Topaz (Aug 10 2020 at 18:37):

Either would be fine. Since this exists:

https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/monad/types.lean

But of course, morphisms of monads in the sense of control.monad would be better, since it's more flexible with universes.

view this post on Zulip Adam Topaz (Aug 10 2020 at 18:40):

I looked briefly in category_theory.monad and didn't find anything about morphisms of monads.

view this post on Zulip Simon Hudon (Aug 10 2020 at 19:19):

For category theory, M is an endofunctor, functors form a category (see category_theory/functor_category.lean). Are those morphisms good enough?

view this post on Zulip Simon Hudon (Aug 10 2020 at 19:20):

As for the programming construct, it does not exist yet but if you define it, I'll be happy to see it PR-ed

view this post on Zulip Reid Barton (Aug 10 2020 at 19:24):

There are laws for morphisms of monads, just like a morphism of monoids has to satisfy some equations (really, they are the same equations).

view this post on Zulip Simon Hudon (Aug 10 2020 at 19:25):

Right, I did not consider that they wouldn't follow from normal natural transformations. My mistake

view this post on Zulip Adam Topaz (Aug 10 2020 at 19:25):

It's just a natural transformation that's compatible with bind and pure.

view this post on Zulip Adam Topaz (Aug 10 2020 at 19:26):

I'll try to sketch a definition.

view this post on Zulip Adam Topaz (Aug 10 2020 at 19:39):

Something like this:

variables (M N : Type*  Type*) [monad M] [monad N]

structure monad_hom (M N : Type*  Type*) [monad M] [monad N] :=
(app {α} : M α  N α)
(natural {α β} {f : α  β} {x : M α} : app (f <$> x) = f <$> app x)
(map_pure {α} {a : α} : app (pure a) = pure a)
(map_bind {α β} {ma : M α} {f : α  M β} : app (ma >>= f) = (app ma) >>= (app  f))

Does this look right?

view this post on Zulip Simon Hudon (Aug 10 2020 at 19:41):

Looks good to me

view this post on Zulip Adam Topaz (Aug 10 2020 at 19:42):

Oh, do we already have natural transformations for computer-sciency functors?

view this post on Zulip Simon Hudon (Aug 10 2020 at 19:44):

I don't believe so. The only other use of that idea in programming in mathlib is in control.traversable.basic

view this post on Zulip Mario Carneiro (Aug 10 2020 at 20:15):

Isn't this a "monad transformer" in haskell jargon?

view this post on Zulip Adam Topaz (Aug 10 2020 at 20:15):

I don't think so.

view this post on Zulip Adam Topaz (Aug 10 2020 at 20:16):

I thought a monad transformer takes one monad and makes another.

view this post on Zulip Mario Carneiro (Aug 10 2020 at 20:16):

isn't that what's happening here?

view this post on Zulip Mario Carneiro (Aug 10 2020 at 20:16):

you take elements of one monad and produce elements of another

view this post on Zulip Adam Topaz (Aug 10 2020 at 20:16):

Not quite.

view this post on Zulip Reid Barton (Aug 10 2020 at 20:16):

no, this is an ordinary function that takes an action in one monad and produces an action in another

view this post on Zulip Adam Topaz (Aug 10 2020 at 20:17):

I guess whenever you have a monad transformer T, and a monad M, you can promote the pure in T to a morphism from Mto T M.

view this post on Zulip Adam Topaz (Aug 10 2020 at 20:17):

Or something.

view this post on Zulip Simon Hudon (Aug 10 2020 at 20:18):

In more details, this is a relation between two given monads whereas, with a monad transformer, you take one monad and produce another one. I believe we could say that there should be a monad morphism between the input and the output monads of a monad transformer though

view this post on Zulip Mario Carneiro (Aug 10 2020 at 20:19):

Aha, I knew that haskellers couldn't stop themselves from rediscovering this: https://hackage.haskell.org/package/mmorph-1.1.3/docs/Control-Monad-Morph.html

view this post on Zulip Adam Topaz (Aug 10 2020 at 20:20):

Hey, at least they tell us what notation to use :)

view this post on Zulip Adam Topaz (Aug 10 2020 at 20:20):

Oh wait, I misread.

view this post on Zulip Adam Topaz (Aug 10 2020 at 20:59):

Is there some standard haskelish ascii art for natural transformations?

view this post on Zulip Adam Topaz (Aug 10 2020 at 21:02):

~> I guess.

view this post on Zulip Scott Morrison (Aug 10 2020 at 22:59):

We do now have monoid objects in monoidal categories, as well as homs between them, and the fact that endofunctors of a category form a monoidal category.

view this post on Zulip Scott Morrison (Aug 10 2020 at 22:59):

Just saying. :-)

view this post on Zulip Adam Topaz (Aug 10 2020 at 23:08):

Has anyone tied monads from the category theory library to monoids in the endofunctor category?

view this post on Zulip Simon Hudon (Aug 10 2020 at 23:14):

Yes, there is category_theory.monad.types where programming monads are shown to be monads in the category theory sense

view this post on Zulip Adam Topaz (Aug 10 2020 at 23:20):

Yes i saw that, but I'm wondering about the equivalence between docs#category_theory.monad and Mon_ (C \func C)

view this post on Zulip Adam Topaz (Aug 10 2020 at 23:22):

But anyway, morphisms of monads are "just" morphisms in Mon_ (C \func C)

view this post on Zulip Scott Morrison (Aug 11 2020 at 00:30):

@Adam Topaz, no, my comment above was precisely trying to goad someone into proving "oh, monads are just monoids in the category of endofunctors".

view this post on Zulip Adam Topaz (Aug 11 2020 at 00:38):

There should be an "nlab-just" tactic.

view this post on Zulip Scott Morrison (Aug 11 2020 at 00:46):

Quantisation, categorification, justification.

view this post on Zulip Adam Topaz (Aug 11 2020 at 03:47):

@Simon Hudon @Scott Morrison I wrote up some definitions for morphisms of functors and monads (in the sense of control.*) in the following two files:

https://github.com/leanprover-community/mathlib/blob/monad_morph/src/control/functor/morph.lean

https://github.com/leanprover-community/mathlib/blob/monad_morph/src/control/monad/morph.lean

These also contain some very basic lemmas. Let me know if it's worth opening a PR.

view this post on Zulip Simon Hudon (Aug 11 2020 at 03:52):

It looks like a nice start. Do you have examples where it is useful? That would be worth including too.

view this post on Zulip Adam Topaz (Aug 11 2020 at 04:00):

I'm interested in this because I'm planning to apply it in some algebraic contexts later, but this is much more involved. I guess one thing that's worth adding is the fact that there is an initial monad (the identity functor).

view this post on Zulip Simon Hudon (Aug 11 2020 at 04:04):

that's a nice example. You could also show that some monad transformers are monad morphisms

view this post on Zulip Simon Hudon (Aug 11 2020 at 04:05):

On terminology, maybe @Scott Morrison will correct me but we use _hom and not _morph to name morphisms.

view this post on Zulip Scott Morrison (Aug 11 2020 at 04:11):

Unless the additional universe flexibility is useful somewhere, why not just use the ones from category_theory/?

view this post on Zulip Scott Morrison (Aug 11 2020 at 04:13):

Actually, while we're on the subject of category_theory/ and control/, would it be insane to move functor in core into the control namespace?

view this post on Zulip Scott Morrison (Aug 11 2020 at 04:13):

I keep running into this name conflict over functor.map_comp.

view this post on Zulip Simon Hudon (Aug 11 2020 at 04:20):

I don't think that would be insane. We picked control because Haskell did but I'm starting to question the choice. If any kind of electrical engineering such as control theory gets into mathlib, that could be confusing. I'm wondering if we should just call it programming

view this post on Zulip Mario Carneiro (Aug 11 2020 at 04:32):

well, functional_programming

view this post on Zulip Mario Carneiro (Aug 11 2020 at 04:33):

however I think that worries about control theory are premature until we get some

view this post on Zulip Adam Topaz (Aug 11 2020 at 04:33):

I would like to use do notation as well. Do the monads in category_theory provide a functional_prpgramming.monad instance?

view this post on Zulip Simon Hudon (Aug 11 2020 at 04:37):

Mario Carneiro said:

however I think that worries about control theory are premature until we get some

That's probably true. I think it remains that it's not a great name for functional programming tools

view this post on Zulip Simon Hudon (Aug 11 2020 at 04:38):

Adam Topaz said:

I would like to use do notation as well. Do the monads in category_theory provide a functional_prpgramming.monad instance?

I don't believe so but it should be easy enough to create one

view this post on Zulip Mario Carneiro (Aug 11 2020 at 04:38):

having just diagnosed a typeclass loop, I am a bit worried about the contribution to the instance problem

view this post on Zulip Mario Carneiro (Aug 11 2020 at 04:39):

Can you derive an instance going the other way?

view this post on Zulip Adam Topaz (Aug 11 2020 at 04:47):

https://github.com/leanprover-community/mathlib/blob/43ceb3e01ef133d5c39a1f2793f092751a573ce9/src/category_theory/monad/types.lean

view this post on Zulip Chris Wong (Aug 11 2020 at 10:09):

We picked control because Haskell did but I'm starting to question the choice.

You can argue that the control / data distinction doesn't make much sense in Haskell either :stuck_out_tongue:

view this post on Zulip Reid Barton (Aug 11 2020 at 10:12):

what if we just use haskell

view this post on Zulip Scott Morrison (Aug 11 2020 at 10:14):

LGTM. :-)

view this post on Zulip Adam Topaz (Aug 11 2020 at 16:10):

@Scott Morrison @Simon Hudon I added some stuff about morphisms of monads in the sense of category theory, as well as the stuff around the initial monad in control.monad. I think the natural thing to do next is to define the category of monads in category_theory.monad.basic, but I'm not sure what would be the best way to go about this, since category_theory.monadis a typeclass. Any suggestions?

The changes from mathlib:master are here:
https://github.com/leanprover-community/mathlib/compare/monad_morph

view this post on Zulip Simon Hudon (Aug 11 2020 at 17:20):

Nice

view this post on Zulip Simon Hudon (Aug 11 2020 at 17:23):

Something that I would like to see in this PR is to show that state_t m defines a morphism between m and state_t m (same for reader_t and cont_t). It would also be cool to see state_t treated as a functor on monad morphisms (same for other transformers). Then, we can have a systematic way of transforming state_t m to state_t n

view this post on Zulip Adam Topaz (Aug 11 2020 at 17:23):

I can add that, but it's actually true for any monad transformer. Is there a class for monad transformers?

view this post on Zulip Simon Hudon (Aug 11 2020 at 17:24):

@Reid Barton I think this would be very honest. At the same time, I think we wouldn't want to create the expectation that we'd be perfectly faithful to Haskell whereas we should take liberties for a nicer formalization

view this post on Zulip Simon Hudon (Aug 11 2020 at 17:25):

Adam Topaz said:

I can add that, but it's actually true for any monad transformer. Is there a class for monad transformers?

There is monad_lift but it doesn't have laws. I have a version somewhere that adds the law if you want but it's not hard to come up with.

view this post on Zulip Adam Topaz (Aug 11 2020 at 17:35):

Oh, it looks like monad_lift is essentially a morphism of monads with no rules.

view this post on Zulip Adam Topaz (Aug 11 2020 at 17:38):

So perhaps it makes sense to unbundle the definition of a monad morphism, extending has_monad_lift, and just add the rules?

view this post on Zulip Reid Barton (Aug 11 2020 at 17:43):

How about bundling monads instead?

view this post on Zulip Adam Topaz (Aug 11 2020 at 17:44):

I would be happy with that. But I don't know about others :)

view this post on Zulip Adam Topaz (Aug 11 2020 at 17:48):

I think certainly the category_theory.monad could be bundled.

view this post on Zulip Adam Topaz (Aug 11 2020 at 17:50):

Well... it is already -- Mon_ (C \func C).

view this post on Zulip Adam Topaz (Aug 11 2020 at 22:55):

Okay, I made bundled monads Monad C and made it a category. Next up, "monads are just monoids in ...".

view this post on Zulip Adam Topaz (Aug 11 2020 at 22:59):

https://github.com/leanprover-community/mathlib/blob/578b4bf74169b9ec65dca05df84508950971b7e2/src/category_theory/monad/basic.lean#L156


Last updated: May 07 2021 at 19:12 UTC