What is ST.Ref.take?

Stream: lean4

[Yicheng Qian]

Just a question out of curiosity, what is ST.Ref.take (or ST.Prim.ref.take)?
I was trying to understand ST.Ref. I guess that ST.Ref.get is similar to Haskell readSTRef (but also lifts from ST to other monads), ST.Ref.set is similar to Haskell writeSTRef and ST.Ref.swap (a:α) swaps the value in the ST.Ref with a. However, I have no idea what is ST.Prim.take.

[Sebastian Ullrich]

take moves the value out of the ref, leaving the ref in a temporarily invalid state (so don't get it in that state). You can it being used in modifyUnsafe to make sure that the value is being used linearly.

[Yicheng Qian]

Thanks for the explanation. I can see that Lean crashes if I first take then get or take. But I can't understand what "being used linearly" stands for.

[Sebastian Ullrich]

If the ref has a unique reference to the contained value, you want to pass that reference uniquely to f as well in order to enable destructive updates (see "Counting Immutable Beans")

[Gabriel Ebner]

leaving the ref in a temporarily invalid state

Just fyi, if you call get in this temporary state after take, then it will busy-wait until you call set again.

[Sebastian Ullrich]

That's what I assumed as well from memory, but it's not actually true in the single-threaded case (in which case waiting wouldn't make much sense either of course)! Which I guess is the reason it's unsafe.

[Mario Carneiro]

what does it do?

[Sebastian Ullrich]

It gives you back an actual nullptr, which will probably break something else down the line (or immediately on inc(nullptr))

[Mario Carneiro]

oh yikes

[Sebastian Ullrich]

It would probably be better to just hard-panic (which is already the case in a debug build) and remove the unsafe