custom monad advice for meta-programming

Stream: general

[Jason Rute]

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]

Yes, you can do similar tricks as in haskell monad transformers

[Jason Rute]

Pretend I don't know Haskell.

[Jason Rute]

(I know Scala, Lean, and some OCaml.)

[Mario Carneiro]

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]

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]

Ok, that is probably a good place to start. Thanks!

[Mario Carneiro]

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]

Also, how do you call a regular tactic inside this ring tactic (like in a do block)?

[Jason Rute]

Do you just construct the obvious conversion function tac_to_ring and wrap your tactics with that?

[Mario Carneiro]

monad transformers usually come with an operation called lift of type inner_monad A -> transformed_monad A

[Mario Carneiro]

meta def lift {α} (m : tactic α) : ring_m α := reader_t.lift (state_t.lift m)

[Mario Carneiro]

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]

otherwise you can just use state_t.lift directly

[Mario Carneiro]

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]

By "not hiding it", do you mean writing functions with signature def foo : reader_t cache (state_t (buffer expr) tactic) α?

[Mario Carneiro]

yes

[Mario Carneiro]

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]

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]

Care to explain mutable variables? (Or point the way to an explanation.)

[Mario Carneiro]

It's a pretty simple api, see #print ref and go to definition

[Jason Rute]

Will do. Thanks for all this!

[Mario Carneiro]

inside the tactic monad you can create (scoped) mutable variables and modify them

[Scott Morrison]

Oh, I never knew about this ref thing!

[Gabriel Ebner]

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.