Skip to content

Monad map

Jump to bottom
thorimur edited this page Oct 22, 2023 · 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/search?q=Lean.Elab.Tactic.TacticM'>TacticM</a>"]
  TermElabM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Elab.Term.TermElabM'>TermElabM</a>"]
  MetaM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Meta.MetaM'>MetaM</a>"]
  CoreM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Core.CoreM'>CoreM</a>"]
  EIO["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=EIO'>EIO</a>"]
  IO["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=IO'>IO</a>"]
  RequestM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=RequestM'>RequestM</a>"]
  DelabM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=DelabM'>DelabM</a>"]
  IO["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=IO'>IO</a>"]
  BaseIO["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=BaseIO'>BaseIO</a>"]
  CommandElabM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Elab.Command.CommandElabM'>CommandElabM</a>"]
  SimpM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Meta.Simp.SimpM'>SimpM</a>"]
  Simp.M["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Meta.Simp.Simp.M'>Simp.M</a>"]
  FrontendM["<a href='https://leanprover-community.github.io/mathlib4_docs/search?q=Lean.Elab.Frontend.FrontendM'>FrontendM</a>"]


  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;
  IO -. IO.toEIO .-> EIO
  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;
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.

Clone this wiki locally