Every language has the growable list, and nearly every language has the same bug hiding under it. A function receives a list, appends “just locally”, and somewhere else a caller’s data has grown. Python’s default-argument list, the Java List handed to a constructor that keeps it, Go’s slice whose append sometimes writes through to the original array and sometimes quietly does not, depending on capacity — the details differ, the shape is one shape: the growable thing is secretly shared, and growth is where the sharing shows.

Mica has the growable array. It does not have the bug, and this article is about the rule that removes it.

The example is examples/DynamicArrays. Build and run it:

make -C examples/DynamicArrays run

No bounds is the whole declaration

type
    Numbers = array of int64;

Where a fixed array writes its bounds into the type, a dynamic array writes none: its length is a run-time fact. It starts as the empty array — a never-touched variable is empty, Length answers zero — and Append grows it:

Append(address xs, 10);
Append(address xs, 20);
Append(address xs, 30);
  before anything: length 0
  after three appends: length 3

Indices always run 0 to Length-1 — Low and High answer 0 and 2 here — and both loops know it: the counted for reads its range off the value, and for v in xs needs no range at all. An index past the end is the same named-line trap the previous article showed; growth does not buy a way around the bounds.

Assignment copies the elements, not a handle

Here is the section that separates Mica from the languages above:

ys := xs;
xs[0] := 99;
Append(address xs, 40);
  xs grew on: length 4, xs[0] = 99
  ys stayed:  length 3, ys[0] = 10

ys := xs copied the array — the elements, not a handle to them. After the copy, xs was rewritten and grown, and ys moved not at all. There is no backing store behind two variables, so there is no capacity threshold at which sharing appears, no “did the append reallocate?” question to reason about, and no answer that depends on the history of the value.

If you know Go: this is the question append makes you ask — does my slice still alias the original? — answered by the language instead of by you, every time, with no.

The same rule crosses call boundaries:

procedure GrowMine(own : Numbers);
begin
    Append(address own, 999);
    WriteLn("  inside: the copy grew to length %llu", Length(own));
end;
  inside: the copy grew to length 5
  after the call: length 4, still

own is the callee’s array. Its growth is real inside and gone at the return. A callee that wants to grow your array must ask for the arrow — procedure Grow(list : pointer Numbers) — and then every call site says address, which is the out-parameter idiom doing its usual work.

Why Append takes an address

Look at the call again:

Append(address xs, 50);

Append grows the variable you name — that is a write to xs — so the call site carries the same address every writing call carries. The standard library does not get a private way to mutate your variable quietly; it uses the same spelled-out road your own procedures use. One rule, no exceptions, which is why you can audit mutation in Mica by searching for one word.

A known size, said at the allocation

Growing one element at a time says less than a program often knows:

row := new Numbers reserve 3;
row[0] := 7;
  reserved: length 3, row[0] 7, row[2] 0

new Numbers reserve 3 allocates three elements at once — length 3 immediately, every element zeroed, indexable from the next line. Use it when the size is known up front; use Append when it is not. (Where that memory comes from and who gives it back is the memory section’s story — note only that nothing in this example needed a dispose, and that is a guarantee, not luck.)

Jagged tables, spelled as what they are

A dynamic array is an ordinary element type, so it composes:

type
    Table = array of Numbers;
Append(address grid, xs);
Append(address grid, ys);
Append(address grid, row);
  grid[0] has length 5
  grid[1] has length 3
  grid[2] has length 3

Rows of differing lengths — the case the matrix deliberately cannot express — are built here by plain nesting, and the raggedness is visible in the type. A Grid is rectangular by construction; a Table is jagged by construction; there is no type that is secretly sometimes each.

And because rows are values, Append(address grid, xs) copied xs into the table: growing xs afterwards would move nothing in grid[0]. The value rule does not stop at one level of nesting — it never stops.

What this does not do

Copies cost their size. ys := xs copies every element, visibly, at the line you wrote. When an array is large and a copy is not what you mean, the pointer is the explicit tool — and until you write pointer, no call and no assignment can share your elements.

Append is one element per call. Bulk fill is new … reserve n plus a loop, and concatenation is a loop you can see. The library does not hide a loop behind a verb.

Growth may move the elements. After an Append, the array’s storage may have been reallocated — which is invisible precisely because nothing else aliases it. This is the freedom the value rule buys: the implementation can move memory without a single dangling view existing anywhere.

The length is not the capacity. reserve states a size; Length reports how many elements exist. There is no exposed capacity number to reason about, because with no aliasing there is nothing a capacity would explain.

What the compiler proved

A never-touched array read as empty rather than as a crash. Every growth step was a visible address at a call site. A copy stayed a copy through mutation, growth, and a call boundary. And the jagged table carried three rows of three different lengths without a rectangular type pretending otherwise.

Next

Conformant arrays — the missing piece between fixed and dynamic: one procedure that accepts an array of any bounds and learns them, per call, from the value itself. (In preparation; its example is next in the repository.)