Issue #1209: A changeable part of a list: xs[a..<b] handed to a mut parameter and changed in place (sort, swap, fill), and fill on a list

Open and answer this issue on GitHub.

ready · opened 2026-11-03 · updated 2026-11-03 · 0 comments

Found while probing the forms a CDCL(T) solver needs in Nikaia: ADR-270 D16 keeps every clause in one arena of u32 words (a header, then the literals), so a clause is a part of a list, and a solver sorts, swaps and resets parts. Probed on target/fast/nikaia at 31e2ea7, language 0.0.1341.

What exists and what does not

• A part is read: ref Array[T] (Part I 2.x) takes xs[a..<b] as well as a whole list (sum(xs[1..<4]) works).
• A part is not changed. Both are refused:

fn zero(mut xs: Array[u32]) {
    for i in 0..<xs.len() { xs[i] = 0 }
}
fn main() {
    let mut xs: Vec[u32] = [1, 2, 3, 4]
    zero(xs[1..<3])
    xs[3..<4].sort()
    println(xs.iter().join(","))
}

zero(xs[1..<3]): NK1102 (zero keeps its xs after the call returns); xs[3..<4].sort(): NK1171 (Array has no method called sort). Expected: 1,0,0,4. ref mut is C-only (NK1158), so nothing else says it.

• xs.fill(v) on a list: NK1171. Part I does not name it; [v; n] and resize exist.

Decision (supervisor, Language decisions: obvious)

No ADR or part refuses a changeable part (no kind 1); it was not decided because nothing needed it (kind 2). The language principles settle it without a choice between designs, so it is approved here and goes ready, not decision:

• The form already exists: a mut parameter is how a function changes what it is given (Part I 6.5), and xs[a..<b] is how a part is named; a mut xs: Array[T] taking xs[a..<b] puts the two together. The rules that already hold for a let mut view (ADR-views-1, ADR-views-2) hold for it: while the part is handed out as mut, the list is not read or changed otherwise (NK2305), so no two changeable parts of one list overlap.
• Nobody pays who does not use it: it lowers to &mut v[a..b], the same slice the read view already is.
• Other languages: Rust (&mut [T], split_at_mut), Go and Swift (ArraySlice) all change a part in place; the alternative, passing the whole list with an offset, moves bounds arithmetic to the user (against complexity goes into the compiler) and is the kind of write-around CLAUDE.md forbids.
• Not decided here, left out: two changeable parts of one list at once (split_at_mut). It needs disjointness to be shown (by the prover or by one call that splits); a builder who needs it stops and reports.

To build

1. Specification (supervisor): Part I, next to ref Array[T]: a mut parameter of type Array[T] takes a part xs[a..<b] or a whole list of a mut place, changed in place; on a list and on such a part: xs[i] = v, swap, sort, sort_by_key, reverse, fill(v); the view rules of 6.5 hold. Version raise and changelog with it.
2. Tests in tests/compiler/tests/: the probe above (.stdout 1,0,0,4); fill on a whole list; a .stderr case reading the list while its part is handed out as mut (NK2305); an out-of-range part aborts as an index does.
3. Checker: accept a mut xs: Array[T] parameter for xs[a..<b] of a mut place (a local let mut, a mut parameter, a field of ref mut self), and the listed methods on a part and on a list.
4. Lowering: &mut v[a..b] for the argument, [T]’s swap/sort/sort_by_key/reverse/fill for the methods.
5. Prover: a part’s len() is b - a, so xs[i] with i < xs.len() inside the callee stays proved.

Back to Open Issues