Using ref in lean 4 (basic q)

Stream: lean4

[Thomas Murrills]

What's the analogue of Lean 3's tactic.ref in Lean 4? I looked in the analogous spot, but couldn't find it. (Also, whatever the analogue is, how should I then actually import/open the relevant files to use it?)

[Henrik Böving]

Several possiblities.

• If you wish to have local mutability use the let mut keyword in do notation
• If you wish to have monadic stuff (that is mutable variables shared across fucntion calls) you can start building your own monad stack with StateRefT or the underlying ST monad.
• You can also go very funky and use a global IO.Ref for example although this is most likely not what you want to do

[Mario Carneiro]

The direct analogue of tactic.ref is IO.Ref

[Mario Carneiro]

and you don't have to import anything, it's already in Init

[Thomas Murrills]

oh, ok! so does it make sense to use IO.Ref in tauto just as a drop-in replacement for ref? it’s not clear to me that IO is actually happening there, unless it’s managed internally or something… (Or would it make more sense to use a StateRefT type of deal there?)

[Mario Carneiro]

I think it's fine to use IO.Ref if you want to keep the structure of the original code

[Mario Carneiro]

StateRefT is basically the same thing, it uses ST.Ref instead of IO.Ref but there isn't much difference between these except the API

[Gabriel Ebner]

The direct analogue of tactic.ref is IO.Ref

This is not really true: the Lean 3 tactic.ref is reset when backtracking (it is stored in the tactic state), while the Lean 4 IO.Ref is an actual reference that exists independently of the tactic state (and thus won't be reset when backtracking).

open tactic
#eval using_new_ref 42 $ λ r, do
  (write_ref r 10 >> fail "") <|> skip,
  read_ref r >>= trace -- prints 42

[Mario Carneiro]

ah yeah, I ran into that issue when implementing squeeze_scope. I don't think there is any real analogue of tactic.ref that gets reset along with the tactic state

[Sébastien Michelland]

An environment extension maybe?

[Mario Carneiro]

That will probably work, but it also clutters up the olean file

[Sébastien Michelland]

Aren't normal extensions local to the current file unlike the persistent ones?

[Thomas Murrills]

should there be a direct analogue of tactic.ref? (I mean I’m guessing it’s above my pay grade right now, so to speak, and it’s probably not strictly necessary for tauto, but I’m still curious what it would take to code it up lean 4…being reset when backtracking in tactics seems useful)

[Gabriel Ebner]

I'd rather avoid it, and explicitly use StateT α TacticM instead (if you want a backtrackable state of type α).

[Thomas Murrills]

ah, ok. I’m guessing this is the “build your own monad stack with StateRefT” strategy mentioned by @Henrik Böving ? (Asking because I’m trying to figure out what the difference between using StateRefT vs. StateT is in this context; might be apparent as soon as I open the metaprogramming book, though… :) )

[Henrik Böving]

They behave equivalently to the user but one is a classic state monad pulling the state through as argument and return value while the other stores it as a real reference that gets mutated

[Gabriel Ebner]

They do not behave equivalently. It's kind of the same difference as between tactic.ref and IO.Ref.

• StateT does backtracking
• StateRefT does not

[Thomas Murrills]

Are there efficiency differences between using StateT and StateRefT/IO.ref? If I'm going to be managing a big state, I can imagine it might be better to use a reference instead of passing the whole state around. Then I would just try to work around the non-backtrackability. But I can also imagine that maybe, say, the internals of StateT make it just as efficient as using a reference.

[Henrik Böving]

StateRefT is generally speaking better if your monad stack allows for it.