Skip to content

Monad map

Jump to bottom
Eric Wieser edited this page Oct 22, 2024 · 18 revisions

A solid arrow left 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 right 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 left to right, with simpler monads at the left and more complex ones at the right. As such, lifts go right, and run-like functions go left.

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;
  EIO -. "<a href='https://leanprover-community.github.io/mathlib4_docs/Init/System/IO.html#IO.toEIO'>IO.toEIO</a>" .- IO
  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

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 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 CommmandElabM (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