Skip to content

Monad map

Jump to bottom
thorimur edited this page Mar 8, 2024 · 15 revisions

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["<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;
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