region.ktr

// The `prelude.region` sub-module: structured concurrency as ordinary agent values — a nursery.
// `provide` opens a scope, `fork` spawns a detached fiber into it, `cancel_by_id` tears one down, and
// `watch` re-emits the fibers' escalations as effects the enclosing program handles. There is
// no `join`: a fiber is a detached worker rather than a future. `parallel` waits, a region
// listens. Every operation routes to the runtime's `region` reactor, so each performs `io`.
//
// The scope: `provide` mints a caller-chosen `Scope` marker for its continuation's row and discharges
// it from its own, and every operation is gated `with Scope`, so no fiber or handle outlives the
// `provide` that opened it. The marker gates the operations, not the ids they carry — a fiber id is
// plain data, so a cancel aimed at another nursery's fiber answers `unknown_fiber` at runtime. Two
// nurseries under one marker share a scope; a distinct marker per nursery keeps them apart.
//
// A fiber runs under the region's `watch`: its escalations surface there and nowhere else. `provide`'s
// second type argument `E` bounds every fiber's effect and is carried invariantly by the handle, and
// `watch` re-emits the full `E` plus the runtime's two ending events, so a row covering
// `E | crashed | failed` around the watch covers everything any fiber can surface.

@"The built-in nursery scope: a nullary phantom marker, carried in a fiber's effect row and every operation's row, never performable, never handleable. `provide` mints it for its continuation and discharges it from its own row, so a fiber cannot outlive its nursery. Declare your own marker per nursery when nesting, so two regions' scopes never merge."
effect scope

// A running child of a nursery, as an opaque handle. `Scope` rides its effect row rather than a `data`
// phantom (which would compare bivariantly and silently let a handle cross regions), so the comparison
// routes through effect-row subtyping. A fiber carries no result type — its outputs ride its
// escalations — so the handle is identity only. (Type synonyms take no docs.)
type fiber[effect Scope] = agent never -> null with Scope

// The nursery handle `provide` hands its continuation. `Scope` and `E` each appear once
// contravariantly and once covariantly, so unifying a handle pins both to exactly what `provide`
// fixed: an operation finds `Scope` still in the caller's row (an upper and lower bound), and `E` is
// neither widened by `fork` nor narrowed by `watch`. The inner agents are never called; each exists
// only to carry a marker at one polarity.
type nursery[effect Scope, effect E] = agent (gate: agent never -> unknown with Scope, bound: agent never -> unknown with E) -> {gate: agent never -> unknown with Scope, bound: agent never -> unknown with E}

@"Open a nursery for the extent of @continuation@, as a scoped provider — the `use region.provide[region.scope, E](...)` form. It hands @continuation@ a `nursery[Scope, E]` handle whose fibers may raise at most the effects `E`, and settles with the continuation's result. `Scope` rides the continuation's row and is discharged from `provide`'s own, so no fiber outlives the block: the nursery closes when @continuation@ returns, cancelling its still-running fibers. Pin `Scope` and the ceiling `E` as the first two type arguments; `R` and the residual outer row are inferred. Two nurseries sharing one marker share a scope, so their fibers become mutually cancellable; a distinct marker per nursery keeps them apart."
external agent provide[effect Scope, effect E, R, effect Eouter](
  @"The nursery body (bound by `use`): receives the handle, and its fibers run exactly while it does." continuation: agent (value: nursery[Scope, E]) -> R with Eouter | Scope,
) -> R with Eouter | io from "region"

@"Spawn @task@ as a fiber in @nursery@, applied to @argument@ — the whole argument record of the call the fiber will make — and return immediately with a `fiber[Scope]` handle (identity only; `fiber_id` reads the id `cancel_by_id` addresses). A fork is a deferred call, so `region.fork(nursery = box, task = deliver, argument = { source = \"mail:core\", hop = 1 })` runs `deliver(source = \"mail:core\", hop = 1)`; @task@ keeps its own parameter names, a nullary task is forked with `argument = {}`, and a wider record fits (parameter records are contravariant). @name@ is an optional opaque tag the runtime echoes back in `roster`, `crashed` and `failed`.

@task@ is `-> null`: a fiber carries no result, and everything it produces leaves through its escalations, which surface at `watch`. A `-> never` body — a watcher that runs until cancelled — fits by subtyping. Its effect fits under the ceiling `E`, except its throws: the task parameter's row is `E | prelude.throw[unknown]`, because an uncaught throw is trapped at `watch` and delivered as the typed `failed` event rather than crossing the region as a throw, so a throwing task forks under a throw-free ceiling.

A fork routes by the handle alone, so forking into another nursery's handle is cross-nursery mail. The forked closure's captured environment travels with it into an instance the sender does not own, so such a fork sends a named agent applied to plain data, which captures nothing; inline closures belong to forks into a nursery the caller owns. Forking into a settled nursery panics — delivery is at-most-once; fold the fork with `supervise.once` + `supervise.signal_panics` where a lost message must be noticed.

Scope-gated (`with Scope`): callable only inside the `provide` that opened this nursery."
external agent fork[effect Scope, effect E, A](
  @"The nursery handle from the enclosing `provide`." nursery: nursery[Scope, E],
  @"The child agent to run; `-> null` (results ride escalations), effect under the ceiling `E` — plus any `prelude.throw`, which never crosses the region as a throw (the boundary traps it and delivers `failed`)." task: agent A -> null with E | prelude.throw[unknown],
  @"The arguments @task@ is applied to, as its whole parameter record — `{}` for a nullary task." argument: A,
  @"An opaque name tag, echoed by `roster`, `crashed` and `failed`; empty means unnamed." name: string ?= "",
) -> fiber[Scope] with Scope | io from "region"

@"Re-emit the nursery's fibers' escalations into the enclosing program as the ceiling effect `E`, plus the runtime's own `crashed` and `failed` events. It returns `never` — it only ever raises — so a handler (or any row covering `E | crashed | failed`) wraps it, and that covers everything any fiber can surface. This is the one channel out of a fiber: a normal completion and a cancellation are silent, and the two endings a task cannot report itself arrive as typed events — a panic as `crashed`, an uncaught `prelude.throw` as `failed`.

An escalation raised before any `watch` is installed is held durably and re-emitted in arrival order the moment one registers, so a watch installed later receives every earlier escalation. `watch` re-emits every escalation concurrently and adds no serialization of its own; the serialization point is the receiving handler, so two escalations to different handlers run concurrently, two to the same stateful (`var`) handler run one at a time in arrival order, and two to the same `parallel handler` run concurrently. One watch interleaves every fiber's stream, so a second adds no concurrency.

Scope-gated (`with Scope`): callable only inside the opening `provide`."
external agent watch[effect Scope, effect E](
  @"The nursery handle from the enclosing `provide`." nursery: nursery[Scope, E],
) -> never with E | crashed | failed | Scope | io from "region"

// The nursery is the registry: the runtime mints the fiber ids, tracks liveness and sees every ending,
// so there is no Katari-side mirror to keep in sync. It does not own the interpretation — both ending
// events are data, and what a death means is a handler's decision. The two events stay two because
// their payloads differ: `failed` carries a typed domain value, `crashed` carries a defect's message.

@"One running fiber, as `roster` reports it: the runtime-minted @id@ (the same id `cancel_by_id`
addresses and `crashed` names) and the @name@ tag its `fork` carried (empty when the fork gave
none)."
data fiber_info(id: string, name: string)

@"A `cancel_by_id` outcome: the fiber was live and has been torn down."
data cancelled(@"The id of the fiber that was cancelled." id: string)

@"A `cancel_by_id` outcome: no running fiber of this nursery has this id — it already settled, was
already cancelled, or the id never existed. Not an error: ids are data (often model-supplied), so a
stale one is an anticipated miss the caller renders."
data unknown_fiber(@"The id that matched nothing." id: string)

// What a cancel-by-id found. (Type synonyms take no docs.)
type cancel_outcome = cancelled | unknown_fiber

@"A fiber crashed — re-emitted at `watch` in place of the fiber's unhandled panic. The fiber is dead at
that instant (a panic never resumes), so the runtime tears it down and reports the ending as data
rather than letting the panic unwind the watch context. Fire-and-forget (`-> null`): a handler above
the `watch` decides what a crash means — report it, fork a replacement, or re-raise to bring the region
down. The runtime is its one author."
request crashed(
  @"The runtime-minted id of the fiber that crashed." id: string,
  @"The name tag its fork carried (empty when the fork gave none)." name: string,
  @"The panic message the fiber died with." message: string,
) -> null

@"A fiber failed — re-emitted at `watch` in place of the fiber's uncaught `prelude.throw`, which had
nothing left inside the task to catch it. @error@ is the thrown value itself, untouched, so a handler
`match`es it exactly as a `prelude.throw` handler would. Fire-and-forget (`-> null`): a handler above
the `watch` decides what the failure means. The throw is trapped here rather than riding the ceiling
out of the region, which is why a `fork` carries no throw guard. Distinct from `crashed`: a throw's
payload is typed domain data, while a panic carries only a message. The runtime is its one author."
request failed(
  @"The runtime-minted id of the fiber that failed." id: string,
  @"The name tag its fork carried (empty when the fork gave none)." name: string,
  @"The value the fiber threw, exactly as it was thrown." error: unknown,
) -> null

@"The runtime-minted id of a fiber handle — the same id `roster` lists, `cancel_by_id` addresses and
`crashed` names, read straight off the handle (a pure read, no runtime round-trip)."
primitive agent fiber_id(@"The fiber handle `fork` returned." handle: agent never -> null with all) -> string

@"The running fibers of @nursery@, straight from the runtime's own liveness — one `fiber_info` per live
fiber, in fork order. There is no Katari-side copy, so a settled or cancelled fiber is simply absent.
Scope-gated (`with Scope`): callable only inside the opening `provide`."
external agent roster[effect Scope, effect E](
  @"The nursery handle from the enclosing `provide`." nursery: nursery[Scope, E],
) -> array[fiber_info] with Scope | io from "region"

@"Tear down the fiber the runtime knows by @id@ — the one way to stop a fiber. An id rather than a
handle because an id is data: it survives a store round-trip and rides into a model-facing stop tool. A
live fiber answers `cancelled`; an id matching no running fiber of this nursery — settled, already
cancelled, never real, or minted by another nursery — answers `unknown_fiber`, a value to render.
Scope-gated (`with Scope`): callable only inside the opening `provide`."
external agent cancel_by_id[effect Scope, effect E](
  @"The nursery handle from the enclosing `provide`." nursery: nursery[Scope, E],
  @"The runtime-minted fiber id to tear down." id: string,
) -> cancel_outcome with Scope | io from "region"