as Names a Type This Language Offers, and a Count Goes In as an i64Status: Superseded by ADR-285 — its D1-D2 are D14-D15 there
Related: ADR-048 D1 (a length comes back as an i64; its §4 left
the parameter direction open and this answers it), ADR-043 D4 (a
conversion that does not fit aborts — the rule as usize was outside of),
ADR-011 D2 (the emitter does not know types, which is why both
conversions are chosen by name)
ADR-048 D1 made a length an i64 and emitted the conversion in both
directions, so a program writes none. Its §4 declined the other half — a std
function whose parameter the language below counts in usize — on the ground
that it is “the same shape of question and a different set of signatures, and no
program has yet been written that makes the answer obvious”. Its §3 named the one
site: " ".repeat(indent as usize) in examples/json/src/main.nika.
The decline was right about the question and wrong about the cost. It recorded
the site as the edge of D1’s scope, written down rather than left to be
discovered. It is not that edge. Three things were true of that line, and only the
first is about usize:
as named any Rust type at all, unread. n as u128 compiled and ran, and so
did n as isize — a type ADR-048 D2 deliberately left out. The
type list was narrowed; what an as may name never was, because nothing had
decided it.-3 as usize is 18,446,744,073,709,551,613. Silently — in a language where
ADR-043 D4 makes a conversion that does not fit abort, and where
the same conversion at an index has reported as an access out of bounds since
D1. Written by the compiler it reports; written by hand it reported nothing." ".repeat(indent) — produced a rustc message whose help was
“you can convert an i64 to a usize“: the compiler recommending a type the
page does not offer, about a file nobody wrote, which is the Part III C.1 class.What was actually missing was not a decision. The ledger writes repeat’s
parameter as n: ? — the absence of a claim (ADR-024) — and carries
no usize anywhere. So there was nothing for a rule to apply to: no conversion can
be emitted at a parameter whose type nobody wrote down. Writing it down is what
made the answer obvious, which is the program §4 was waiting for.
as names one of the types Part I 2.2 offers, and nothing else.i32, i64, u8, f64, bool, char, String, &str. Anything else is
refused as NK1122, naming the type and, where it is a machine-width or
unoffered integer, saying that the compiler writes the machine’s conversion itself.
Wider than the list that decides which conversions are checked at run time
(ADR-043 D4, i32 i64 u8 f64), because the two answer different
questions: that one is which conversions can lose something, this one is which
types a program may write. A narrower list here would refuse a program for a
reason nothing on the page states.
A refusal, and now rather than later. It costs nothing today — the whole corpus contains four casts, and the two it breaks are fixed by D2 in the same change — and the same refusal after programs exist breaks them.
std parameter the language below counts in usize is written as the i64 a program can hold, and the conversion is emitted.The ledger says str::repeat(&str, n: i64) -> String, and the emitter writes
nikaia_std::count::of(…) around the argument. So a program writes
" ".repeat(indent) and never a conversion, in either direction — which is what
D1 of ADR-048 buys at a length, now bought at a count.
A negative count says what it is, and this is where it differs from an index.
index::at reports a negative as an access out of bounds because it is one,
which is what let ADR-048 emit that conversion without inventing a failure mode. A
negative count is not an access at all, so count::of has a message of its own:
“a count cannot be negative: the count is -1”. Reusing the index message would
name something the program does not do.
Chosen by name and position, not by a rule, for the reason the length
conversion is: what it encodes is a fact about Rust’s library rather than about
this language, and the emitter does not know types (ADR-011 D2). The
list is the ledger entries whose Rust counterpart counts in usize, and today it
is one. a_count_parameter_is_an_i64_and_the_emitter_knows_its_name in
tests/contracts.rs is what keeps the ledger and the emitter from drifting apart.
Being a name is safe because count::of is the identity for anything that is
not a number — the property that lets index::at be written around every index. A
method of the program’s own called repeat passes through untouched.
A literal count takes no conversion, the same exception an index has:
"-".repeat(3) stays as written, because of(3) has nothing to infer its argument
type from — every integer type answers with the same usize — and cannot infer
type about a generated file is what Part III C.1 forbids. Rust’s own inference
already gives a literal the usize.
examples/json/src/main.nika loses both casts, and its indent becomes an i64. That
last part is the answer arriving from the direction §4 asked it to: with the
parameter written down, the type checker said the i32 did not match — a question
nothing could ask while the signature was ?.
The ledger names usize in no signature at all now, in either direction. It is
a type of the machine, and the compiler writes every conversion into and out of it.
std entry arrives that cannot be described
without one, that is the argument for reopening it, and no such entry exists.Both decisions, with the corpus and the suite green.
check::OFFERED is the eight types and NK1122 is raised at a cast that leaves
them. nikaia_std::count is the conversion, with a message of its own and the
identity for everything that is not a number. emit::is_count writes it around
repeat’s argument, skipping one written only in literals. std.contracts says
n: i64, and no signature in it names usize.