Mutable variables with dependent types

Stream: new members

[Evgeny Kurnevsky]

Hi. Is it possible to assign mutable variables with dependent types inside a do notation? Here is an example what I'm trying to do:

def f := Id.run do
  let mut ⟨x₁, x₂, prop⟩: Σ' x y: Nat, x = y := ⟨1, 1, rfl⟩
  repeat
    ⟨x₁, x₂, prop⟩ := ⟨x₁.succ, x₂.succ, Nat.succ_inj'.mpr prop⟩
    if x₁ > 5 then
      break
  return x₁

It doesn't compile because of some type mismatch. Maybe I just miss some part of lean syntax? :)

It works if I assign them into a single variable like:

def f := Id.run do
  let mut x: Σ' x y: Nat, x = y := ⟨1, 1, rfl⟩
  repeat
    x := ⟨x.fst.succ, x.snd.fst.succ, Nat.succ_inj'.mpr x.snd.snd⟩
    if x.fst > 5 then
      break
  return x.fst

It's less readable.

[Chris Bailey]

Will you settle for this:

def f := Id.run do
  let mut psig@⟨x₁, x₂, prop⟩: Σ' x y: Nat, x = y := ⟨1, 1, rfl⟩
  repeat
    psig := ⟨x₁.succ, x₂.succ, Nat.succ_inj'.mpr prop⟩
    if x₁ > 5 then
      break
  return x₁

[Chris Bailey]

Oh boy, that makes a really subtle change to the evaluation.

[Evgeny Kurnevsky]

Yeah, unfortunately it doesn't change x₁ outside the loop, otherwise it would look good :)

[Evgeny Kurnevsky]

And if I change it to

def f := Id.run do
  let mut psig@⟨x₁, x₂, prop⟩: Σ' x y: Nat, x = y := ⟨1, 1, rfl⟩
  repeat
    psig := ⟨x₁.succ, x₂.succ, Nat.succ_inj'.mpr prop⟩
    if x₁ > 5 then
      break
  return psig.fst

it just gets stuck in the loop :)

[Chris Bailey]

Yeah that behavior of the @- binding is rough. I would almost prefer that use of pattern bindings to be prohibited if it's going to create a second copy of the underlying value behind the scenes.

[Eric Wieser]

I think I saw a proposal somewhere to force pattern bindings to be spelt with have instead