# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Morphisms of monads

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

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.

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

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

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`

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

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

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

I don't think so.

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

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

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

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

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 `M`

to `T M`

.

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

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

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

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

Oh wait, I misread.

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

#### Scott Morrison (Aug 10 2020 at 22:59):

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:

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.

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

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

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

#### Adam Topaz (Aug 11 2020 at 04:47):

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

#### Scott Morrison (Aug 11 2020 at 10:14):

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.monad`

is a typeclass. Any suggestions?

The changes from mathlib:master are here:

https://github.com/leanprover-community/mathlib/compare/monad_morph

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

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

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.

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

#### Reid Barton (Aug 11 2020 at 17:43):

How about bundling monads instead?

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

#### Adam Topaz (Aug 11 2020 at 22:59):

Last updated: May 07 2021 at 19:12 UTC