Nikaia
Menu
v0.0.1343pre-alpha GitHub

ADR-288: sync Means a Function Never Pauses — Earned From the Body, Decided by a Lambda Where One Runs, Promised Across Packages Only Where Written

Status: Accepted Date: October 3, 2026 (D11 clarified: October 5, 2026) History: the records this one replaces are archived in docs/history/adr; read them only for how the decision was reached Answers: whether sync is typed or inferred, and in which direction an inference that cannot see a call fails; how the inference learns where a method call goes without a second type checker; how a higher-order function’s sync can depend on its lambda — effect polymorphism; how a library signature says the V of the receiver; what sync promises — pausing only, or also I/O — and how touches is filled; whether a trait method may pause, and what Rust that needs; and what a pub function promises about pausing to another package Related: ADR-020 — the ledger the inference writes to, and D5: a library written in another language writes its contracts and reviews them; ADR-010 D1 — an analysis that fails open is a vulnerability generator; the same polarity answered here; ADR-024 D4 — a generic parameter is erased to ?, and why a bound variable is not that; ADR-292 D3 — the touches column and its fail-closed polarity; ADR-281 D28-D30 — a lock inside a lock, and the lock-touching property built on touches; ADR-055 — the lowering: a function that may pause is an async fn; ADR-100 — a consumer reads a dependency’s ledger and never derives it; ADR-277 D7, D8 — a function type reads like a declaration; run or kept is inferred; ADR-297 D10 — the panic hook must be sync and may block; ADR-305 — the Rust floor, measured; ADR-251 D3, D4 — sync’s three written states, and the ledger’s Nikaia spelling

1. Question

What does sync promise, who decides that a function has it, and whom can a caller believe?

sync is the gate on every safe concurrency construct in Part II 12: a lock’s access, update and access_all, a par_iter lambda, a scope’s parallel tasks, the panic hook. A rule that only says a sync function calls only sync functions leaves five things to decide:

Without an answer the restrictive side of the language is the unusable one: under opt-in sync, putting bonus(score) — two integers added — inside access meant annotating it, everything it calls, and nothing one did not own.

2. How others do it

The comparisons are mostly against the language’s own neighbouring mechanisms and against Rust, which is the language below.

Language / mechanism Its answer What it costs there Source
Rust, async fn in traits stable since 1.75, with return-position impl Trait; the sugar warns (async_fn_in_trait) on a public trait whose future has no Send bound the trait’s author must choose the Send bound; a trait with an async method is not object-safe D26
Rust, HashMap<K, V>::get takes anything the key borrows as, not K a signature written key: K would reject correct calls D19
Nikaia’s provenance (ADR-010 D1) where it cannot be established, the answer is Untrusted fewer values are trusted than could be D2
Nikaia’s throws the word is written on the signature; only the set of errors is inferred, its growth reported at every catch (NK2402) the author writes throws §3
Nikaia’s returns = "borrows(a \| b)" a ledger already said depends on a parameter for borrows — D15
std.contracts, written by hand each entry says sync = true, the lambda form, or nothing (read as pausing); none "inferred" every entry is reviewed like code D11, D12

What does not transfer: a language whose async is visible in the type (Rust, C#) colours functions; Nikaia’s promise is that it does not, so the question here is not async or not but may this be put where pausing is forbidden.

3. Options, weighed

Question Option rejected Why it lost
where sync comes from keep it opt-in the annotation chain makes every lock and par_iter body unusable; it trains put less inside the lock for the wrong reason
an unresolvable call infer, and treat it as harmless the entry ships; a wrong sync is a pausing body inside somebody else’s lock, with no diagnostic anywhere
  infer, and warn where undecided every method call in every program, for a question most callers never ask
the keyword drop it now that bodies are read it is the only override for what the inference refuses, and the only way to hold a function to the property on its next edit
the ledger one sync = true for both origins a withdrawn assertion and a lapsed inference would print the same line
throws infer it the same way sync is a permission, throws an obligation; deriving throws silently changes what callers must write
method calls give sync.rs its own receiver types a second type checker obliged to agree with the first
  write std contracts for everything Rust has a wrong entry rejects a correct program, and every entry is a claim someone reviews
higher-order methods mark and_modify, map … sync = true a promise about code the ledger has never seen
  work out the effect at each call site, record nothing no answer across a package boundary, which is what a ledger is for
the function type give it a result in the ledger too no entry needs one; in the source ADR-277 D6 writes -> R
type arguments full unification; variables in arguments; capitalisation instead of a sigil no entry needed more; counts.get(fragment) would be rejected; Vec, Stats and Entry are capitalised too
what sync means take println out of sync costs the panic hook, which must be sync and must write a crash report, and makes every printing function async for a suspension that does not happen
a third word pure or repeatable beside sync and touches none of the consumers needs more than no effect; a word carrying two promises is how this went wrong
packages classify a ledger diff as breaking the same change breaks some callers and not others, and the author cannot see the callers
  publish an inferred lambda form, write nothing a log line in the body withdraws it at the consumer’s upgrade, with no word the author could write
  leave the lambda form unwritable too weak for a par_iter caller, or refuses every pausing lambda
  lower an unpromised callee as pausing too every call into a package whose author forgot a sync would build a future

The weights that decided, in the words of ADR-258: an analysis that claims a property fails closed (the special case pays — D2); the compiler reads the body so the developer does not write a chain (D1); a promise across a package is what the author wrote, and costs nothing at run time (D28, D30).

4. Decision

D1-D6 make sync inferred; D7-D12 let the inference see through method calls; D13-D16 through a lambda; D17-D20 through a container’s type arguments; D21-D23 say what the word means and fill touches beside it; D24-D27 apply it to traits; D28-D32 say what crosses a package.

D1 — sync is inferred from the body, for every function.

A function is sync when every call it makes resolves and every callee is sync. The inference runs over the call graph of the unit after the ledger’s entries exist, resolving into a library’s ledger as the check does. The fixpoint is a greatest one: start from every candidate is sync and take the claim away from anything that reaches a function without it — which is what makes mutual recursion between two pure functions come out sync.

D2 — The inference fails closed; the check never rejects what it cannot see.

A call the compiler cannot resolve costs the function its claim: a name no ledger knows, a spawn, a dsl’s action blocks. The check of a written sync and the inference share one resolution rule; where they differ is only what an unresolvable call means. A source that asserts sync and calls something no ledger knows is refused (NK2202) rather than keeping an assertion nothing could check, because the ledger ships.

D3 — The ledger records which of the two it is.

sync = true where the source wrote it, sync = "inferred" where the body implies it, absent where neither. Inside a package a caller reads both as cannot pause; a diff tells them apart, because withdrawing an assertion is a decision and losing an inference is a consequence elsewhere. (Across a package the two are read differently: D28.)

D4 — An assertion is never overwritten by the inference.

Where the source says sync, the inference leaves it, including where it could not have derived it. The keyword is an assertion you make, not a mode you enter: it holds a property, and NK2202 reports what contradicts it. It changes nothing in the generated program.

D5 — The header of the derivation names the change.

A ledger whose sync was read off bodies says so in its inference header, so a regenerated ledger shows the toolchain moving rather than the code. The header lives in nikaia.derived beside the contract.

D6 — --locked names the entry a changed line belongs to.

A --locked diff prints whose contract moved, not a bare sync = true.

D7 — The type checker records where each method call went.

The checker’s result carries, per function, the keys its method calls resolved to and whether any did not resolve. The inference reads that answer instead of inferring receiver types itself: the module with the types answers the questions about types (ADR-025 D7 was the first instance).

D8 — Ledger::infer runs the checker, in a fixed order.

Read the declarations; run the type checker against that ledger; infer sync from the bodies using both. The checker reads signature, fields and iterates, never sync, so step 2 does not depend on step 3 — an invariant held by a test that runs the checker against both ledgers and compares.

D9 — A written sync is contradicted at the call.

A diagnostic has a caret on a call (Part III C.2), so the contradiction of a written sync is reported where the pausing call stands: a free call resolved by name, a method call by the type checker (Part III, NK2202). A per-function answer was never allowed to stand in for one.

D10 — Indexing a container has a type.

Vec[T] and List[T] indexed yield T; HashMap[K, V] yields V; anything else, text included, still claims nothing.

D11 — std.contracts describes the collections and text the language below provides.

Vec, HashMap, str, String, f64 are Rust’s; their contracts are written and reviewed (ADR-020 D5), never copied from Rust’s whole surface: a missing entry only fails to help, a wrong one rejects a correct program. Types are ? where there is no one answer; arity is claimed and checked.

This is a rule for how an entry is made, not for what the language offers. What std provides is the specification’s decision, taken from what the language is for, from the coherence of its own types - a buffer whose content cannot be read is not a buffer - and from what other languages count as the basic surface of a type. It is never taken from what the programs in this repository happen to call: they are the compiler and a handful of examples, not the programs the language is for, and a gap they do not hit is still a gap.

D12 — A higher-order entry claims no sync of its own.

A function that runs a caller’s lambda does not say sync = true: that would be a promise about somebody else’s code. It says the lambda decides (D15).

D13 — The type language has a function type.

Changed by ADR-251 D4: the ledger spells it as Nikaia does, so a lambda handed a view is fn(ref Stats).

fn(ref Stats), fn(), fn(ref str, i64) say what a lambda is handed. A program writes the same type in its source, with a result, sync and throws, as ADR-277 D6 decides.

D14 — A lambda’s parameters get their types from the callee’s signature.

The checker resolves a call first and walks its arguments after, handing each the type its parameter expects; an implicit lambda’s a, b, c are bound in order to what the signature says it is handed.

D15 — sync(f) says the lambda decides.

The fourth state beside true, "inferred" and absent names the parameter whose lambda decides; the ledger spells it sync = "sync(f)". A caller reads it as this call adds no pausing of its own, which is sound because the lambda runs during the call, so its body is the writer’s and already counted. The rule is sync’s alone: throws needs no such key (the error set is grown by the same walk), and touches would need the opposite instruction — add what the lambda reaches.

D16 — The lambda form is for an immediate lambda only, and std is held to it.

A parameter the callee stores or spawns breaks D15’s reason: its calls belong to nobody the caller counts. A test walks every such entry in std.contracts and requires it to name a function-typed parameter. For a program’s own function, whether a parameter is run or kept is inferred (ADR-277 D8), and naming a kept one is refused (D31).

D17 — A signature may name its receiver’s type arguments.

HashMap::entry is [K, V](mut self: ref collections::HashMap[K, V], key: ?) -> Entry[V], and Entry::and_modify hands its lambda a fn(ref V). At a call the receiver’s actual type binds the variables and they are substituted away: HashMap[ref String, Stats] makes a in and_modify fn { a.add(t) } a ref Stats. A variable is declared, never guessed from capitalisation.

D18 — An unbound variable becomes ?, never a name.

A variable is bound and replaced, or it is ?, so it never reaches a comparison — which is why this does not contradict ADR-024 D4. fits treats a variable as compatible with everything as a second guard.

D19 — A variable says what flows out; ? stays for what flows in.

A variable may stand in a result and in a lambda’s parameter type, not in an argument of a std entry: Rust’s collections accept more than their type parameters suggest (counts.get(fragment) on a HashMap[String, …]), and rejecting a correct program is the one thing the checker may not do.

D20 — Binding is one structural walk, without unification.

The receiver binds, positionally; a free function’s arguments and a struct literal’s fields bind its written type parameters (ADR-295 D2). No constraints, no queue, no fixpoint; the view flag is not compared when binding. A wider inference is a decision of its own.

D21 — sync promises one thing: the function never pauses.

It does not promise that the function has no effect. println is sync: it writes and returns, and never suspends. A panic hook is sync and may block. What a function reaches is a second question with a second column, touches. A name in this language answers one question.

D22 — touches is inferred from the body, like the columns beside it.

A greatest fixpoint over the same call graph, starting from touches nothing. The polarity is the column’s own (ADR-292 D3): a call nothing describes, a construct that runs something, or a callee whose set is nobody said leaves the caller unknown, and no fixpoint brings the claim back. An empty set is an answer; an absent one is not. A resource named by a callee’s parameter (file(path)) does not travel to the caller: such a callee leaves the caller unknown.

D23 — A lock is a resource, and lock is in the vocabulary.

It names no parameter: the property says a lock and never which (ADR-281 D30). get, access and access_all are reads and do not conflict; set, update and update_all are writes.

D24 — A trait method reads like a function type.

Without sync it may pause; without throws it cannot fail. The ledger’s trait entry records the words as written, and a call through a bound pauses where the declaration may.

trait Source {
    fn load(ref self) -> String throws     // may pause, may fail
    fn name(ref self) -> String sync       // never pauses, cannot fail
}

D25 — An implementation is checked against its declaration.

A body that pauses under a sync declaration is NK1129; one that fails under a declaration without throws is NK1140. A body that does less than the declaration allows fits. An implementation is lowered async where its declaration may pause, whether or not its own body does — an edge in the inference’s graph, drawn only where the trait is declared in this package’s or a dependency’s ledger.

D26 — The emitter writes the return-position form, and Send follows the executor.

In the trait, a method that may pause is fn load(&self) -> impl Future<Output = String>, + Send at user_parallelism = yes and without it at no; the impl writes async fn. This is the executor’s requirement, not a claim about a type (ADR-312).

D27 — The Rust the emitted code needs is one constant, written where Cargo reads it and checked first.

Every generated Cargo.toml carries rust-version from one constant in the emitter (RUST_FLOOR), and the compiler compares it with rustc --version before cargo runs, refusing in its own words. The channel stays rust-toolchain.toml’s (ADR-001 D1). The floor rises only by a record. The number is 1.88, measured, for the compiler, std and the emitted code alike.

D28 — A consumer in another package reads "inferred" as absent.

Across a package boundary a pub function is sync only where its source writes sync or sync(f). Inside the package nothing changes. So the published promise is what was written, may pause is the default, and no change to a body can widen what was promised. The polarity is the opposite of throws, on purpose: pausing harms only the callers in a sync function, a lock’s door, a par_iter lambda or a sync trait method’s body.

D29 — The author is told which pub functions could promise sync and do not.

A build names, as a note, the package’s pub functions whose entry says "inferred", with sync as the word to write, and those whose only pausing is a lambda’s, with sync(f).

D30 — The check reads the promise; the lowering reads the body.

A call into another package is checked against D28 and lowered by what the callee’s body is, so D28 costs nothing at run time. A caller whose only pausing call is an unpromised callee may pause to its own consumers.

D31 — sync(f) in the source promises that a function pauses only where its lambda does.

pub fn apply(f: fn(i64) -> i64, x: i64) -> i64 sync(f) {
    return f(x)
}

It stands where sync stands and names the function’s own parameters, sync(f, g) for several. In the body a call to f is allowed and nothing else may pause (NK2202); at a call, the call is sync where the lambda handed over is. Only an immediate parameter may be named; a name that is no parameter, not a function, or kept is NK2210. A sync parameter type with a plain sync on the function is the stricter contract, refusing every pausing lambda (NK2206).

D32 — The author is warned when a pub function loses the sync it had.

Where the committed ledger says "inferred" for a pub function and the build finds that it can now pause, the build warns (NK2211) at the statement that made it, with the calls that lead there. Committing the ledger acknowledges it.

5. Consequences

6. What this does not decide

This site is open source. Improve this page.