Modifying `let mut` variables in `let`-bound functions

Stream: lean4

[Rish Vaishnav]

Is there a way to modify mutable values in let functions? For example, this doesn't work:

def test : IO Unit := do
  let mut n : Nat := 0
  let mut m : Nat := 0
  let f := do
    n := n + m -- `n` cannot be mutated ...
    m := n + 1 -- (edit: should use the old value of `n`, but you get the idea...)
  f ; f ; f ; f
  IO.println (n, m)

If not, is there a better way around it than this:

def test : IO Unit := do
  let mut n : Nat := 0
  let mut m : Nat := 0
  let f n m := do
    pure (n + m, n + 1)
  (n, m) ← f n m ; (n, m) ← f n m
  (n, m) ← f n m ; (n, m) ← f n m
  IO.println (n, m)

#eval test
-- (4, 3)

This considerably less readable, firstly because it's not clear which variables are being reassigned in f, and secondly because the calls to f are more complex.

[Kyle Miller]

No, mut variables are only modifiable within a "contiguous" do block. Functions get in the way of the transformation that mut needs to do.

[Henrik Böving]

The feature you are looking for here would be dangerous. f as a closure can be sent anywhere (including the return value of the function) so it would allow for some spooky mutations instead of only having local mutability only.

[Kyle Miller]

Something you can do is explicitly use StateT yourself, which is essentially what mut does for you.

[Kyle Miller]

Or you could potentially use IO.ref

[Kyle Miller]

(Henrik, that might be true, but it's also not a "the language is protecting you" limitation like your comment might lead someone to believe. It's a limitation of how the mut desugaring works, if I understand correctly, but of course what you say is a reason to not try to remove this limitation.)

[Henrik Böving]

Well it is not only a limitation. It would require local variables from the function to be kept around as mutable values within the context of the closure which is impossible without something like IO.Ref so I would say it's a very inherent limitation of what is possible.

[Kyle Miller]

"It's not only a limitation because it's a real big limitation"? ;-)

[Kyle Miller]

Here's StateT, quickly written, could be nicer:

structure MyState where
  n : Nat := 0
  m : Nat := 0

def test' : StateT MyState IO Unit := do
  let f := do
    modify fun s =>
      { s with n := s.n + s.m, m := s.n + 1}
  f ; f ; f ; f
  IO.println ((← get).n, (← get).m)

def test : IO Unit := test'.run' {}

[Kyle Miller]

There's also this, which is something you might be expected to do instead:

def test : IO Unit := do
  let mut n : Nat := 0
  let mut m : Nat := 0
  for _ in [0:4] do
    n := n + m
    m := n + 1
  IO.println (n, m)

[Rish Vaishnav]

I see, so it is possible with some additional state it seems. In fact, that seems closer to my original intent, since in writing test I assumed that n and m would be assigned in parallel, which of course isn't the case -- so the loop version isn't equivalent (but that's on me). Though it does make me wonder if some kind of metaprogramming could make the state machinery a bit less obtrusive.

[Rish Vaishnav]

(In fact, a loop would actually work in the specific case that I'm dealing with, so thank you for pointing me towards what should have been obvious :joy:)

[Kyle Miller]

For simultaneous update, you can do

def test : IO Unit := do
  let mut n : Nat := 0
  let mut m : Nat := 0
  for _ in [0:4] do
    (n, m) := (n + m, n + 1)
  IO.println (n, m)

[Kyle Miller]

so it is possible with some additional state it seems

Just to be clear, the StateT transformation I did is essentially what the mut variables are hiding — the transformation already exists to some degree. The issue is that the transformation would also need to transform the type of f, changing the return type from IO Unit to something that includes the variable state.

This doesn't seem impossible, but it would take some design work. Imagine how surprising it would be if updating m or n from within f automatically changes the type of f!

[Rish Vaishnav]

Oh okay, yes, thank you I understand the issue much better now. Though, I must say that I think that I am willing to accept that suprise if that means I don't have to define my own state.