Map of Lean's monads

Stream: lean4

[Adam Topaz]

I remember seeing a diagram some time ago describing the relationship between the various monads in lean4 core (CommandElabM, TermElabM, etc.). But I can't seem to find it right now. Does anyone have this handy? Is it still relevant?

[Wojciech Nawrocki]

Perhaps https://leanprover-community.github.io/lt2021/slides/leo-LT2021-meta.pdf ?

[Adam Topaz]

Yeah! That's it (on page 5)

[Adam Topaz]

Thanks!

[James Gallicchio]

Maybe that diagram should be added to the metaprogramming book :eyes:

[Scott Morrison]

We also need a "cheat sheet" of all the run functions that let you move the "unnatural" directions in the monad diagram, by providing the additional state manually.

[Mario Carneiro]

I made a zulip post about that a while ago

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.204.20monads/near/275880681

[Patrick Massot]

I just tried to do it:

\documentclass{standalone}
\usepackage{tikz}

\begin{document}
\begin{tikzpicture}[auto, scale=.5]
  \node (TacticM)      at (10, 0)   {TacticM};
  \node (TermElabM)    at (10, 5)   {TermElabM};
  \node (MetaM)        at (10,10)   {MetaM};
  \node (CoreM)        at (10, 15)  {CoreM};
  \node (EIO)          at (10, 20)  {EIO};
  \node (MacroM)       at (0,20) {MacroM};
  \node (UnexpandM)    at (0,15) {UnexpandM};
  \node (CommandElabM) at (30,5)   {CommandElabM};
  \node (IO)           at (20,20)  {IO};
  \node (SimpM)        at (0,10) {SimpM};
  \node (FrontendM)    at (30,20)  {FrontendM};

  \draw [->] (TacticM) to (TermElabM);
  \draw [->] (TermElabM) to (MetaM);
  \draw [->] (MetaM) to (CoreM);
  \draw [->] (CoreM) to (EIO);
  \draw [->, dashed, bend right, swap] (TermElabM) to node {Lean.Elab.Tactic.run} (TacticM);
  \draw [->, dashed, bend right, swap] (CoreM) to node {MetaM.run} (MetaM);
  \draw [->, dashed, bend right, swap] (EIO)   to node {CoreM.run} (CoreM);
  \draw [->, dashed] (CommandElabM) to node {runTermElabM} node[swap]{liftTermElabM} (TermElabM);
  \draw [->, dashed, sloped] (CommandElabM) to node {liftCoreM} (CoreM);
  \draw [->] (CommandElabM) to (EIO);
  \draw [->, dashed, sloped, swap, pos=.2] (IO) to node {MetaM.toIO} (MetaM);
  \draw [->, dashed, sloped, pos=0.35] (IO) to node {CoreM.toIO} (CoreM);
  \draw [->] (IO) to (EIO);
  \draw [->] (SimpM) to (MetaM);
  \draw [->, dashed] (FrontendM) to node {runCommandElabM} (CommandElabM);
  \draw [->] (FrontendM) to (IO);
\end{tikzpicture}
\end{document}

The result is monads.pdf. I used the same arrow direction convention as in Leo's slides but it does look a bit weird that MetaM.toIO goes from IO to MetaM for instance. Anyway, anyone should feel free to steal that code, improve it and put it somewhere useful.

[Scott Morrison]

I would definitely reverse the arrows! Then the solid arrows become "if you have X, you can freely use it when you need Y", while the dashed arrows are "you can turn X into Y, but only if you know what you're doing (=have appropriate state/context)".

[Mario Carneiro]

yeah, the base of the monad hierarchy should be the root of the tree

[Eric Wieser]

I started a wiki page at https://github.com/leanprover-community/mathlib4/wiki/Monad-map

[Eric Wieser]

@David Thrane Christiansen, @Henrik Böving: it would be great to have some support for text-based diagrams along these lines within the docs pages, though I imagine you have plenty of other more valuable docs improvements in mind as well

[Eric Wieser]

(bonus points if they can be generated from source code to ensure they stay up to date)

[Thomas Murrills]

This is great! I'll definitely be referring to this from time to time. :) Would it be ok to reverse the arrows though, for the reasons mentioned? (I can do the edit if it's helpful)

[Mario Carneiro]

There is a missing solid arrow from CoreM to IO

[Eric Wieser]

Feel free to edit: that was the reason for me making it a wiki page

[Thomas Murrills]

So, feel free to revert my edit if we don't like it, but:

I thought it would be a lot clearer if the map went from bottom to top, but mermaid doesn't currently support backwards arrows (which go against the overall direction of the graph without messing up the rankings). So, I sacrificed the arrows on the dotted lines, and explained that dotted lines going downward from B to A let you run A inside B. It's not perfect, but, tradeoffs.

I also added RequestM and DelabM, since those are pretty important. I also closed the loop for SimpM to show how you would actually use it while metaprogramming. There are of course a lot of even more niche monads which might not belong here, like MkBindingM—the diagram looks complex enough! :) So I put a note at the bottom explaining that SimpM was used as an example of those.

[Eric Wieser]

I'm confused by your comment about backwards arrows messing with the ranking; why didn't they cause the original version any issues?

[Eric Wieser]

Also, is Simp.M a typo?

[Thomas Murrills]

Eric Wieser said:

I'm confused by your comment about backwards arrows messing with the ranking; why didn't they cause the original version any issues?

Honestly, I don't know. But in the version right before I edited, there was no coherent ranking—IO was somewhere in the middle right, for example.

[Thomas Murrills]

Eric Wieser said:

Also, is Simp.M a typo?

Nope! We have SimpM and Simp.M. :upside_down:

[Thomas Murrills]

Re: ranking, this is what I see on the revision right before my edit. Is it the same for you?
image.png

[Thomas Murrills]

Maybe this is technically ok ranking-wise despite looking odd? But in any case, if you simply reverse all of those arrows (which I tried first), problems start to arise.

[Thomas Murrills]

If you can restore the arrowheads without changing the bottom-to-top flow though, please do, ofc! I couldn't get it to work even after a good deal of fiddling.

[Eric Wieser]

docs

Thomas Murrills said:

Eric Wieser said:

Also, is Simp.M a typo?

Nope! We have SimpM and Simp.M. :upside_down:

I say this because the link on the wiki doesn't go anywhere. Maybe docs#Simp.M works.