Procedural programming with arrays

Stream: lean4

[Kind Bubble]

I thought I read somewhere that Arrays in Lean 4 are mutable. What does this entail on the front and back end?

[Henrik Böving]

Arrays in Lean will be optimized to be accessed in a mutable way if you use them in a linear fashion, that is there is only ever one reference to them at a time at runtime.

That being said I don't quite understand your question, do you want to know how its implemented?

[Jason Rute]

This paper explains the implementation if I understand correctly. https://arxiv.org/pdf/1908.05647.pdf

[Jason Rute]

I don't know if arrays are particularly special, or if this generally falls under the "destructive updates" pattern. Various slides by the developers (e.g. http://leanprover.github.io/talks/NFM2022.pdf) summarizes it as:

Runtime uses reference counting for GC, and performs destructive updates if RC = 1

[Sebastian Ullrich]

Arrays are special in the sense that destructive updates are triggered by runtime primitives (think Array.push), not heuristic optimizations

[Sebastian Ullrich]

See §7.1

[Kind Bubble]

Thanks, this is good info. I think I'll have to keep this understanding for several months into the future since I'm just getting used to the basics.