Zulip Chat Archive
Stream: general
Topic: custom monad advice for meta-programming
Jason Rute (May 15 2020 at 04:26):
I'm constructing a fairly complicated tactic with a lot of parts which I've broken into many separate tactic-valued functions. I also need to pass around certain information a lot. This is a sort of "state", but not the tactic state. I happen to call it search_state
. I find myself writing a lot of tactics of the form:
meta def foo (s : tactic search_state) : tactic (output × search_state) := do
...
return (o, new_s)
for various output
types. Clearly, I should just make my own monad, new_monad
and then everything is cleaner:
meta def foo : new_monad output := do
...
some tactic which changes the `search_state`,
...
return o
Last, I'd like new_monad
to be able to (fairly easily) call regular tactic
monads.
I could hack through this ("type sudoku" if you will), but is there a tried-and-true approach to doing this (i.e. creating a new state monad on top of the tactic monad that plays nicely with the tactic monad)?
Mario Carneiro (May 15 2020 at 04:28):
Yes, you can do similar tricks as in haskell monad transformers
Jason Rute (May 15 2020 at 04:28):
Pretend I don't know Haskell.
Jason Rute (May 15 2020 at 04:28):
(I know Scala, Lean, and some OCaml.)
Mario Carneiro (May 15 2020 at 04:29):
Here is an example from the ring
tactic:
@[derive [monad, alternative]]
meta def ring_m (α : Type) : Type :=
reader_t cache (state_t (buffer expr) tactic) α
Mario Carneiro (May 15 2020 at 04:30):
This is augmenting the tactic monad with a state monad transformer (so you can modify an object of type buffer expr
) and a reader monad transformer (so any tactic gets read only access to an object of type cache
)
Jason Rute (May 15 2020 at 04:31):
Ok, that is probably a good place to start. Thanks!
Mario Carneiro (May 15 2020 at 04:31):
concretely, this means that a ring_m A
is actually a cache -> buffer expr -> tactic (buffer expr x A)
, but using monad transformers means that you get the monad operations for free
Jason Rute (May 15 2020 at 04:32):
Also, how do you call a regular tactic inside this ring tactic (like in a do
block)?
Jason Rute (May 15 2020 at 04:33):
Do you just construct the obvious conversion function tac_to_ring
and wrap your tactics with that?
Mario Carneiro (May 15 2020 at 04:33):
monad transformers usually come with an operation called lift
of type inner_monad A -> transformed_monad A
Mario Carneiro (May 15 2020 at 04:33):
meta def lift {α} (m : tactic α) : ring_m α := reader_t.lift (state_t.lift m)
Mario Carneiro (May 15 2020 at 04:34):
you don't need to define these functions unless you hide the definition of the transformer stack behind a definition like ring_m
here
Mario Carneiro (May 15 2020 at 04:35):
otherwise you can just use state_t.lift
directly
Mario Carneiro (May 15 2020 at 04:36):
You can also declare lift
to be a coercion, and then you can write regular tactics in a do
block for the transformed monad without any notation
Jason Rute (May 15 2020 at 04:37):
By "not hiding it", do you mean writing functions with signature def foo : reader_t cache (state_t (buffer expr) tactic) α
?
Mario Carneiro (May 15 2020 at 04:37):
yes
Mario Carneiro (May 15 2020 at 04:37):
If it's just one state_t
this is reasonable, but once you stack more than one I would suggest making a definition
Mario Carneiro (May 15 2020 at 04:39):
Also, you might consider whether a mutable variable of type ref search_state
is better than threading the state through everything using the state monad
Jason Rute (May 15 2020 at 04:40):
Care to explain mutable variables? (Or point the way to an explanation.)
Mario Carneiro (May 15 2020 at 04:41):
It's a pretty simple api, see #print ref
and go to definition
Jason Rute (May 15 2020 at 04:41):
Will do. Thanks for all this!
Mario Carneiro (May 15 2020 at 04:41):
inside the tactic monad you can create (scoped) mutable variables and modify them
Scott Morrison (May 15 2020 at 04:49):
Oh, I never knew about this ref
thing!
Gabriel Ebner (May 15 2020 at 07:51):
One important thing to note about ref
is that it is tied to the tactic state (the tactic state contains a map storing the values of the ref
variables). Backtracking (<|>
) hence also backtracks the state of the ref
variable. So they are not really mutable variables in the sense you may be used to.
Last updated: Dec 20 2023 at 11:08 UTC