Mica has four ways to hold a run of elements. They differ in where the elements live and who decides how many there are, and in almost nothing else: the same readers answer all four, the same reductions walk all four, and one law governs every value among them.
This page is the map. It assumes records and arrays, dynamic arrays, conformant arrays and spans, and it puts them side by side so the shape of the whole family is visible at once.
The example is
examples/SequenceFamilies.
Build and run it:
make -C examples/SequenceFamilies runThe four faces
fixed array a : array[0..3] of int64 the value IS the element block
┌──────┬──────┬──────┬──────┐ bounds live in the type, checked before the run
│ a[0] │ a[1] │ a[2] │ a[3] │ 32 bytes, inline, no heap
└──────┴──────┴──────┴──────┘
vector, v : vector[4] of int64 a fixed array wearing its shape in its type
matrix m : matrix[3, 3] of float64 the shape is the type's own, checked before the run
matrix elements are one contiguous row-major block
dynamic array d : array of int64 the value is a descriptor, the elements a backing
┌──────┬────────┬──────────┬──────┐ ':=' deep-copies the backing — no hidden sharing
│ data │ length │ capacity │ head │ ──▶ Append may move the backing
└──────┴────────┴──────────┴──────┘
span w : span of int64 the value is a borrow, three words wide
┌──────┬─────┬──────┐ owns nothing: no dispose, no copy, no growth
│ data │ low │ high │ ──▶ someone else's read-only; never outlives its backing
└──────┴─────┴──────┘Two of the four own their elements outright — the fixed array and the vector carry them inline, in the value itself. One owns them at arm’s length: a dynamic array’s value is a descriptor, and the elements live in a backing it allocated. One owns nothing at all: a span is a window onto elements somebody else holds.
One vocabulary reads all four
WriteLn(" fixed length %lld low %lld high %lld sum %lld", Length(fixed), Low(fixed), High(fixed), Sum(fixed));The same four calls answer for every face:
fixed length 4 low 0 high 3 sum 10
vector length 4 low 0 high 3 sum 10
dynamic length 4 low 0 high 3 sum 10 capacity 4
span length 2 low 1 high 2 sum 4Length says how many elements a value has. Low and High say where its
indices run. Sum — and every other reduction — walks it. Capacity is the
dynamic array’s own extra question: how many elements the backing it currently
holds could take before growth had to allocate again.
Every one of them answers in the signed 64-bit domain, so a count and a
bound meet in ordinary arithmetic with no conversion standing between them, and
Length(x) - 1 over an empty sequence is minus one rather than the largest
representable unsigned value. There is one exception, and it is not an
inconsistency: an array indexed by an enumeration answers Low and High in
that enumeration, because that is what its indices are.
The counted for reads its range off the value, and for x in needs no range
at all — both work over all four faces.
The one law
Everything above is convenience. This is the part that decides what programs you can write without being careful:
A value owns its elements, all the way down. A borrow is spelled where it is taken.
Both halves are checkable, and the example checks them.
A copy owns its elements
Take a table of rows — a growable array whose elements are themselves growable arrays — copy it, and then rewrite and grow the source:
copied := table;
table[0][0] := 999;
Append(address table[0], 777); source row 0 length 5 first 999
copied row 0 length 4 first 4The copy did not move. Not the element it never asked about, not the length it never asked about. There is no depth at which Mica switches from copying to sharing — no shallow copy, no reference at level three — and this holds for every road a value travels, not only assignment: a by-value parameter, a returned result, a record field, an element of a larger array. The aggregates page proved this for a record inside an array; here it holds for a growable row inside a growable table, which is the case where a language has to work for it.
What it costs is the honest thing: a copy costs its size, visibly, at the line
you wrote. When that 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.
A borrow is visible
The other half is the span. A borrow reads storage it does not own, so the program says where it was taken:
window := Span(fixed, 1, 2); span length 2 low 1 high 2 sum 4
after fixed[1] := 50 the same span sums to 53The window saw the new value, because there is no copy to go stale. That is what makes it a borrow rather than a slice — and it is also why the language has rules about where a borrow may rest, which the spans page states in full.
A record field lends like a variable
A field is whole storage exactly as a variable is, and it lives as long as the
record that holds it. So it lends on every road a variable lends on: the
reductions read it, Span borrows a window of it, a named span may hold that
window, and the writable view writes through it.
WriteLn(" field sum %lld window sum %lld", Sum(probe.samples), Sum(Span(probe.samples, 0, 1)));
Scale(address probe.samples, 10); field sum 10 window sum 5
after Scale(address probe.samples, 10) the field sums to 100Scale is an ordinary writable view, which is the write face of a borrow:
procedure Scale(a : pointer array[lo..hi : int64] of int64, by : int64);The bounds arrive from the argument’s own value, the callee sees elements and
never the descriptor, and the call site spells address like every other write
in Mica. A span of T is the read face and stays read-only; writing keeps the
pointer-spelled binder, so you can still audit mutation by searching for one
word.
The element verbs
A dynamic array grows by Append, and the arrays unit carries the rest of
the vocabulary. All of it is written in Mica, generic over any storable
element, and total at every edge — a window reaching past the end stops at
the end instead of trapping.
| Verb | What it does |
|---|---|
Insert(address xs, index, item) | opens one position at index and puts item there |
Remove(address xs, index, count) | closes count positions from index |
AppendAll(address xs, address items) | appends every element of items |
Sort(address xs) | heapsort in place, no allocation, worst case equal to best |
SubArray(address xs, index, count, address into) | fills into with an owning copy of the window |
after Insert, Remove and Sort: length 4 first 2 last 99
SubArray of 2 from index 1: length 2 first 3
AppendAll of that piece onto itself: length 4 last 4That last line is worth a sentence. AppendAll reads the source length once
before the first append, so appending an array to itself terminates on the
length it started with. Each verb is shaped for the hazard it has: Insert
grows and then shifts downward so nothing is overwritten before it has moved,
and Remove shifts upward and then resizes, because the length is the array’s
own answer to how many elements it has.
Sizing has its own three: Reserve asks for capacity, Resize sets the
length outright — zero-filling whatever the growth exposes — and Clear is the
resize to nothing.
Where the answer is built
Two positions used to be closed to a dynamic array, and both are open.
A function grows its own result variable, so the answer is built where it will be returned from:
function Squares(count : int64) : Row;
var
i : int64;
begin
for i := 1 to count do
Append(address Squares, i * i);
end;The result variable is the one storage a callee owns outright — it lives exactly as long as the activation that builds it, and the return hands its value on. So no local is built and no whole copy moves the answer out at the return.
And a generic takes one by value, like any other value:
function Total(xs : List of E) : E;
gen
E is numeric; Squares(5) length 5 last 25
Total(grown) through a generic taking it by value: 55The callee receives an independent copy, so what it does to that copy is
invisible to its caller — which is the whole point of passing by value, and it
is what makes a map whose values are dynamic arrays expressible: Put takes
its value by value.
Writing a whole value at once
Any of these shapes can be written as a value, in one expression, wherever a value of that type belongs:
var
fixed : Fixed := (4, 1, 3, 2);
shaped : Shaped := (4, 1, 3, 2);The list is an expression, not a declaration form: it stands in an assignment, an argument, and a result as readily as in a declaration. A record spells its fields, and nesting composes, so a matrix is written the way it looks on paper:
m := ((1.0, 2.0), (3.0, 4.0));
point := (x: 1.5, y: 2.5);The list is total: every position is written exactly once, and a short list, a long list, a repeated field name, or an element whose type does not fit its position is refused with a message naming the position. The spelling is parentheses because brackets are the set constructor, and a parenthesized expression with neither a comma nor a field name is still an ordinary grouping — nothing that compiled before means something else now.
Two positions do not take one, and for the same reason in different words: a dynamic array names a backing the list has no region to allocate, and a span borrows elements it does not own. Both say so:
analyzer error 5502: an aggregate literal writes a whole composite value, and a
span borrows one: a span owns no elements of its own, so there is nothing in it
for a list of values to fill — build the elements in an array the program owns
and borrow thatWhat this does not do
No whole-value comparison. a = b between two aggregates is refused:
equality over a block of elements is a walk, not an operator, so you compare
the elements or the fields that decide the answer. The relational operators are
refused for the same reason.
No writable span. One face, the read face. The writable view keeps its
pointer-spelled binder, so every write path still says address.
No bracket slicing. Span(place, from, upto) is the one spelling for a
borrowed window. Brackets go on meaning one element, and no sugar mints a
borrow that reads like a copy.
No dispose on a sequence. A dynamic array’s backing belongs to the region
that allocated it and is reclaimed with it; there is no hand-back to write and
none to forget.
No anonymous element type. An array’s element is a named type, so
array of array of float64 is refused and the diagnostic writes the two
declarations it wants instead.
What the compiler proved
One reader vocabulary answered four different shapes with no conversion between a count and a bound. A copy of a table of growable rows stayed a copy through a rewrite and a growth of its source. A window reported its backing’s later edit, because it is a borrow and says so at the line it was taken. A record’s own field lent itself for reading and for writing. Every element verb held its edge. A function grew its result where it stood, and a generic took the finished array by value.
Next
The type system reference carries the same map in normative form — one table of what each family admits and what it refuses, with the code the compiler prints beside every refusal.