The array/tuple question was never meant to be a long running thing. And as it often happens, the solution was right there in front of me the whole time.
Arrays are intuitive, fast, and let you do (basically) anything. Therein lies the problem with them, no type-constraint, no tracking (other than what you keep in your head).
Tuples are almost exactly the opposite. Powerful, dependable (in and of themselves), type-safe at the position level. But they are awkward, and tend to make code that depends on them, more brittle.
When a debate goes back and forth multiple times with NO NEW INFORMATION being submitted; it tends to devolve into an interminable loop. The only way to break the cycle is to add data, or perspective. The second is honestly the more powerful, by far.
So, what is the perspective that this question is inspected from? "a programming language needs arrays, tuples, or both." There, simply by stating what the subject is in clear terms, we can start to see that the problem is in the perspective itself.
"A programming language needs an ordered-sequence data-structure" (hyphens were hand typed, mmm). Now just look at that! The solution practically bites you on the nose.
Don't use arrays or tuples.
A "tape" is a "constrained by use-case" data sequence. You can think of it as an array with a la carte permissions. With no permissions, a tape explicitly declared will remain exactly that forever.
<primes:int[]=[2, 3, 5, 7]/>
@primes.push(11) // error: length is fixed
@primes[0] = 1 // error: positions are read-only
@primes = [1, 2, 3] // error: replacing the whole thing is its own permission
const big = @primes.map(p => p * 10) // fine: map returns a new value
The sequence itself is frozen: no appends, no removals, no reordering, no swapping one element for another. The elements are exactly as frozen as their own type says. If the type of the thing on the tape has a writable field, that field is writable, tape or no tape. Same rule, all the way down.
<todo:struct>
<title:string=""/>
<let done:bool=false/> // this field grants its own write
</>
<todos:todo[]=[...]/> // a tape with no permissions
@todos[0].done = true // fine: judged by `done`, not by the tape
@todos[0].title = "x" // error: title is locked
@todos.push(t) // error: the tape is frozen
The obvious way to build this is a list of allowed methods: this tape may push, that one may pop. That breaks immediately. @log = @log.slice(1) throws away the first entry using nothing but a non-mutating method and an assignment. No banned method was called. So a tape's permissions aren't a list of methods, they're axes: how the length may change, where changes may happen, whether a position may be rewritten. The compiler judges every write by what it DOES to the value, not by how it's spelled. slice(1) is a change at the front. If the tape doesn't allow front changes, that line doesn't compile.
Here's an audit log. Free length, changes only at the end, and nothing else:
type Entry:struct = { at: number, actor: string, action: string }
<audit:Entry[free, end]=[]/>
@audit.push(entry) // fine
@audit = [...@audit, entry] // same edit, different spelling: fine
@audit.shift() // error: a change at the front
@audit = @audit.slice(1) // error: still a change at the front
@audit = @audit.filter(e => e.actor != "x") // error: a removal from anywhere
@audit = [] // error: a replace
reset(@audit) // error: reset is a replace too
No statement anywhere in the program can remove or rewrite an entry, however it's spelled. That log is provably append-only, and the proof costs you one line.
The permissions are part of the tape's type, so they travel. A function only gets to do what its parameter says:
fn pushEdit(s: Edit[end], e: Edit) -> Edit[end] {
return [...s, e] // the only thing this function CAN do to `s`
}
<undo:Edit[end]=[]/>
@undo = pushEdit(@undo, e) // fine: the compiler reads the body and sees an append at the end
There's no "all permissions" switch. A fully mutable tape has to name every axis it wants. An all-grant is a leaky abstraction, unacceptable.
<todos:Todo[free, anywhere, writable, replace]=[]/>
Every axis named. No shorthand. That's the point.
The tape is specified in the scrml language spec (§66.12) and is being built into the new compiler now. It is not in the shipping compiler yet, and the permission syntax shown here is the proposed spelling.