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?

C answers by throwing the type away: pass a pointer and a length, and the compiler can no longer check anything — the length might be wrong, the pointer might point at three elements, and every buffer overflow you have ever read a CVE about lives in that gap. Pascal answered better in 1977, and Mica keeps that answer: 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.

What this does not do

Dynamic arrays do not fit. A conformant view conforms over fixed bounds:

analyzer error 5350: the argument type 'Numbers' does not match the conformant
array parameter 'conformant_array_of_int64': a one-dimensional fixed array
with element type 'int64' is required

A dynamic array already knows its length at run time, and a routine over one takes the dynamic type itself. The two shapes stay distinct on purpose: one word in the signature tells you whether a routine serves fixed shapes or growing ones.

One dimension. The refusal above says it: a conformant view is one-dimensional. A routine over every possible Grid shape is not expressible this way — a matrix routine takes the matrix type.

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.

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.