Status: Superseded by ADR-288 — its D1-D6 are D7-D12 there Extends: ADR-027, whose §4 named this as the next question Related: ADR-024 (the checker whose answers this reuses), ADR-025 D7 (the first instance of the same shape), ADR-020 (the ledger says what a caller cannot see), ADR-029 (answers D6)
ADR-027 made sync something a function earns from its body rather than something a person
types. It measured what that was worth on examples/1brc.nika: strip all seven sync
declarations, rebuild, and four come back. The three that did not were named, and so was
the reason:
Summary::{new, record, merge}reachHashMap::new()and.entry(…), a path and a method no ledger names. […] a method becomes resolvable the day its receiver has a signature written down, and neither analysis has to change for that to help.
That was written as future work. It turned out to be nearer than that, because of a fact the ADR did not check: the type checker resolves method calls already.
// crates/nikaia/src/check/mod.rs, before this ADR
Expr::MethodCall { receiver, method, args } => {
let on = self.expr(receiver, span); // the receiver's type
let key = format!("{name}::{}", …); // Stats::add
let Some((key, contract)) = self.method(&key) else { return Ty::Unknown };
…
}Everything ADR-027 D2 refused to guess at was being computed one module away, on every build,
and thrown away. The sync inference was not short of an analysis. It was short of an
answer somebody else had.
sync.rs walks the AST and asks a ledger what each call promises. It has no types, and giving
it types would mean giving it a second type checker — worse than the first one and obliged to
agree with it. ADR-027 already made the case against two resolution rules for one question;
two type checkers is the same mistake one level up.
The alternative is what ADR-025 D7 did for the emitter, which needed to know
which for iterates a fallible stream and could not tell without inferring the iterator’s
type. It did not grow an inference. It asked. This is the second instance of that shape, and
it should be the pattern rather than a coincidence: the module with the types answers the
questions about types, and the answer is part of what a pass hands back.
Checked gains methods: BTreeMap<String, MethodCalls> — per function, by the name the ledger
records it under, the set of keys its method calls resolved to and whether any did not resolve.
Per function, not per call site, and that is forced rather than chosen: identifiers are
interned (Symbol carries no position), so there is nothing to key a call site by. It is
enough for the inference, which asks “can anything this function calls pause” and never “which
call”.
Ledger::infer runs the checker, in a fixed order.sync from the bodies, using both.Step 2 does not depend on step 3, which is what makes this sound rather than circular. The
checker reads signature, fields and iterates from a ledger and never sync. So resolving
a method against the step-1 ledger yields exactly what resolving it against the finished one
would.
That is an invariant, not an observation, and it is held to by a test
(the_checker_does_not_depend_on_the_sync_it_helps_infer) that runs the checker twice — once
against each ledger — and compares all three of its outputs. If someone ever teaches the
checker to read sync, that test fails and says why, instead of the ledger quietly ceasing to
be a pure function of its source.
The pass is handed back rather than discarded (Ledger::infer_checked), because the compiler
wants the findings and the fallible loops too. Running the checker twice a build to get one of
them would be waste, not caution.
NK2202 names one call and puts a caret under it. D1’s answer is per function, so the best it
could produce is “something in here pauses” — which Part III C.2 does not allow, and which
would be a worse diagnostic than the silence it replaced.
So the check keeps the permissive polarity ADR-027 D2 gave it, and the inference — which needs no caret — does not wait for expression-level spans. The two now differ in one more way, and each difference still has a reason of its own.
Expr::Index claimed Ty::Unknown unconditionally. The cost was never the missing type; it
was everything built on it. In n-body.nika:
let b = &self.bodies[i] // b: unknown
let dx = b.x - self.bodies[j].x // unknown
e = e - (…) / (dx * dx + dy * dy + dz * dz).sqrt() // receiver unknown → `.sqrt` unresolvedenergy is arithmetic over floats from first line to last, and a single Unknown at the
bottom of the expression erased all of it.
Vec[T] and List[T] indexed yield T; HashMap[K, V] yields V; anything else still
claims nothing. Indexing text is a slice in some languages and a byte in others and Nikaia
has not said, so it stays ? (ADR-024 D1) until it does.
std.contracts describes the collections and text the language below provides.Vec, HashMap, str, String, f64 are Rust’s, and a compiler that does not read Rust
cannot infer them. ADR-020 D5 already established the mechanism — a library whose
implementation is in another language writes those contracts down and reviews them like code —
and this is that mechanism used for a second purpose.
Every entry was observed being asked for by a program in this repository. None is speculative, and the discipline matters more here than usual: a missing entry only fails to help, while a wrong one makes the checker reject a correct program, which is the one promise the checker cannot break.
Types are ? wherever the honest answer is “there is no one type”. What an entry does claim is
its arity, and that is checked — so the corpus is what holds the risk down.
sync, deliberately.Entry::and_modify and Entry::or_insert_with run the lambda they are given. Whether they
pause depends on what is in it, and a ledger cannot say “it depends” yet.
So they get a signature — the type checker resolves through them — and no sync. A caller
therefore still loses its inferred promise, which is the correct answer rather than a
limitation to apologise for: sync = true there would be a promise about somebody else’s code.
sync = "from(f)" is the shape that says it properly, and it is
ADR-029’s — which answers it, so the four functions §3 leaves open
close there rather than here.
Strip every sync declaration from each example that has one, rebuild, and count how many of
those exact entries the compiler gives back on its own:
| example | before (ADR-027) | after | still open |
|---|---|---|---|
1brc.nika |
4 / 7 | 5 / 7 | Summary::record, Summary::merge |
access-log.nika |
3 / 6 | 4 / 6 | Report::record, Report::merge |
k-nucleotide.nika |
2 / 2 | 2 / 2 | — |
n-body.nika |
0 / 3 | 3 / 3 | — |
| total | 9 / 18 | 14 / 18 |
n-body is D4 on its own: nothing about it involves a collection method, and all three
functions were blocked by one untyped index.
The four that remain are one shape, not four problems. Every one of them is a method called on a lambda parameter:
self.stations.entry(m.name)
.and_modify fn { a.add(m.temp) } // what is `a`?
.or_insert_with fn { Stats(m.temp) }a is an implicit closure argument, and nothing gives it a type. To type it, the ledger would
have to say what and_modify passes its lambda — a function type in the signature language,
which it does not have. That is the same missing vocabulary D6 ran into from the other
side, which makes the remaining four a single well-defined next question rather
than a long tail — and ADR-029 answers it.
Give sync.rs its own receiver-type inference. A second type checker, obliged to agree
with the first. ADR-027 refused two resolution rules for one question; this is that at a larger
size.
Key the resolutions by call site. Would let the check use them too (D3), and there is nothing to key by: identifiers are interned and carry no position. Available the day expression-level spans exist, and nothing here has to change to take it.
Write std contracts for everything Rust has. Fast to do, and every wrong entry rejects a
correct program silently until somebody writes the program that trips it. D5’s rule — an entry
exists because a program asked for it — is slower and keeps the checker’s promise.
Mark and_modify sync = true because its lambdas are pure in practice. It would have
made the table above read 18 / 18. It would also be a promise about code the ledger has never
seen, which is exactly the failure mode ADR-027 §2 exists to prevent.
Type an index over text. s[i] has no decided meaning in Nikaia. Claiming one here would
settle a language question inside a type checker.
sync inference reaches five more functions in the corpus and
the number rises again whenever std.contracts grows — with no change to either analysis.std entries put both
sides of more comparisons in writing. That is the checker’s stated growth path (ADR-024) and
needed no change to it either.Ledger::infer is no longer a pure walk of the AST; it runs the checker. The ordering that
makes that sound is D2’s invariant and is tested rather than asserted.