Status: Superseded by ADR-277 — its D1-D5 are D6, D7, D8, D9, D11 there
Date: September 15, 2026
Target Version: Nikaia 0.0.8
Related: ADR-029 D3 and D4 (sync = "from(f)" for a lambda
run during the call, and its limit), ADR-094 D2 (the keeps
inference this reuses), ADR-027 (a sync written is an
assertion), ADR-018 (what a handler is given and gives back),
ADR-069 D1 (http is a package, which is why a package has to
be able to say this), ADR-055 (the emitted async)
A parameter may not be a function. The type grammar has a name, a view, type
arguments and ?, so fn route(path: &str, handler: fn(Request) -> Response)
is a parse error, and the eight std entries that take a lambda are written
straight into the ledger where the grammar never sees them. A second author
cannot write route, retry, sort_by or a panic hook.
Two things have to be said about a parameter that is code, and the language
already says the first. A lambda the callee runs during the call — map,
filter, access — adds nothing to the caller’s own answers: the caller has
counted its lambda’s calls already, so the callee’s sync is the lambda
decides (ADR-029 D3). A lambda the callee keeps — a router
stores the handler and calls it per request from listen — runs where
nobody counted it, so that rule cannot apply (ADR-029 D4) and
nothing else says what the stored code may do.
fn(A, B) -> R is a type, written the way a signature is written.Parameters in parentheses, -> R where there is a result, and sync and
throws after the result, in the positions a declaration puts them:
fn route(&mut self, path: &str, handler: fn(Request) -> Response) // may pause
fn on_tick(&mut self, handler: fn() sync) // never pauses
fn load(&mut self, reader: fn(Path) -> Bytes throws) // may fail
A function type may stand wherever a type may: a parameter, a struct field, a result.
Without sync the function may pause; with it, it never does. Without
throws it cannot fail; with it, it may. That is the reading a declaration
already has, applied to a type.
A lambda that does less fits a type that allows more: one that never pauses
goes where pausing is allowed, one that cannot fail goes where failing is. The
other direction is refused here, in the shape ADR-027’s
NK2202 has — a pausing lambda handed to a fn() sync is NK2206, a
failing one handed to a type without throws is NK2606 — because a
declaration that says sync is an assertion and a type that says it is the
same assertion made about somebody else’s code.
The same analysis that decides whether a value is a view or kept (ADR-094 D2), asked of a parameter that is code:
sync, throws and touches are from the lambda, as they are
for map today, and the lambda borrows what it captures (Part I 5.4 A).listen
calling a stored fn(Request) -> Response is a call that may pause, so
listen may pause; calling a stored fn() sync is a sync call. The
lambda moves what it captures (Part I 5.4 B), and a shared handle is
duplicated (ADR-040 D1).Nothing is written for it. @detached was never a word a program writes and
stays that way: the ledger records which of the two a parameter is, from the
body, the way it records keeps.
The type carries sync and throws and no more. A stored handler’s
touches is everything and its locks is may, the fail-closed answers
the ledger gives an undescribed call, so an overlap branch that calls a
stored handler meets every other branch and a door may not call one. A run
lambda is unchanged: its body is in front of the check.
A parameter whose type may pause lowers to a closure returning a boxed
future, run or kept — the shape a handler is taken in practice, and the one
task::interleave already takes; a parameter whose type says sync lowers to
a plain closure (ADR-122). A kept parameter is boxed as well,
because it is stored. Where the type says throws, the closure’s result is
the Result a throws function’s is.
examples/http/ can declare route, and examples/fortunes.nika’s main
is a program the package can accept. A panic hook, a supervisor’s task, a
comparator and a retry are things a package can take.
What a library author writes is the type, and the type is the contract:
a caller who hands over a pausing handler where the signature says sync is
told so in this compiler’s words, where today the same program is refused by
rustc about a file nobody wrote.
The trait door is a separate question. A Handler trait held in a
struct works within a file; a bound that names a trait in another package
does not parse, and that is a namespace question rather than a function-type
one. It stays on open-decisions.md, narrowed to that.
touches. D4 fails closed; a
stored handler that provably touches one file is treated as touching
everything. A spelling for less would be a type saying more than
sync/throws, and no program has asked.fn[T](../../specification/adr/T) -> T. Not written
anywhere.fn apply(f: fn())
that only calls f gets from the lambda by D3; a wrapper that stores
and runs gets the kept answer, which is the safe one.Step 1. fn(A, B) -> R sync throws is a type in the grammar, in the
ledger’s type language, and in the lowering. The parameters go where a tuple’s
parts go — ast::Type puts them in generics, so everything that walks a
type’s arguments walks them without knowing what this is — and what is beside
them is the part a tuple has no room for: the result and the two promises. The
ledger renders and parses the whole spelling and round-trips it, a function type
inside another one included, which is why the closing parenthesis is counted
rather than looked for at the end.
D2’s reading is in the fit, and step 2 says it in words: NK2206 for a
lambda that pauses where the type says sync, NK2606 for one that fails where
the type declares none. Each is the shape of the refusal one level down —
NK2202 and NK2605 — because a type that says sync is the same assertion a
declaration makes, made about somebody else’s code. The answer comes from what
the body’s calls say in the ledger, so a callee nothing describes leaves it
unasked (Part III C.4).
NK2606 is the whole message. The function around the lambda is not the
one that has to answer for a failure the type refuses, so NK2605 — this
function can fail because … — does not stand beside it; where the type does
say throws, the failure travels to the caller by ADR-029 D3 and
NK2605 is right again. Two messages for one mistake, one of them pointing at
the wrong function, is what that costs if it is not said.
What step 2 needed first, and it was ADR-029’s own ordering. A
free call walked its arguments before it resolved its callee, so a lambda
handed to one reached the checker with no signature behind it: hand(fn(n) { …
}) left n with no type at all, and the promises had nothing to be asked of.
The method path was given that ordering when ADR-029 landed and this one was
not. It has it now, which types a free call’s lambda parameters as well.
Step 3. Which of D3’s two cases a code parameter is, is inferred, and the
ledger says so: a parameter the body runs gives the function
sync = "from(f)" — the lambda decides — and one it keeps is answered
from the type, so a kept fn() sync cannot pause and a kept fn() takes the
claim away. A body that stores and runs gets the kept answer, which is §4’s
own sentence and the safe one. Until this, a function that took a lambda had to
commit to the pessimistic answer for every caller: twice lowered to an
async fn that every call awaited.
Sync::From is an outcome of inference now, where before only a written
std entry produced one. It is sound for the reason ADR-029 D3
gives and for one fact of this compiler: visit_expr_blocks walks the body of a
lambda passed as an argument, not only a trailing one, so every lambda a
caller writes is counted in the caller whichever parameter the column names.
That is also why a body running two code parameters is sound with one name
recorded — the name is what a reader and a second build need, and the soundness
is the caller’s walk.
Run-or-kept is asked here rather than read off keeps, which is what D3
names, and the reason is an ordering: keeps::infer runs after this pass.
What is asked instead is the column’s own question in the small — the name is
mentioned, and every mention is the callee of a call. It fails closed, which
is the direction a greatest fixpoint has to fail in (ADR-010 D1).
The lowering is D5’s run case, a closure argument: impl Fn(A) -> R, and
-> Result<R, …> where the type says throws, which is the same Result a
throws function’s own declaration has. A kept one — a boxed closure over a
boxed future — is not built, and the positions where a function type can only be
kept (a field, a result, a let) are refused here with NK1142 rather than
handed to the language below, where impl Fn(…) in a field is not Rust and the
answer would be about a file nobody wrote (Part III C.1).
One thing the record had not said, and the grammar had to settle it. The
trailing words are greedy: in fn make() -> fn(i64) -> i64 sync the sync
belongs to the result type.
And the way out this paragraph named is gone. It said a function whose own
promise is meant writes it before the arrow, and
ADR-140 D4 takes that form out of the language so that a
declaration and a type read the same way round. What it costs is a spelling for
a shape nothing can write: a function type in a result is NK1142 until D5’s
boxed lowering exists, so no program is waiting on it — and D5 is the record that
owes one the day it lands.
The prerequisite it named is no longer one. This said “no keeps
inference exists for any parameter”, and ADR-094 §5’s first
step landed the same day: contracts::keeps infers the column over the call
graph and the ledger records it. What step 3 below adds is asking that
inference about a parameter whose type is a function — the same question
one level over, rather than the question itself.
The order of work:
fn(…) for std — built;keeps — built, and asked in
the small rather than shared, for the ordering reason above;NK1142 stands in
front of.#181 carries the remainder.