Unnecessary Inhabited constraint on Array.modified

Stream: lean4

[Jannis Limperg]

Array.modify is currently implemented in terms of Array.modifyM, which induces an Inhabited constraint. I don't really understand why this constraint is necessary for modifyM, but it's certainly unnecessary for modify. Would you take a PR that reimplements modify to remove the constraint?

[Sebastian Ullrich]

Jannis Limperg said:

I don't really understand why this constraint is necessary for modifyM

Try removing it :) . It is necessary to ensure that v is used linearly, at least without resorting to unsafe code.

[Leonardo de Moura]

It is necessary to ensure that v is used linearly, at least without resorting to unsafe code.

Correct.

BTW, there are few modifications planned for this code.

• Consistent use of panic, ! suffix, and safe versions (based on @Andrew Kent and @Joe Hendrix feedback). That is, we will split the modify functions into modify! (takes Nat and panics) and modify (takes Fin)
• Add unsafe get that borrows the array content.
• Use previous unsafe get for implementing non-monadic modify

[Jannis Limperg]

I see, thanks! In that case, I (or rather my BSc student) will work with the current API for now.

[Andrew Kent]

Sebastian Ullrich said:

Jannis Limperg said:

I don't really understand why this constraint is necessary for modifyM

Try removing it :) . It is necessary to ensure that v is used linearly, at least without resorting to unsafe code.

This is quite interesting. Has there already been debate for/against there being an Array.modify primitive that is linear without requiring Inhabited? I feel like for the "unsafe" version (i.e., modify!) it is obviously not of an issue because the inhabited constraint is already their for type system soundness, but if the index is provably valid, it would be neat if you could update-and-replace the value. Morally the element type doesn't _need_ to be inhabited it feels like anyway.

[Andrew Kent]

I think I'm essentially asking if it makes more sense for modify to be the underlying array primitive for changing/setting values in an Array instead of set, since the former can express the latter and gives us linearity "for free".

[Sebastian Ullrich]

modify would not be a good primitive since we can't specialize away the closure over language boundaries