## Stream: Is there code for X?

#### Adam Topaz (Aug 10 2020 at 18:10):

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

#### 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?

#### Adam Topaz (Aug 10 2020 at 18:37):

Either would be fine. Since this exists:

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

#### Adam Topaz (Aug 10 2020 at 18:40):

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

#### 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?

#### 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

#### 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).

#### Simon Hudon (Aug 10 2020 at 19:25):

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

#### Adam Topaz (Aug 10 2020 at 19:25):

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

#### Adam Topaz (Aug 10 2020 at 19:26):

I'll try to sketch a definition.

#### Adam Topaz (Aug 10 2020 at 19:39):

Something like this:

variables (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?

Looks good to me

#### Adam Topaz (Aug 10 2020 at 19:42):

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

#### 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

#### Adam Topaz (Aug 10 2020 at 20:15):

I don't think so.

#### Mario Carneiro (Aug 10 2020 at 20:16):

isn't that what's happening here?

#### Mario Carneiro (Aug 10 2020 at 20:16):

you take elements of one monad and produce elements of another

Not quite.

#### 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

#### 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.

Or something.

#### 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

#### Adam Topaz (Aug 10 2020 at 20:20):

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

#### Adam Topaz (Aug 10 2020 at 20:59):

Is there some standard haskelish ascii art for natural transformations?

#### Adam Topaz (Aug 10 2020 at 21:02):

~> I guess.

#### 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.

Just saying. :-)

#### Adam Topaz (Aug 10 2020 at 23:08):

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

#### 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

#### 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)

#### Adam Topaz (Aug 10 2020 at 23:22):

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

#### 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".

#### Adam Topaz (Aug 11 2020 at 00:38):

There should be an "nlab-just" tactic.

#### Scott Morrison (Aug 11 2020 at 00:46):

Quantisation, categorification, justification.

#### 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:

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

#### 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.

#### 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).

#### Simon Hudon (Aug 11 2020 at 04:04):

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

#### 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.

#### 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/?

#### 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?

#### Scott Morrison (Aug 11 2020 at 04:13):

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

#### 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

#### Mario Carneiro (Aug 11 2020 at 04:32):

well, functional_programming

#### Mario Carneiro (Aug 11 2020 at 04:33):

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

#### 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?

#### 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

#### Simon Hudon (Aug 11 2020 at 04:38):

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

#### 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

#### Mario Carneiro (Aug 11 2020 at 04:39):

Can you derive an instance going the other way?

#### 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:

#### Reid Barton (Aug 11 2020 at 10:12):

what if we just use haskell

LGTM. :-)

#### 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:

Nice

#### 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

#### 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?

#### 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

#### Simon Hudon (Aug 11 2020 at 17:25):

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.

#### Adam Topaz (Aug 11 2020 at 17:35):

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

#### 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?

#### Adam Topaz (Aug 11 2020 at 17:44):

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

#### Adam Topaz (Aug 11 2020 at 17:48):

I think certainly the category_theory.monad could be bundled.

#### Adam Topaz (Aug 11 2020 at 17:50):

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

#### 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 ...".