Status: Superseded by ADR-288 — its D1-D4 are D13-D16 there
Extends: ADR-027 §7, which named effect polymorphism as the
larger version of the problem, and ADR-028 D6
Related: ADR-024 (? is the absence of a claim),
ADR-020 (the ledger’s type language this widens),
ADR-031 (closes §4)
ADR-028 gave std’s higher-order methods signatures so that the type checker could resolve
through them, and deliberately gave them no sync:
Entry::and_modifyandEntry::or_insert_withrun the lambda they are given. Whether they pause depends on what is in it, and a ledger cannot say “it depends” yet.
That was honest and it was expensive. A ledger entry has to hold for every caller, so a function
that runs somebody else’s code has to commit to the pessimistic answer — and the pessimistic
answer propagates. xs.sort_by_key fn { a } cannot pause by any reading of it, and the compiler
had no way to know:
error[NK2202]: `im_lock` is `sync`, and `ordne` can pause
9 | return ordne(xs)
= `ordne` carries no `sync` in this program's contractsordne sorts a list by a key. That is a correct program being rejected, which is the one
thing the compiler is not allowed to do, and it was not a bug in either analysis: both were
reading a contract that said what it had to say.
The effect is worse than one message, because of what sync gates. access, access_all,
par_iter and a scope’s parallel tasks all demand a sync lambda (Part II, 12.2). So
“no higher-order function is sync” reads, at the place it bites, as “no map, filter,
fold or sort_by_key inside a lock” — over any lambda at all.
fn(…).Ty::Fn { params }, written fn(&Stats), fn(), fn(&str, i64). It says what a lambda is
handed; what it hands back is deliberately absent, because nothing needs it and a spelling
is easier to add than to change.
Only a ledger writes one. Nikaia’s grammar has no syntax for a function type — fn f(g:
fn(i32)) is a parse error today — so no .nika source can declare a parameter of this shape.
That is worth stating because it closes a hole rather than leaving one: a function that took a
lambda and passed it on would need its own effects to follow its parameter, which is real
polymorphism and is not what this ADR does. The grammar makes the case unreachable, and the day
it does not, this paragraph is where the gap is recorded.
The checker walked a call’s arguments before resolving the callee, so a lambda was walked with nothing known about it. It now resolves first and walks after, handing each argument the type its parameter expects.
The implicit form is the one that needed this and the one that could not have it: fn { a.add(t) }
records no parameters at all in the AST, because Part I 5.3 settles how many arguments a
lambda takes from which of a, b, c its body mentions, and that is decided when it is
emitted. So the names are bound here, in order, to whatever the signature says the lambda is
handed.
sync = "from(f)" says the lambda decides.A fourth state beside true, "inferred" and absent, naming the parameter that decides — the
same shape returns = "borrows(a | b)" already uses for “depends on a parameter”, which is why
it needed no new grammar in the file.
A caller reads it as “this call adds no pausing of its own.” That is sound for exactly one
reason, and the reason is worth writing down because it is not obvious: the lambda runs
during the call, so its body is part of the function that writes it, and that function’s own
analysis has already counted its calls. from adds nothing because there is nothing left to
add.
Which bounds the columns that may say it, and the bound is not D4’s. Beside immediacy the
reason needs a second premise: the analysis reading the contract must ask about a whole
function, because only then is “already counted” counted where the contract is being read.
throws meets it — the error set is grown by the same walk, so a lambda’s failures are already
in the enclosing function’s set, and a throws = "from(f)" would have nothing to add and could
only weaken the "?" a method call already earns.
ADR-033’s touches does not: its consumer asks what a statement reaches,
nothing reads a lambda for an effect, and “adds nothing” there would buy an overlap on an
incomplete touch set — two printlns free to interleave, which is the polarity
ADR-010 D1 forbids and D4’s immediacy does not rescue. So this is one rule and
not three: throws needs no key, and touches would need the opposite instruction — add what
the lambda reaches, and everything where it cannot be read — under a word that does not look
like this one. The programs that settle each are in
docs/history/from-for-throws-and-touches.md.
from is for an immediate lambda, and std is held to it.The corollary of D3’s reason is its limit. A parameter the callee stores or spawns — Part I
5.4’s @detached — breaks it: the lambda’s calls belong to nobody the caller is counting, so a
pausing body would slip into a lock with the ledger saying it could not.
The ledger cannot spell @detached, so the rule is enforced rather than assumed:
a_detached_lambda_may_not_use_from walks every from entry in std.contracts and requires
that it name a parameter which is a fn(…). std has no detached parameter today; the day it
gains one, from needs a companion and that test is where it is noticed.
ADR-027 and ADR-028 were measured by stripping every sync declaration from the examples and
counting what came back. On that measure this ADR changes nothing: 14 of 18, before and
after. Counting how many functions in the whole corpus are sync gives the same answer: 20 of
43, unchanged.
That is not a disappointing result to be explained away. It is the result: no program in this
repository is unblocked by it. The four functions still open (Summary::{record, merge},
Report::{record, merge}) are blocked by something else, named in §4, and every other
higher-order call in the corpus sits in a function that does I/O anyway.
What the change does is remove a false rejection, and the smallest program that shows it is the measurement:
fn ordne(xs: Vec[i64]) -> i64 { xs.sort_by_key fn { a } return 1 }
fn im_lock(xs: Vec[i64]) -> i64 sync { return ordne(xs) }Before: NK2202, ordne can pause. After: it compiles, and ordne is sync = "inferred".
That program is now a test.
So the case for this ADR is not a number on the current corpus. It is that the corpus is eleven mostly parser-driven programs and the rule it removes — no iterator method inside a lock — applies to a category rather than to a program. A reader who wants a measured crossover before believing a change is right to want one, and should know that this one does not have it yet.
The four remaining functions are all this:
self.stations.entry(m.name).and_modify fn { a.add(m.temp) }D2 types a from and_modify’s signature, and and_modify’s signature says fn(?). It cannot
say fn(&Stats), because Stats comes from the type argument of the map — HashMap[&str,
Stats] — and the signature language has no type variables. ADR-024 settled that a generic
parameter is recorded as ? for a Nikaia function whose generics are erased; a hand-written
library contract that wants to say “the V of the receiver” is a different question, and this ADR
does not answer it.
So the next question is a specific one: may a std.contracts signature refer to its
receiver’s type arguments? It is worth about four functions here and rather more in any
program that uses a map of structs. It is also the first thing in this file’s history that would
add inference to the ledger’s type language rather than vocabulary, which is why it gets its
own decision.
Mark the higher-order methods sync = true and move on. 18 of 18 on the measure, and a
promise about code the ledger has never seen. ADR-027 §2 exists to prevent exactly this.
Work out the effect at each call site instead of recording it. The ledger would say nothing and the inference would look at the lambda. It is the same answer by a longer route for a program’s own code, and no answer at all across a package boundary — which is what a ledger is for.
Give the function type a result as well (fn(&Stats) -> i64). Nothing needs it: the sync
question is about what a lambda does, not what it returns, and map’s own result is ?
anyway. Adding an unused half to a spelling makes it harder to change later.
Infer from rather than writing it. For std it cannot be inferred — the bodies are Rust.
For Nikaia code it could, the day a Nikaia function can take a lambda at all, and that day the
question is whether the parameter is immediate or detached (D4) rather than whether it is a
lambda.
sync promise, so the
constructs in Chapter 12 that demand one are usable with the standard library rather than
around it.Sync is no longer Copy — From(String) carries a name. A handful of call sites take it by
reference; nothing about the file format or the reading of it changed.