Skip to content

Monad map

Jump to bottom
Evgenia Karunus edited this page Apr 9, 2025 · 20 revisions 
graph LR
  TacticM["<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Tactic/Basic.html#Lean.Elab.Tactic.TacticM'>TacticM</a>"]
  TermElabM["<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Term.html#Lean.Elab.Term.TermElabM'>TermElabM</a>"]
  MetaM["<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Basic.html#Lean.Meta.MetaM'>MetaM</a>
"]
  CoreM["<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/CoreM.html#Lean.Core.CoreM'>CoreM</a>
"]
  EIO["<a href='https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#EIO'>EIO</a>"]
  IO["<a href='https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#IO'>IO</a>"]
  RequestM["<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Server/Requests.html#Lean.Server.RequestM'>RequestM</a>"]
  DelabM["<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/PrettyPrinter/Delaborator/Basic.html#Lean.PrettyPrinter.Delaborator.DelabM'>DelabM</a>"]
  BaseIO["<a href='https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#BaseIO'>BaseIO</a>"]
  CommandElabM["<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Command.html#Lean.Elab.Command.CommandElabM'>CommandElabM</a>"]
  SimpM["<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Tactic/Simp/Types.html#Lean.Meta.Simp.SimpM'>SimpM</a>"]
  FrontendM["<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Frontend.html#Lean.Elab.Frontend.FrontendM'>FrontendM</a>"]

  TermElabM ==> TacticM;
  CoreM ==> MetaM;
  IO ==> FrontendM & CommandElabM & RequestM;
  MetaM -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Term.html#Lean.Elab.Term.TermElabM.run'>TermElabM.run</a>" ..- TermElabM;
  MetaM ==> TermElabM;
  MetaM ==> DelabM;
  MetaM -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/PrettyPrinter/Delaborator/Basic.html#Lean.PrettyPrinter.delab'>PrettyPrinter.delab</a>" .- DelabM;
  MetaM ==> SimpM;
  IO -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Term.html#Lean.Elab.Term.TermElabM.toIO'>TermElabM.toIO</a>" .- TermElabM;
  BaseIO ==> IO;
  BaseIO -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#EIO.toBaseIO'>EIO.toBaseIO</a>" .- EIO;
  BaseIO ==> EIO;
  IO -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#IO.toEIO'>IO.toEIO</a>" .- EIO
  EIO -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#EIO.toIO'>EIO.toIO</a>" .- IO
  IO ==> CoreM;
  IO -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/CoreM.html#Lean.Core.CoreM.toIO'>CoreM.toIO</a>" .- CoreM;
  IO -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Basic.html#Lean.Meta.MetaM.toIO'>MetaM.toIO</a>" .- MetaM;
  EIO -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/CoreM.html#Lean.Core.CoreM.run'>CoreM.run</a>" .- CoreM;
  MetaM -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Init/Control/StateRef.html#StateRefT'.run'>StateRefT'.run</a>" .- SimpM;
  TermElabM -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Tactic/Basic.html#Lean.Elab.Tactic.run'>Tactic.run</a>" .- TacticM;
  CoreM -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/Basic.html#Lean.Meta.MetaM.run'>MetaM.run</a>" .- MetaM;
  RequestM -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Server/Requests.html#Lean.Server.RequestM.runCommandElabM'>RequestM.runCommandElabM</a>" .- CommandElabM;
  RequestM -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Server/Requests.html#Lean.Server.RequestM.runTermElabM'>RequestM.runTermElabM</a>" .- TermElabM;
  CommandElabM -.-|"<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Command.html#Lean.Elab.Command.runTermElabM'>runTermElabM</a>, <a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Command.html#Lean.Elab.Command.liftTermElabM'>liftTermElabM</a>"| TermElabM;
  FrontendM -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Frontend.html#Lean.Elab.Frontend.runCommandElabM'>Frontend.runCommandElabM</a>" .- CommandElabM;
  RequestM -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Server/Requests.html#Lean.Server.RequestM.runCoreM'>RequestM.runCoreM</a>" .- CoreM;
  CommandElabM -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Command.html#Lean.Elab.Command.liftCoreM'>liftCoreM</a>" .- CoreM;
  CoreM -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Command.html#Lean.liftCommandElabM'>liftCommandElabM</a>" .- CommandElabM;
Loading

This diagram is ordered from left to right, with simpler monads on the left, and more complex monads on the right.

In this diagram, you see bold lines and dotted lines. The direction of the dotted lines is correct, however you should mentally reverse the direction of the bold lines (we cannot easily reverse them in the diagram because of the mermaid graph limitations!).

  • A bold arrow between LEFT and RIGHT means "when in the RIGHT monad, anything in LEFT can be called directly", i.e. there is a lift from LEFT to RIGHT.
  • A dotted line from LEFT to RIGHT means you can call a function (possibly with some extra arguments, such as initial state) to run RIGHT inside of LEFT. 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.

Many application-specific monads are defined in terms of monad transformers on top of typical metaprogramming monads; for example, in addition to SimpM, we have SimpAll.M, and many others. Instead of having dedicated functions to run in 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 SimpM to return to the MetaM monad. SimpM is given here as an example.

Note that runTermElabM and liftTermElabM both turn a TermElabM into a CommandElabM (and neither is a MonadLift). The difference is that runTermElabM allows the TermElabM computation to act on any scoped free variables (introduced by the variable command), whereas liftTermElabM doesn't. As a mnemonic: the run lets us specify some part of the "initial state" for the monad computation (like e.g. StateT.run), whereas the lift (as usual) doesn't.

Clone this wiki locally