Zulip Chat Archive

Stream: lean4

Topic: Lean 4 monads

Arthur Paulino (Mar 19 2022 at 00:49):

Page 5 of https://leanprover-community.github.io/lt2021/slides/leo-LT2021-meta.pdf has the following diagram:
image.png

I have some questions about it:

What do those arrows really mean? I don't see a direct relationship between CommandElabM and TermElabM and still it's possible to perform computations in the later from the former through liftTermElabM
Are there more "transitions" available like the one mentioned in the previous question?

Mario Carneiro (Mar 19 2022 at 00:56):

The arrows represent "lifts"; this means that you can use a value in a lower monad in a higher monad with no notation (or with liftM if you want to be explicit or coercion doesn't work)

Mario Carneiro (Mar 19 2022 at 00:57):

If we draw arrows whenever one monad can run another a la liftTermElabM, then there are generally arrows going in the reverse direction of all present

Arthur Paulino (Mar 19 2022 at 00:59):

What do you mean by "lower" monad in the diagram? Literally the vertical orientation of the image?
(thus TacticM is lower than TermElabM?)

Mario Carneiro (Mar 19 2022 at 01:00):

sorry, I mean upward in the diagram

Mario Carneiro (Mar 19 2022 at 01:00):

lower in the dependency hierarchy, more or less

Arthur Paulino (Mar 19 2022 at 01:01):

How is it possible to lift from CommandElabM to TermElabM if there's no path between them in the diagram (not even if we invert all arrows)?

Mario Carneiro (Mar 19 2022 at 01:01):

each arrow is a monad stack on top of the lower one, using StateT and ReaderT to add some read-write and read-only state respectively (conventionally called State and Context in the relevant namespace)

Mario Carneiro (Mar 19 2022 at 01:02):

Inverting an arrow is saying that for example you can run a MetaM from an IO context; however you have to provide the Meta.Context and Meta.State types to kick it off

Mario Carneiro (Mar 19 2022 at 01:03):

most of the arrows that cross the figure like liftTermElabM do this by conjuring up some dummy state to operate on

Mario Carneiro (Mar 19 2022 at 01:04):

for example if you are in a CommandElabM and want to run a TacticM you need to invent some trivial goal to work on, because the tactic wants a tactic state