Fixed arrays left one problem deliberately unsolved. Their bounds are part of the type — that is what makes the counted for provable and half the checks free — but it means array[0..4] and array[10..19] are different types. So how do you write one Sum?

The tempting answer is to throw the type away: pass an address and a length, and trust the two to agree. But a bare length can lie about its buffer — nothing ties the number to the storage it describes, the count might be wrong, the address might reach three elements, and every buffer overflow you have ever read a CVE about lives in that gap. The answer Mica keeps is as old as Pascal: let the parameter declare the bounds as variables, and fill them, per call, from the argument’s own type.

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

make -C examples/ConformantArrays run

The parameter that learns its bounds

function SumOf(a : array[lo..hi : int64] of int64) : int64;
var
    i, total : int64;
begin
    total := 0;

    for i := lo to hi do
        total := total + a[i];

    SumOf := total;
end;

The brackets do not name bounds — they declare them. lo and hi are two extra parameters, filled at each call with the argument’s own declared bounds, readable inside like any local:

WriteLn("  SumOf over 0..4:   %lld", SumOf(s));
WriteLn("  SumOf over 10..19: %lld", SumOf(w));
  SumOf over 0..4:   15
  SumOf over 10..19: 1000

One routine, both types, no conversion at either call. For the Small, lo and hi read 0 and 4; for the Wide, 10 and 19. The loop cannot be off by one against either array, because it reads the same declaration each caller’s type wrote — the guarantee from the aggregates article, now crossing a call boundary intact.

And nothing was passed beside the array. There is no length argument to get wrong, which is precisely the C gap this construct closes: the bounds travel inside the value, so they cannot disagree with it.

The bounds being ordinary values, a routine can answer questions about the shape itself, and views hand on — a conformant view passed to another conformant routine carries its bounds with it:

function SpanOf(a : array[lo..hi : int64] of int64) : int64;
begin
    SpanOf := hi - lo + 1;
end;

function AverageFloorOf(a : array[lo..hi : int64] of int64) : int64;
begin
    AverageFloorOf := SumOf(a) / SpanOf(a);
end;
  SpanOf(s) = 5, SpanOf(w) = 10
  AverageFloorOf(s) = 3

The view is constant — enforced, not promised

Here is where Mica sharpens the 1977 answer. The plain view reads the caller’s elements in place — no copy is taken — and in exchange, writing through it does not compile:

a[lo] := 777;
analyzer error 5146: left side of an assignment cannot be a constant
parameter: 'a' with passing mode 'by constant value'

Read that mode name again: by constant value. The routine sees the caller’s array without copying it, and the compiler guarantees the caller’s array leaves the call untouched. You get the performance of pass-by-reference with the semantics of pass-by-value, and neither is a convention — both are checked.

This is the value model bending exactly once, where it is safe: a view that provably cannot write is the one case where sharing storage costs the caller nothing.

Writing takes the pointer view

When mutation is the point, the same bracket spelling goes behind pointer:

procedure FillRamp(a : pointer array[lo..hi : int64] of int64, step : int64);
var
    i : int64;
begin
    for i := lo to hi do
        a[i] := (i - lo) * step;
end;

And the call site says what every writing call in Mica says:

FillTwice(address w);
  w[10] 0, w[18] 16, w[19] -1
  SumOf over the refilled 10..19: 71

address at the call is the caller’s consent, exactly as it was for the scalar out-parameter and for Append. Note the middle routine:

procedure FillTwice(a : pointer array[lo..hi : int64] of int64);
begin
    FillRamp(a, 2);
    a[hi] := -1;
end;

FillTwice forwards the view to FillRamp with no address — it already holds the pointer view, and its own parameter type says so. Permission to write is visible at every level: granted once at the original call site, carried explicitly in every signature it passes through.

The bounds still bite

A view does not relax the checks. Index it outside the bounds it arrived with and the trap names the line, inside the callee:

function At(a : array[lo..hi : int64] of int64, index : int64) : int64;
begin
    At := a[index];
end;
ok 4
Mica runtime failure: reason=index_out_of_range (12)
Mica runtime context: file=CT.mica, line=11, column=12
Mica runtime source:     At := a[index];

At(s, 4) answered; At(s, 5) trapped at the indexing line. The view carries the real bounds, so the check inside the callee is against the caller’s true array — not against a length somebody passed alongside and got wrong.

Dynamic arrays pass too

A dynamic array passes into the read view exactly as a declared array does: its runtime length becomes the view’s bounds, lo at 0 and hi at length - 1. One SumOf therefore serves a declared array, a dynamic array, and a view passed through — the signature does not care how the storage got its size. An empty dynamic array passes as the empty view, which is precisely how a whole-array reduction first meets emptiness.

The writable view stays a fixed array’s contract: address d over a dynamic array is refused, because growth and in-place writes through a borrow are different promises — a routine that grows dynamic storage takes the dynamic type itself, as Append does.

What this does not do

Three or more dimensions. A conformant view reads one contiguous run: a one-dimensional array passes its declared bounds, and a two-dimensional array passes as its flat row-major block, the same reading its whole-matrix reductions use. A rank-three Grid has no single contiguous reading a view could name, so it is refused in shape vocabulary:

analyzer error 5350: the argument type 'Grid' does not match the conformant
array parameter 'span of int64': a one- or two-dimensional fixed array or a
one-dimensional dynamic array with element type 'int64' is required

The element type is fixed. SumOf serves every bounds of int64 array, not every element type. Genericity over the element is a different mechanism with its own rules — gen blocks — and its own place in this series later.

The bound parameters are read-only. lo and hi describe the view, and assigning to one is its own refusal:

analyzer error 5351: the bound 'lo' of a conformant array parameter is
read-only: it carries the caller array's declared bound

What the compiler proved

One SumOf served two incompatible types with no length argument to lie. The reading view took no copy and still could not write — refused at compile time, not discouraged in a comment. The writing view was consented to with address at one call site and visible in every signature below it. And an index that left the real bounds trapped at its line, inside the callee, against the caller’s true array.

The view outgrew the parameter

Since 7.0.0 the read view is no longer confined to parameter position: the same three words have a positional spelling, span of T, that stands in var, parameter and return positions, and a Span intrinsic that borrows a sub-range of an array you name. The binder spelling on this page and the span spelling are one type — a span argument passes straight into SumOf above — and the borrow’s safety story, the lending law, has its own page: spans.

Next

That completes the wave: values and pointers, records and arrays, dynamic arrays, and this one. Sets and bitsets open the next wave of the values section.