Monad map

A solid arrow upwards from A to B means "when in the A Monad, anything in B can be called directly", i.e. there is a lift from B to A. (If this arrow is labeled, you must call that function to do so.)

A dotted line downwards from B to A means that you can call a function (possibly with some extra arguments, such as initial state) to run B inside A. Note that many of these functions have apostrophe variants (e.g. TermElabM.run and TermElabM.run'): run typically returns the final state of the monad that we're running inside the other monad along with the actual return value, whereas run' simply discards it.

This diagram is ordered from bottom to top, with simpler monads at the bottom and more complex ones at the top. As such, lifts go up, and run-like functions go down.

graph BT
  TacticM
  TermElabM
  MetaM
  CoreM
  EIO
  IO
  RequestM
  DelabM
  IO
  BaseIO
  CommandElabM
  SimpM
  Simp.M
  FrontendM

  TermElabM --> TacticM;
  CoreM --> MetaM;
  IO --> FrontendM & CommandElabM & RequestM;
  MetaM -. TermElabM.run ..- TermElabM;
  MetaM --> TermElabM;
  MetaM --> DelabM;
  MetaM -. Lean.PrettyPrinter.delab .- DelabM;
  MetaM --> SimpM --> Simp.M;
  IO -. TermElabM.toIO .- TermElabM;
  BaseIO --> IO;
  BaseIO -. EIO.toBaseIO .- EIO;
  BaseIO --> EIO;
  EIO -. IO.toEIO .- IO
  EIO -. EIO.toIO .-> IO
  IO --> CoreM;
  IO -. CoreM.toIO .- CoreM;
  IO -. MetaM.toIO .- MetaM;
  EIO -. CoreM.run .- CoreM;
  MetaM -. StateRefT'.run .- Simp.M;
  TermElabM -. Lean.Elab.Tactic.run .- TacticM;
  CoreM -. MetaM.run .- MetaM;
  RequestM -. runCommandElabM .- CommandElabM;
  RequestM -. runTermElabM .- TermElabM;
  CommandElabM -.-|runTermElabM, liftTermElabM| TermElabM;
  FrontendM -. runCommandElabM .- CommandElabM;
  RequestM -. runCoreM .- CoreM;
  CommandElabM -. liftCoreM .- CoreM;

  click TacticM href "https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Elab.Tactic.TacticM" _blank
  click TermElabM href "https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Elab.Term.TermElabM" _blank
  click MetaM href "https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Meta.MetaM" _blank
  click CoreM href "https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Core.CoreM" _blank
  click EIO href "https://leanprover-community.github.io/mathlib4_docs/search?q=EIO" _blank
  click IO href "https://leanprover-community.github.io/mathlib4_docs/search?q=IO" _blank
  click RequestM href "https://leanprover-community.github.io/mathlib4_docs/search?q=RequestM" _blank
  click DelabM href "https://leanprover-community.github.io/mathlib4_docs/search?q=DelabM" _blank
  click IO href "https://leanprover-community.github.io/mathlib4_docs/search?q=IO" _blank
  click BaseIO href "https://leanprover-community.github.io/mathlib4_docs/search?q=BaseIO" _blank
  click CommandElabM href "https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Elab.Command.CommandElabM" _blank
  click SimpM href "https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Meta.Simp.SimpM" _blank
  click Simp.M href "https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Meta.Simp.Simp.M" _blank
  click FrontendM href "https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Elab.Frontend.FrontendM" _blank

Loading

Note that IO and EIO are taken to each other by the functions IO.toEIO and EIO.toIO, neither of which is a lift, so in this case, the top-to-bottom directionality of dotted lines isn't meaningful.

Many application-specific monads are defined in terms of monad transformers on top of typical metaprogramming monads; for example, in addition to Simp.M, we have SimpAll.M, and many others. Instead of having dedicated functions to return to the monad they're defined on top of, many of these simply use the function given by the monad transformer, e.g. StateRefT'.run for Simp.M to return to the MetaM monad it is built on top of. Simp.M is given here as an example.