Every growable list carries the same hazard. A function receives a list, appends “just locally” — and somewhere else a caller’s data has grown, because the value handed over was secretly a view of storage someone else still owns. Sometimes the growth writes through, sometimes a reallocation quietly severs the tie, and which of the two happens can depend on a capacity nobody wrote down. The details differ from ecosystem to ecosystem; 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 hazard, 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 %lld", 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. The bulk verbs live in the arrays unit and are spelled where they are used — AppendAll concatenates, Insert and Remove open and close positions, Sort orders in place, and SubArray answers an owning copy of a window. Each one is written in Mica and is total at its edges. The sequence families page walks them.

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. Length reports how many elements exist and Capacity how many the current backing could hold before growth had to allocate again; Reserve asks for capacity without changing the length, and Resize sets the length outright, zero-filling whatever it exposes. The two numbers never decide whether a copy is a copy — that question has one answer everywhere, which is what the rest of this page is about.

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. Then the sequence families puts all four shapes side by side and states the one law they share.