lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

feat: `modifyM`/`modifyGetM` for `IO.Ref`

Open tydeu opened this issue 5 months ago • 4 comments

Adds IO.Ref.modfyM / IO.Ref.modifyGetM which are monadic variants of IO.Ref.modify (ST.Prim.Ref.modify) / IO.Ref.modifyGet (ST.Prim.Ref.modifyGet). Like them, it uses ST.Prim.Ref.take to atomically modify the reference via busy-waiting, but allow users to perform BaseIO actions within the critical section. This is safe because BaseIO / ST σ α actions do not throw exceptions. Without these utilities, to modify a reference while preforming I/O, one needs to use IO.Mutex. Thus, this provides a lightweight alternative for users.

The outstanding question here is whether this is good idea or if users should be expected to use IO.Mutex if they wish to modify a reference while performing I/O.

tydeu avatar Mar 09 '24 21:03 tydeu