Open and answer this issue on GitHub.
ready · opened 2026-10-14 · updated 2026-10-15 · 8 comments
In Nikaia a function says only throws. What it can fail with is inferred by the compiler from its body, across the whole program, and written to the ledger (Part I 7.1: “throws names no types. What a function can fail with follows from its body.”). In a catch, error is “the sum of the errors that can arrive at this point, as the compiler inferred them”. Since ADR-345, process::exit is one of them: the fatal error process::Exit.
A function can also be a value: handed to a parameter, stored in a field, a list, a supervisor::Child, or a server’s handler.
enum Bad { Oops }
impl Error for Bad { fn message(ref self) -> String { return "oops" } }
struct Job { run: fn() throws }
fn fail() throws { throw Bad::Oops }
fn now(f: fn() throws) throws { f() }
fn main() {
now(fail) catch { match error { Bad::Oops => println("immediate") } } // compiles: the set arrives
let job = Job { run: fail }
job.run() catch { match error { Bad::Oops => println("kept") } } // refused
}Part I 5.4 C draws the line between the two: “For an immediate parameter the lambda’s touches and throws count for the callee […]. For a kept parameter the callee’s promises follow the type.” A kept function value is just fn() throws, “can fail with something”. The inferred error set is dropped where a function value is kept.
The owner, 2026-10-14, while reading #605’s item 5 (a catch written directly on supervisor::run). The decision basis there recommends wrapping a child’s fatal error in supervisor::Handed (Java’s ExecutionException model), because a child’s error set is not known: ADR-346 §5, D7: “The hand-over is a type of its own because run’s channel is typed and a child’s is not.” The owner’s view: a language meant for formal proofs must not throw away on the way what it inferred, all the more since the ledger keeps so much at every function boundary. This issue is the question behind #605’s item 5, and #605 is blocked by it.
Something concrete needs the answer: #605’s last open item, the defect below, and every std entry that keeps a function.
error in a catch is their sum. Not touched here.TaskHandle carries its body’s error set and join throws it. D7 did not do the same for supervisor::Child.sync, the ledger already carries a property through function values: 27 entries in std.contracts say sync = "from(f)" or sync = "sync(f)". For throws there is no such form; not one entry has it.1. The checker puts a kept function’s errors at the wrong place. The program above:
error[NK2605]: This function can fail, because `fail` can fail.
--> a.nika:16:5
16 | let job = Job { run: fail }
error[NK1134]: Nothing here can fail, so the `catch` has nothing to handle.
--> a.nika:17:5
17 | job.run() catch {Storing fail is counted as a failing call. The actual call, job.run(), is counted as unable to fail, so its error cannot be caught at all. With main() throws and no catch, the program runs and ends with Error: oops: the runtime hands the error on in the box; only the checker’s view is wrong. This is a defect under every option below.
2. std entries that keep a function, and where their errors go:
| Entry | Contract | The kept function’s errors |
|---|---|---|
supervisor::child(body: fn() throws) |
keeps = ["body"] |
restart policy; a fatal one becomes supervisor::Handed (ADR-346 D7) |
net::serve(address, handler: fn(net::Connection) throws) |
keeps = ["handler"], throws = ["io::IoError"] |
net.rs said(): eprintln! and dropped. A fatal Exit from a handler sets no exit status, against ADR-346 D1/D6 |
task::Scope::spawn(body: fn() throws) |
sync = "sync(body)" |
handed on by the scope (ADR-346 D7, 0.0.915) |
task::scope(body: fn(ref task::Scope) -> T throws) |
throws = ["task::Crashed"] |
the tasks’ errors travel in a box |
SharedMut::supervised(build: fn() -> T sync) |
no throws |
cannot fail |
3. Two runtime registries exist because the types were dropped:
process.rs FATAL (0.0.906): main registers which types are fatal, so a box can tell at run time.task.rs CROSSING (0.0.909): main registers which error types may cross threads as themselves.Both answer at run time a question the compiler had answered and then forgot.
From memory (m); to be checked before an ADR quotes it.
| Language | A function value’s error type | Kept (stored) functions |
|---|---|---|
| Java (m) | checked exceptions are written by hand; java.util.function interfaces declare none |
lambdas that throw are wrapped in unchecked exceptions; a generic throws E carries one type only. The typical failure of hand-written effects |
| Swift (m) | rethrows for a parameter called at once; typed throws throws(E) (Swift 6) is generic |
throws(E) is part of the closure’s type, so a stored closure keeps it |
| Rust (m) | the error is in the result type, impl Fn() -> Result<T, E> / Box<dyn Fn() -> Result<T, E>> |
the type keeps E; a list of mixed closures needs one E (an enum or a box) |
| Koka (m) | effect rows, inferred and polymorphic | a stored function keeps its row; a list of them has their union |
| Kotlin, C# (m) | unchecked; nothing in the type | nothing to keep |
Java failed because the sets had to be written. Nikaia infers them, so its cost is the one Koka pays: sets that travel through types.
A — As today: a kept function is “can fail with anything”. Fix defect 1 so job.run() counts as failing with ? and a catch with else is allowed. Pro: small. Con: a catch over a kept call is never exhaustive; Exit cannot be seen statically; Handed and both registries stay; net::serve’s lost fatal error stays a run-time special case. Worst case: the compiler cannot prove what it could have proved: a missing proof, not a wrong value.
B — A function value’s type carries its inferred error set, kept or not. fn() throws in source still names no types; the compiler infers the set at each value (a named function, a lambda) and carries it through let, fields, lists, maps, returns and parameters. A container of functions with different sets carries their union, the same sum 7.1 already builds for a catch. A pub entry that keeps a function says so in the ledger as it does for sync: its calls and the types that hold it throw what f throws (throws = "from(f)"-style). Pro: 7.1 holds everywhere; job.run() catch is exhaustive; #605 item 5 becomes option 1 for any list; Handed, FATAL and probably CROSSING can go; net::serve knows statically whether a handler can exit. Con: error sets become part of type identity. Two functions with different sets are different types, unified to the union where they meet. That is new checker work through fields, generics and with. A library that keeps a caller’s function needs the from(f) form across package boundaries, and a change to what a kept function throws changes a type its users see (ADR-288’s weakened-contract warning would apply). Worst case: a refusal where unification is not yet implemented: visible, not a wrong value.
C — Only std types carry it, case by case. TaskHandle (done), then Child, serve’s handler; user fields stay as A. Pro: covers today’s concrete cases. Con: two rules for the same thing; every new std type that keeps a function repeats the work; a user’s struct Job { run: fn() throws } stays unprovable.
B. It is 7.1 taken at its word, and it is what ADR-346 D5 already did for one type. The ledger has the mechanism for sync; this extends it to throws. The cost is real but of the refusal kind, and it removes two run-time registries and a wrapper type that exist only because the information was lost.
Risk of the recommendation: the unification of error sets through generic containers (Vec[fn() throws], HashMap[K, fn() throws]) is the part nobody has built yet; it may surface cases where the union grows larger than a reader expects. That is a message to design, not a wrong program.
Replace “For an immediate parameter the lambda’s touches and throws count for the callee, while … For a kept parameter the callee’s promises follow the type” with:
A function value keeps the error set the compiler inferred for it (7.1), wherever it goes: a
let, a field, an element, a result, a parameter. Calling it can fail with that set. Where function values with different sets meet, as two elements of one list or two arms of oneif, the value carries their union. For an immediate parameter the lambda’stouchescount for the callee; whether the call may pause, and the shape it is lowered to, follow the parameter’s type.
kept arm exhaustive, and under A with an else arm; NK2605 is not reported on the let.if, match, list and map literals, push, insert). Tests: a Vec[fn() throws] of two functions with different errors, a catch over a call of an element takes both by name; a list of non-failing functions is fn() and a catch over it is NK1134.throws form for entries that keep a function (from(f)), and for a pub function of a user package that keeps one. Tests across a package boundary.std: supervisor::child and supervisor::run: run throws Escalated plus the fatal members of its children’s sets; remove Handed (ADR-346 D7 amended). net::serve: a fatal error from a handler goes to the exit status as a detached task’s does (ADR-346 D6). Tests for both.process.rs FATAL where the static set answers; check whether task.rs CROSSING can go too (the Send question remains).Then #605’s item 5 is option 1, and #605 can close.
A function value keeps the error set the compiler inferred for it, called at once or kept. Recorded in ADR-351 (D1-D7). The rule is in Part I 7.1 (“A function value keeps its set”) and 5.4 C. The supervisor part is in Part II 12.8, the ledger’s from(p) in Part III 13.5, and the handler rule beside net::serve in Part III. ADR-346 D7 is changed (Changed by note, index What supersedes what). Version 0.0.929, commit 7d40c23.
In short:
let, fields, list and map elements, results and parameters (D1).if/match, elements of one list or map, values assigned to one variable or field, the arguments every caller hands one parameter), the place carries the union. A place no failing value reaches cannot fail (D3).throws member "from(p)", with p a parameter or a field path of one. The caller replaces it with what it passed. A type holding a function value carries the value’s set, as TaskHandle[T] does (D4).supervisor::run throws Escalated and its children’s fatal errors themselves. supervisor::Handed is withdrawn (D5).net::serve handler’s error is a detached task’s error: long form on stderr, and a fatal one sets the exit status at main’s end (D6)."?" stays for code no ledger describes, never for a function value (D7).Not decided: an explicit set in source (fn() throws(E)), and how a large union is shown in a message.
kept arm is exhaustive with no else, and NK2605 is not reported on the let. NK1134 over a call through a value that carries the empty set.if/match arms, list and map literals, push/insert, reassignment, fields, with, and parameters across all callers. Tests:
Vec[fn() throws] of two functions with different errors: a catch over a call of an element takes both by name;catch over a call of an element is NK1134."from(p)". Write it for a function that calls a function value it was given (parameter or field path), read it at callers, and do the same across a package boundary (nikaia describe-free, a path dependency). Also apply ADR-288’s warning when what such a function throws widens. Tests across two packages.std contracts. supervisor::child/Child carry the body’s set. supervisor::run throws Escalated plus the fatal members. net::serve’s handler and task::Scope::spawn/task::scope carry their bodies’ sets.supervisor::Handed and make run throw the child’s error. In net::serve, said() hands a handler’s error to the detached-task path (task.rs DETACHED), so a fatal one sets the status. Remove process.rs FATAL where the static set answers. Check whether task.rs CROSSING can go (the Send question remains). Tests:
exit(4): run throws process::Exit, a catch arm process::Exit takes it, and without a catch the status is 4;exit(3): the status is 3 at main’s end.The last commit of this list says Fixes #620, #605.
Generated by Claude Code
Course correction: no ? for function values (ADR-351 D7).
The owner asked whether treating a function value’s errors as open (?) is sound architecture. Checked against ADR-351, it is not what was decided:
?”.from(p) in the ledger, substituted at the call site, and a function value’s set carried as part of the type of whatever holds it.What is built today falls back to ? in several places:
mut names, push, assignment to a field, with.pub field of a pub type.That fallback is sound: a catch over it needs else (NK1151), so nothing reaches unreachable!. It is still not specific, so it is a temporary safety net and debt, not the design.
To build, in place of the open steps:
? source above with the specific set: D3 for mutation, push, assignment and with; D4 from(p) for parameters and for functions used as values; the set carried on the holding type for fields, pub ones included. Each with a test: a catch without else over that set compiles, and a missing member is refused.from(p) is read back as itself, not as ? with a side map.Handed and FATAL, net::serve).Fixes #620, #605 only lands when no function value produces ?.If a step needs a language decision that ADR-351 does not cover, it is asked here, not settled with ?.
Generated by Claude Code
A function value carries the error set the compiler inferred for it (ADR-351 D1). When a function calls code it was given, the ledger says so with from(p), and the caller replaces p with what it passed (D4, Part III 13.5):
pub fn now(f: fn() throws) throws { f() } // ledger: throws = ["from(f)"]
// caller in another package:
lib::now(fail) catch { match error { Bad::Oops => … } } // exhaustive: from(f) = what `fail` throwsThat case is buildable and was built (branch wip/fnsets-from-p: the ledger writes from(f), the call site substitutes). The owner’s correction (no ? for any function value, D7) also asks to replace the remaining safety nets: a function named as a value, a pub field of a pub type, and mut names / push / field assignment / with. Most of that is D3 (a union over everything that reaches the place) and needs no decision. One case does.
A library keeps code in one call and calls it in another, so the calling function has no parameter that from(p) could name:
pub struct Task { pub run: fn() throws }
var tasks: Vec[Task] = [] // library state
pub fn register(t: Task) { tasks.push(t) } // keeps
pub fn fire() throws { for t in tasks { t.run() } } // calls: from(?)fire’s set is the union of what every caller of register, in every package, hands it (D3). The library cannot know that set when it is built, and the caller of fire cannot know it either. The same happens with a pub fn make() -> Task whose result’s field set has to be published: Part III has no spelling for “the set of field run of the result”.
The owner’s course correction of 2026-10-14 to this issue’s To build step 3 (ledger from(p)). Something concrete needs the answer: a server or registry-style library (net::serve keeps its handler, but calls it through its own parameter, so serve is covered; a user library with register/fire is not). The step can’t finish without an answer, and Fixes #620 waits for it.
from(p) names a parameter or a field path of one. Nothing names a place inside the library’s state or a result.? (the owner confirmed this today).fire’s call through tasks is ? (the 0.0.947 safety net: a pub field of a pub type is stored into by other packages). A catch over fire() needs else (NK1151). Nothing panics at run time, but nothing is proved either.
A. Places in the ledger, resolved by the program package. The library publishes the place by name: register says keeps = ["t → place tasks.run"], and fire says throws = ["from(place tasks.run)"]. The library’s own set for fire stays open. The package that builds main sees every package, unions what each one hands register (D3), and closes the set there, as 7.1’s whole-program inference already does for named functions. Pro: D3 and D7 hold everywhere, with no ?. Con: a new ledger spelling (places, and result.field for make). A library’s catch over fire() inside the library can never be exhaustive, because its set is only known at the program; such a catch needs else, and that else is something the library cannot name, not a ?. Worst case: a refusal in the library, never a wrong value.
B. A type that holds code is generic over its set. Task is Task[E] invisibly; tasks: Vec[Task] in a library has one fixed E per program, inferred at the program, which is A seen through types. Pro: this is D4’s second half taken literally (“the set is part of the value’s type”). Con: the same ledger spelling question, plus generic sets through Vec, maps and globals in the checker. Worst case: as A.
C. Refuse it. A pub function may not call code that another pub function kept, except through from(p). Con: rules out registries, event buses and plugin lists, which every language counts as basic.
A (B is the same rule stated through types; the ledger needs A’s spelling either way). It is 7.1’s whole-program inference extended by one kind of place. The library’s own catch stays open, and that is honest: the library really does not know.
from(place tasks.run), keeps naming the place) and of a result’s field (from(result.run));from(…) member varies with the caller. The plan is to keep the opaque box and lower a call site whose set is closed to a downcast into the caller’s sum.Label set to decision. Built so far for this step: the ledger’s from(p) for parameters, and call-site substitution, on branch wip/fnsets-from-p (df61a87). It is not on develop, because it reads from(p) back as ? plus a side map, which the correction rules out. Step 1’s remaining D3 work (mut, push, assignment, with, named-as-value) does not depend on this question.
Generated by Claude Code
Addendum to the question above: how other languages handle code a library keeps in its own state. These rows are from memory and have not been checked against current manuals.
| Language | register(t) / fire() over a library-held list |
|---|---|
| Rust | static list of Box<dyn Fn() -> Result<(), E>>. Either the library fixes E, or it uses Box<dyn Error>, which is open. A static cannot be generic. |
| Swift (typed throws) | A Registry<E> type can be generic. A global or shared registry needs a fixed E or any Error, which is open. |
| Koka | A mutable reference holding functions has one fixed effect row in its type. Effect polymorphism does not reach into global state. |
| Java, Kotlin, C# | Unchecked: always open. |
| Whole-program compilers (MLton) | They resolve every function value at link time, but for code, not for error types. No language from this list closes an error set there. |
So in every typed language, either the library names the set, or it is open. Option A, where the program package closes the set, would be new. It follows from Part I 7.1 (whole-program inference) and has no precedent elsewhere.
One option is missing above:
D. An explicit set on the stored type (pub run: fn() throws(IoError, Timeout)). ADR-351 §7 left this undecided. The library names what its stored code may throw. register refuses a t whose inferred set is larger, and fire() is exact inside the library and for every caller. No new ledger spelling is needed beyond the type.
throws names no types (ADR-023), and D would be the first place where they are written.Generated by Claude Code
State after 0.0.956 (f81800f), ADR-351 D3:
? sources removed. A let mut name (reassigning it adds the new value’s set), push/insert/extend/append into a name or a field, assignment into a field or an element, and with. Each place now carries the union. Tests in function_value_errors.rs: an exhaustive catch with no else compiles, and a missing member is NK1151.
Still conservative (open, not ?-by-decision). A let mut name of code handed to a mut parameter or to any method may be changed there, so its set stays open.
Fixed on the way:
catch over a closed set of two or more members, through a field or a name of code, did not check that every member had an arm, and lowered the missing ones to unreachable!. This was true on develop before this change, for example with Job { run: both }. It is now NK1151 (check_boxes.nika, a_closed_set_that_misses_a_case).fn() throws had no set. Its handler lowered to a match on the box, which rustc refused. It now takes the place’s set and the box is opened.What remains:
for over a field path (for run in jobs.all) does not take the field’s set yet. It is NK1134 today, and the test a_list_field_carries_what_was_pushed is #[ignore]d.from(p) is not started: a function named as a value whose parameters are code, pub functions, the ledger, call-site substitution, the two-package test and the ADR-288 warning. origin/wip/fnsets-from-p is still the source for the ledger writer, the substitution and the two-package test. Its readback as ? is not to be reused.Handed/FATAL; the net::serve detached path) are not started.pub-field ? safety net is unchanged, kept for the owner’s open question (comment 6175094338).Also seen and not caused by this change: contracts::the_shipped_std_ledger_agrees_with_its_nikaia_sources fails on develop since c01e22c. supervisor::Restart::decide has keeps = ["history"] in the sources but not in std.contracts.
Generated by Claude Code
State after 0.0.963 (0468828), ADR-351 D3/D4. Part of #620; nothing closed.
Built
for over a field path (for run in jobs.all) takes the field’s set. A Vec/map of code in a struct literal or in a field is now a place too: a_field_holds_code and the literal’s code_field used to look only at a bare fn. The test a_list_field_carries_what_was_pushed is no longer ignored.from(p):
throws = ["from(p)"] for a pub function, or one used as a value, that calls code it was given.?, no side map, no throws_from field.from(F::p). A callee’s own from(F::p) is dropped at its callers, because their arguments already reached the place. F publishes it as from(p).from(p) from its arguments (contracts/throws.rs, from_given).check_core_call_from_given). An unsubstituted from(..) is open in a catch (needs else), as ? is.catch over it opens the box by the type each arm names.throws = ["?"] on develop, always. A call by a local name was Opaque, which became ?, and the parameter’s place was never an edge of the graph. Now the call is @name, resolved against the checker’s places, and the parameter call is recorded as one.std.contracts: supervisor::Restart::decide now has keeps = ["history"], so the_shipped_std_ledger_agrees_with_its_nikaia_sources passes again.Tests:
a_caller_replaces_from_with_what_it_passed: an exhaustive catch compiles, and passing worse is refused.the_ledger_says_from_the_parameter: written as from(f) and read back as from(f).function_value_errors_across::the_library_publishes_from_its_parameter: two packages, a path dependency.Open
fn() throws parameter (now(fail)) is lowered in its own channel (Thrown<Bad>), and rustc wants the box there. On develop before this change the same program failed with expected Box<dyn Error>, found Bad. The checker side is right. The two-package run test a_catch_over_a_library_call_takes_what_was_passed is #[ignore]d for it. This blocks D4 at run time and is the next step.from(p) (project.rs newly) is not built.? sources:
g(f), where f is a parameter): code_into finds no stored entry;let mut name of code handed to a mut parameter or a method (step 3, not started);pub-field safety net, kept for the register/fire decision.supervisor, task::scope/spawn and net::serve, and removing Handed/FATAL) are not started.Tested after the final rebase (release):
function_value_errors, contracts, catch_handler, errors_lowering;cargo clippy --all-targets -D warnings;lower-std is a no-op.One rebase earlier the run also covered catch_error_type, specification, self_hosting, sysroot, ledger_spelling, language, function_values, tasks and function_value_errors_across, all green.
Generated by Claude Code
A correction to the question above. Its example keeps code in library state, var tasks: Vec[Task] = []. That cannot be written in Nikaia: var is no keyword (Didn't expect var here), and ADR-281 D32 says “This language has no global mutable data.” There are no trait objects either (Part I: “a trait is not a type: there is no dyn“); traits are bounds, resolved per type. So code that is kept always lives in a value someone holds, reached from a parameter or a result. The “place only the program can close” that option A needed does not exist.
Checked on develop 0.0.964, with a registry written in Nikaia (struct Registry { tasks: Vec[Task] }, register(ref mut self, t), fire(ref self) throws):
catch over r.fire() naming Bad and Worse needed else. That followed Part I 7.1, which disagreed with this issue’s function-value tests; that became #625 and is decided as ADR-357.else, rustc refused the lowering: fire returns Box<dyn Error> and the catch matched the box as if it were the sum. This is filed as #624, and D8’s lowering removes the box.now(fail) (a from(p) callee) lowers to the box and is refused by rustc (the known defect, test ignored).Decision. Recorded as ADR-351 D8, Part I 7.1 and Part III 13.5 (new ledger key code). Version 0.0.966, commit af76c02.
Shared, both ends of a channel, positions sharing makes one allocation) shares it. It is the union of everything put there over the value’s whole life, flow-insensitive.code, in the shape of maps: code = ["self.tasks.run: from(t)", "<result>.run: Bad"]. A path is one field long below the parameter, through list or map elements. A caller adds the set, with from(p) replaced, to the value it holds.from(…) member, take a Rust type parameter for the error, filled with the place’s generated sum. Code is converted where it enters the place, and a catch matches the sum. The box stays only for "?".fn() throws(E) (§7, still not needed);With ADR-357 (#625), a catch over such a call that names every type is complete.
code. Write it for a function that puts code into a place reached from a parameter or its result, read it at callers, and add the set to the caller’s value at that path, with handles of one storage sharing it. Remove the pub-field ? safety net. Tests:
r.fire() with arms Bad and Worse and no else compiles and runs;Registry in a library, register/fire called from the app);Shared registry registered through one handle and fired through another;recv;lib::setup(mut r) adding a task, which then reaches r.fire()’s set.from(p) member becomes generic over the error: fn now<E>(f: &impl Fn() -> Result<(), E>) -> Result<(), E>.Task<E>, Registry<E>.now(fail) runs (un-ignore a_catch_over_a_library_call_takes_what_was_passed), the registry runs, and the lowered Rust has no Box<dyn std::error::Error> in either.? sources. A parameter of code forwarded to another function (g(f)) gives from(f). A let mut name handed to a method is covered by code.supervisor, task::scope/spawn, net::serve), and the runtime (remove Handed and FATAL, the net::serve detached path).The last commit says Fixes #620, #605, #624.
Generated by Claude Code
State after 0.0.971 (37df596). Part of #620; nothing closed.
Built
throws function hands its failure on. Before this, now’s body f() lowered to f().await; with no ?, so the error was dropped silently. This was a lowering defect. The checker now records the call (fact run_code_fails), and the emitter writes the ?.from(p). A catch over now(fail) is told what fail gained since the committed ledger, even though now still says from(f). Test: new_error_reaches_a_catch::a_passed_function_that_gained_an_error_is_named.twice(g) { now(g) }) is the place @twice::g, not ?.
twice publishes ["Bad", "from(g)"], and now publishes ["Bad", "from(f)"].from(G::q) that reaches F through F’s own parameter place is published as F’s from(p).catch over twice(fail) with only a Bad arm compiles and runs. Test: a_parameter_handed_on_chains_from.let mut name handed to a mut parameter of an own function holds what that parameter’s place holds. Test: a_mut_list_handed_to_a_mut_parameter, which now accepts both arms with no else and refuses one arm alone.now(fail). It was replaced by D8, which lowers without a box. The two run tests in function_value_errors_across stay #[ignore]d until D8’s generic lowering lands.Open (new list)
code, and removing the pub-field net.let mut name handed to a method, or to a function in another package, is still ?. Per the new list, ledger code covers it.Tested after the final rebase (release):
lower-std is a no-op, and cargo clippy --all-targets -D warnings passes;function_value_errors, new_error_reaches_a_catch, contracts, sysroot.One rebase earlier the run also covered function_value_errors_across, catch_*, errors, errors_lowering, function_values, language, ledger_spelling, self_hosting, specification and tasks, all green.
Generated by Claude Code