Morphisms of monads

Stream: Is there code for X?

[Adam Topaz]

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

[Simon Hudon]

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]

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]

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

[Simon Hudon]

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

[Simon Hudon]

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]

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]

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

[Adam Topaz]

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

[Adam Topaz]

I'll try to sketch a definition.

[Adam Topaz]

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]

Looks good to me

[Adam Topaz]

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

[Simon Hudon]

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

[Mario Carneiro]

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

[Adam Topaz]

I don't think so.

[Adam Topaz]

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

[Mario Carneiro]

isn't that what's happening here?

[Mario Carneiro]

you take elements of one monad and produce elements of another

[Adam Topaz]

Not quite.

[Reid Barton]

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

[Adam Topaz]

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.

[Adam Topaz]

Or something.

[Simon Hudon]

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]

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]

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

[Adam Topaz]

Oh wait, I misread.

[Adam Topaz]

Is there some standard haskelish ascii art for natural transformations?

[Adam Topaz]

~> I guess.

[Scott Morrison]

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]

Just saying. :-)

[Adam Topaz]

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

[Simon Hudon]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Scott Morrison]

@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]

There should be an "nlab-just" tactic.

[Scott Morrison]

Quantisation, categorification, justification.

[Adam Topaz]

@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]

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

[Adam Topaz]

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]

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

[Simon Hudon]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Simon Hudon]

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]

well, functional_programming

[Mario Carneiro]

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

[Adam Topaz]

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

[Simon Hudon]

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]

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]

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

[Mario Carneiro]

Can you derive an instance going the other way?

[Adam Topaz]

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

[Chris Wong]

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]

what if we just use haskell

[Scott Morrison]

LGTM. :-)

[Adam Topaz]

@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

[Simon Hudon]

Nice

[Simon Hudon]

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]

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

[Simon Hudon]

@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]

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]

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

[Adam Topaz]

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

[Reid Barton]

How about bundling monads instead?

[Adam Topaz]

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

[Adam Topaz]

I think certainly the category_theory.monad could be bundled.

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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