proc main(): void {
mut Str[3] v = ["a", "b", "c"]
v = ["x", "y", "z"] // still exactly three: the promise is kept
echo v[2] // no guard needed, here or ever
// v = ["x"] // compile error: `v` is declared Str[3]
}proc main(): void {
mut v := ["a", "b", "c"] // a Str[3]: rebound only to three, never grown
v[0] = "x" // a write through the name keeps the length
echo v[2]
// v = ["x"] // compile error: `v` is a Str[3]
// v = ["x", "y", "z"] // fine, but a rebinding costs the proof,
// echo v[2] // so this would need a guard
}func twice(n: Int): Int { return n * 2 }
proc main(): void {
Int[2] a = [2, 1]
Int[8] b = [1, 2, 3, 4, 5, 6, 7, 8]
both := a + b // ten elements: the lengths add
echo both[9] // no guard needed
doubled := map(a, twice) // still two
ordered := sort(a) // still two
echo "{doubled[1]} {ordered[1]}"
// filter and filterMap claim nothing, so their results always need one.
}type Reading {
sectors: Float[3] // three, in every Reading there will ever be
notes: Str[dyn] // any number, in each one separately
}
func slower(was: Reading): Reading {
return Reading([was.sectors[0] + 0.1, was.sectors[1], was.sectors[2]], was.notes)
}
proc main(): void {
mut Reading lap = Reading([31.4, 28.9, 33.2], ["clean"])
echo lap.sectors[2] // no guard: the declaration promised three
lap = slower(lap) // a whole new record...
echo lap.sectors[2] // ...and still three, so still no guard
// The other way round for a [dyn] field, where only a guard can say:
if lap.notes bounds 0 {
echo lap.notes[0]
}
}A declared static length is a promise, and it is kept everywhere: every value that lands in a Str[3] slot has to be a vector of exactly three — an initialiser, a later assignment, an argument, a field of a constructed value, a returned value — and a length the compiler cannot see is refused too, which is why split can never fill one. Because the promise holds at every call site it is never lost, so a Str[3] can be indexed unguarded even after being reassigned, and so can a Str[3] parameter inside the callee. A field is the same: a Str[3] field is enforced wherever a value reaches it, construction included, so assigning a whole new record leaves it exactly three.
An inferred length is a length all the same — mut v := ["a", "b", "c"] is rebound only to another three and never grows — but the bounds pass keeps less about it. Writing through the name keeps the proof; rebinding the name costs it, even to the same length, and even inside a branch that may not run, since a proof that holds only sometimes is not a proof. Declare the type when you want the promise, and [dyn] when you want a vector that grows and will guard its indexes.
What a guard proves is weaker again, and in the same way: if 2 < len(box.items) is about the value the field held at that moment, so replacing the field — or the record around it — costs it, even inside the branch the guard opened.
A length the compiler does know survives everything that cannot lose it. + adds the two lengths, map keeps its input's, and sort keeps it too. filter and filterMap claim nothing: what is knowable about them is a maximum, and a maximum can never put an index in range, since a filter that keeps nothing is always possible.