Status: Superseded by ADR-288 — its D1-D4 are D17-D20 there
Closes: the question ADR-029 §4 left open
Related: ADR-024 D4 (a generic parameter is erased to ?, and
why this is not that), ADR-020 (the ledger’s type language)
Three ADRs in a row ended at the same wall.
ADR-027 inferred sync from bodies and could not vouch for a method call. ADR-028 resolved
method calls and could not type a lambda’s parameter. ADR-029 gave the ledger function types and
still could not say what and_modify hands its lambda:
self.stations.entry(m.name).and_modify fn { a.add(m.temp) }a should be a &Stats. Stats comes from the map — HashMap[&str, Stats] — and the
signature language had no way to refer to it. and_modify(Entry, f: fn(?)) was the most it could
say, so a was ?, so a.add resolved to nothing, so record could not be shown to be pure.
A spike settled where exactly it broke:
RECV .entry auf HashMap[&str, Stats] ← the arguments are there
RECV .and_modify auf Entry ← and here they are goneThe information existed at the receiver and was dropped at the result. Nothing needed to be inferred that was not already known; it needed to be carried.
$V, bound from the receiver.[fn."HashMap::entry"]
signature = "(&HashMap[$K, $V], key: ?) -> Entry[$V]"
[fn."Entry::and_modify"]
signature = "(Entry[$V], f: fn(&$V)) -> Entry[$V]"At a call site the receiver’s actual type binds the variables and they are substituted away.
HashMap[&str, Stats] binds $V to Stats, so entry hands back an Entry[Stats], so
and_modify’s fn(&$V) is a fn(&Stats), so a is a &Stats and a.add(v) resolves.
The sigil is not decoration. T, K and V are perfectly good type names, and a rule that
guessed from capitalisation would silently turn somebody’s type into a hole.
?, never a name.This is the whole safety argument, and it is why this does not contradict ADR-024 D4.
D4 erases a Nikaia function’s T to ? because “recording it as a type would make the checker
report that i32 is not T”. That is what happens to a variable which is never bound — it
survives as a name and reaches a comparison. Here it cannot: it is bound and replaced, or it is
Unknown. let m = HashMap::new() gives HashMap[?, ?], binds $V to nothing, and the lambda’s
parameter is ? — the chain simply stops helping, which is the correct failure.
Belt and braces: fits treats a variable as compatible with everything, so even a leaked one
cannot become a false rejection.
? stays for what flows in.A variable may appear in a result and in a lambda’s parameter type. It may not appear in an argument.
This is not caution, it is a distinction. What flows out is a promise this file makes, and a
wrong one is wrong on the ledger’s own account. What flows in is a constraint on somebody’s
program, and Rust’s collections deliberately accept more than their type parameters suggest:
HashMap<String, V>::get takes anything the key borrows as, so
counts.get(fragment) // k-nucleotide.nika:151, a HashMap[String, …]is correct and key: $K would reject it. Rejecting a correct program is the one thing the
checker may not do (ADR-024), and D3 is what keeps this decision from being the thing that does
it.
So HashMap::get is (&HashMap[$K, $V], key: ?) -> $V: the result is claimed, the argument is
not.
No binding from arguments, no matching against nested patterns, no constraints. The receiver is the signature’s first parameter where there is one, and that is the only place a variable is bound.
The narrowness is the decision rather than the implementation. This is the first inference in the ledger’s type language — everything before it was vocabulary — and an inference engine grows: bind from an argument, then unify two candidates, then carry constraints. Each of those wants its own reason, and drawing the line here means the next one has to be argued for rather than arriving as a refactor.
The view flag is deliberately not compared when binding: a signature writes the receiver the way
the method takes it (&HashMap[…]) and a caller holds it however it holds it, so requiring the
two to agree would make every &-taking method fail to bind.
Strip every sync declaration from each example that has one, rebuild, count how many of those
exact entries come back on their own:
| example | ADR-027 | ADR-028 | ADR-029 | this |
|---|---|---|---|---|
1brc.nika |
4 / 7 | 5 / 7 | 5 / 7 | 7 / 7 |
access-log.nika |
3 / 6 | 4 / 6 | 4 / 6 | 6 / 6 |
k-nucleotide.nika |
2 / 2 | 2 / 2 | 2 / 2 | 2 / 2 |
n-body.nika |
0 / 3 | 3 / 3 | 3 / 3 | 3 / 3 |
| total | 9 / 18 | 14 / 18 | 14 / 18 | 18 / 18 |
Every sync written by hand in this repository is now something the compiler works out for
itself. The keyword is what Part II 12.1 says it is since ADR-027 — an assertion you write where
you want a property held — and no longer something a program has to carry to be usable.
Corpus-wide, 21 of 43 functions are sync, up from 20. The four that moved are the four that
were named as open, and the rest of the gap is main and friends, which do I/O and should not be
sync.
Full unification. Bind from arguments, match nested patterns, propagate. It is the natural
next step and there is no case for it yet: D4’s one pattern answers every entry std has. The
first entry that needs more is the argument for more.
Variables in arguments too. 18 of 18 without them, and k-nucleotide.nika:151 is the program
they would have broken. D3.
Make Entry carry its type by naming it Entry[V] in Rust terms and inferring from that.
The compiler does not read Rust. That is the premise the whole ledger rests on.
Infer the variables rather than writing them. For std there is nothing to infer from — the
bodies are Rust. This is exactly the case ADR-020 D5 set aside for contracts that are written and
reviewed like code.
Let a variable be recognised by capitalisation (V rather than $V). Vec, String,
Stats and Entry are capitalised too. A silent collision here turns a type into a hole and
nothing says so.
std.contracts can describe a generic container honestly for the first time. The entries that
benefit are the ones a program actually uses: a map of structs, a list of records.?. The corpus is the guard, and a_key_may_be_given_as_something_it_borrows_as
is the specific case that would have been broken by the obvious mistake.