for Lends, and Everything Downstream of the Binding Has to Know ItStatus: Accepted
Date: September 21, 2026
Closes: #138 (a cast over a for
binding is a cast over a view) and #147 (a slice of text read as a value does
not lower)
Builds: ADR-094 D4 (a for lends) and
ADR-293 D9 (a read is a call and the * takes it apart), neither
of which changes — this is what they already said, said at the two places that
had not heard it
Related: ADR-285 D12 (a narrowing conversion aborts),
ADR-285 D1 (a length is an i64), ADR-152 D4
(an array carries its length), ADR-179 D1 (ref Array[T] is a run),
ADR-185 D1 (a let that declares a struct over a lent binding),
ADR-288 (the emitter knows no types)
Two constructs left Part III C.1 to the language below, speaking about the generated file (#138):
comptime NS: Array[i32, 3] = [1, 2, 3]
for n in NS { sum = sum + (n as i64) } // casting `&i32` as `i64` is invalid
println(f"{text[1..3]}") // the size for values of type `str`
// cannot be known at compilation timeNeither noun — &i32, str — is in the program, and both came with a way out
that cannot be taken: dereference the expression, the trait Sized is not
implemented for str. C.2 says a way out that
cannot be taken is not one.
What makes them one record is that both are a view the compiler wrote
meeting a construct that was never told. A for lends
(ADR-094 D4), so the binding is a &i32; a read is a call whose
* takes it apart (ADR-293 D9), and over a range what it
takes apart is a &str. Each decision is right and neither is wrong here: what
is needed is the sentence that says so at the cast and at the bracket — and at
the three further places D3 to D5 name, each of which would otherwise be a
silent wrong answer.
*.nikaia_std::num::value(n) as i64, where value is the identity for a number
that is already a number and the number behind any run of views.
A * would be right at the binding and wrong one line down. let n = 5
inside the loop shadows it, and a * written onto that is rustc about the
generated file — the very thing this closes, moved rather than removed. Choosing
on the type is what a trait is, and this is
index::At’s own reasoning one
construct over: a uniform rule is the one that cannot be applied to the wrong
operand.
Which operands is the checker’s, because which name is a view is a
question about the scope and the emitter keeps none
(ADR-288). It is recorded on the binding —
Local::lent — for the reason immutable is: the scope is then the one the
checker already keeps, and a let that shadows the name stops being a view
exactly where it stops being the answer.
Only a bare name, because that is the only operand shape that can arrive as a view: a call, a literal and an arithmetic expression each come to a value, and a field read or an index is taken apart by the lowering that wrote it.
Inside the checked conversion and not around it. A narrowing cast over a lent binding is still a narrowing cast, and the abort ADR-285 D12 puts there is not a thing a view may skip.
*.text[1..3] and xs[1..3] answer a &str and a &[T]; * over one of those
is a str or a [T], which the language below has no size for. The read at a
number keeps its *, because xs[0] is the element the program asked for
and not a view of it.
Off the shape of what is in the brackets, which is the one place this needs
no type: a range is a run and a key is not, in this language and in the one
below alike. So ADR-288 holds — nothing here asks what text is.
And a written ref over such a read is the view it already is. ref
dna[i..<i + k] would otherwise be a &&str below: the source’s ref and the
read’s own view are one claim written twice.
index::at cannot pin a bare 1..=2: At is implemented for a range of every
signed type and all of them answer the same RangeInclusive<usize>, so there is
nothing to infer from and what came back was cannot infer type about the
generated file. Handed over as written it settles itself, because
RangeInclusive<usize> is the only candidate that is a SliceIndex<[V]>.
A range built out of names is an i64 one and has to be converted, which is
ADR-285 D1’s whole trade. So the literal exception the write
branch already had applies to a range too, which it could not while the *
stood over one.
Except where it counts from the end. xs[-2..-1] is an access out of
bounds and reports as one at run time, which is D1’s own rule — and it has to
reach run time. Handed over as written it does not: -2 against the usize
a slice wants is the trait Neg is not implemented for usize, about a type
the program never named, with consider specifying an integer type that can be
negative as the way out. So a negation goes back through the conversion,
widened, because an i64 is the one width this language indexes with and
at has nothing else to read it off. What the program then gets is index out
of bounds: the index is -2, at the line that wrote it.
element_of answers for Array[T, N] — whose two arguments are why a
Vec arm does not reach it — and for ref Array[T], as it does for Vec[T],
List[T] and Seq[T]. Otherwise a for over either binds a name of
unknown type, and everything downstream goes quiet with it.
Including ADR-285 D12’s abort: for n in NS { n as u8 } over an
Array[i64, 2] would truncate silently, which is the one thing that record
exists to stop. An absent type is not an error (ADR-024 D1) and
that is right — but an absent type that should have been there is every check
downstream of it not run.
let whose annotation is a number reads it through the binding; a let whose annotation is a type does not.let q: i64 = n over a lent n would be &i64 where an i64 was declared.
The number is read through the view, by D1’s own helper.
A let copy: Row = r is a different question, decided by
ADR-185 D1. A
number is Copy, so reading one through a view inserts nothing; a struct is
not, so the same answer there would be a copy the source did not write —
ADR-283 D3 forbids one in as many words. The way out exists and
the program can take it (let copy = r), which makes it a refusal rather
than a lowering.
num::value is a fifth uniform rule, beside index::at, index::get,
count::of and concat. Each exists because this emitter cannot ask what a
thing is, and each is the identity for what it is not for.bool on every local, and a call in the generated file
at the casts that need it and nowhere else.let r = 1..3 is not a value this language has a
type for, so xs[r] is not a shape to decide about yet.for binding should be readable as the element. It is a view,
and that is ADR-094 D4’s decision and not this record’s; what
this adds is that the constructs downstream of it are told. A binding that is
a number, a bool or a char is read as the element: the loop’s body opens
by reading it through the view with D1’s helper, because telling one construct
at a time misses one. A view of a copy and the copy say the same thing.