-
Notifications
You must be signed in to change notification settings - Fork 313
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["<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;
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;
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.