Concurrent

Cooperative async/await concurrency as a single handler, polymorphic in the effects the fibers perform.

fork spawns a fiber and returns a Fiber handle, yield reschedules, await blocks on a fiber’s result, and cancel requests a cooperative cancellation. channel, send, and recv are a buffered FIFO channel for fiber-to-fiber messages. A fiber may perform any effect row e in addition to Async; e is a row-kinded parameter of the reified command type, so one run queue holds every fiber without existential types. Because a fiber’s effects tie to the ambient row at fork, they flow out through run_async: run_async : (() -> a ! {Async(a) | e}) -> a ! {e}, so a fiber that performs E makes the whole run demand a handler for E. Nothing is smuggled past the scheduler.

Prism has no shared mutable cell, so the handler only REIFIES each step as a Cmd, and a pure drive loop threads the run queue, the finished results, the parked awaiters, and the channel buffers. Those parked continuations escape into the scheduler state, so a program using this is whole-program free-monad; it runs in constant native stack under PRISM_TRAMPOLINE.

Cancellation is a cooperative unwind, not a drop. cancel(f) marks f and all its descendants; each is stopped at its next suspension point (yield, await, send, recv), never mid-step, and unwinds through its never finalizers so every resource is released exactly once. Wrap a resource with on_cancel(cleanup, body) to run cleanup on that unwind. A cancelled fiber’s awaiters observe it through try_await (which yields Was_Cancelled rather than hanging); a fiber that fails (an unhandled fail()) cancels its siblings in a scope and re-raises at the scope boundary.

scope is a structured nursery: it forks a list of fibers and joins them all, so no fiber escapes the call, and a failing child fails the whole scope.

A channel carries the shared result type a; fibers in one run share a (use a sum type for mixed messages or results).

Types

Fiber

type Fiber = Fiber(Int)

A handle to a spawned fiber, returned by fork and passed to await/cancel.

Chan

type Chan = Chan(Int)

A handle to a buffered FIFO channel, opened with channel.

Outcome

type Outcome(a) = Completed(a) | Was_Cancelled

The outcome of try_await: a fiber that completed with a value, or one that was cancelled before it could.

Effects

Async

effect Async(a)
  fork(() -> a ! {Async(a) | e}) : Fiber
  poll_yield() : Signal
  poll_await(Fiber) : Wake(a)
  cancel(Fiber) : Unit
  channel() : Chan
  bounded(Int) : Chan
  poll_send(Chan, a) : Signal
  poll_recv(Chan) : Wake(a)
  never kill() : b
  never vanished() : b

The async/await effect. fork spawns a fiber and returns its handle, yield reschedules, await blocks on a fiber’s result, and cancel requests a cooperative cancellation; channel/send/recv are a buffered FIFO channel for fiber-to-fiber messages. Discharge it with run_async.

The public yield/await/send/recv are thin wrappers (below) over the raw poll_* operations, which return a cancellation Signal/Wake the wrapper turns into a cooperative kill. kill and vanished never resume (per-site bottom return b); run_async absorbs the whole effect, so none of the cancel machinery surfaces in a fiber’s row.

Clock

effect Clock
  now() : Int
  sleep(Int) : Unit
  wall_now() : Int
  mono_now() : Int

A logical-time capability: now reads the current tick and sleep advances it. Discharged by run_clock, which threads a pure counter, so time is virtual and deterministic: advance it in a test and behaviour is a function of it, with no real clock and no time primitive. A fiber may perform Clock; since the scheduler does not handle it, it flows out of run_async to an enclosing run_clock like any other capability. now/sleep are the logical scheduler clock (virtual ticks). wall_now and mono_now are the real-time reads (nanoseconds): the system wall clock (Unix epoch, UTC) and a monotonic counter. All four share the one Clock capability; which reading you get is a property of the installed handler, not the call. run_clock serves every op from the virtual counter (deterministic tests); Time.run_clock_real serves wall_now/mono_now from the recorded OS clock.

Functions and Values

yield

yield : forall a. (Unit) -> Unit ! {Concurrent.Async(a)}

Reschedule the current fiber. A cooperative yield point; also a cancellation point (a cancelled fiber unwinds here instead of resuming).

await

await : forall a. (Concurrent.Fiber) -> a ! {Concurrent.Async(a)}

Block until fiber f finishes, returning its result. If f was cancelled, this raises the in-scheduler vanished signal (observe it with try_await); if the waiting fiber is itself cancelled, it unwinds here.

send

send : forall a. (Concurrent.Chan, a) -> Unit ! {Concurrent.Async(a)}

Send v on channel c. On a bounded channel a full buffer parks the sender until a receiver drains it; a cancellation delivered while parked unwinds here.

recv

recv : forall a. (Concurrent.Chan) -> a ! {Concurrent.Async(a)}

Receive a value from channel c, parking until one is available. A cancellation delivered while parked unwinds here.

on_cancel

on_cancel : forall e0 a b. (() -> Unit ! {Concurrent.Async(a), e0}, () -> b ! {Concurrent.Async(a), Concurrent.Async(a), e0}) -> b ! {Concurrent.Async(a), e0}

Run body, and if it is cancelled (unwinds through kill), run cleanup once before the cancellation propagates outward. This is a forwarding handler: every Async operation body performs is relayed unchanged to the enclosing run_async, so the finalizer is transparent except on the cancel path. Nest these for stacked resources; each cleanup runs exactly once, innermost first.

try_await

try_await : forall a. (Concurrent.Fiber) -> Concurrent.Outcome(a) ! {Concurrent.Async(a)}

Await fiber f, observing cancellation as a value instead of a signal: Completed(v) if f finished, Was_Cancelled if it was cancelled. Never hangs on a cancelled fiber. A forwarding handler that catches only the vanished signal await raises for a cancelled target.

run_async

run_async : forall e0 a. (() -> a ! {Concurrent.Async(a), Fail, e0}) -> a ! {Fail, e0}

Run main and its fibers cooperatively under the FIFO (round-robin) policy, returning main‘s result. The fibers’ effects e flow out unchanged, so the caller still handles them.

run_cooperative

run_cooperative : forall e0 a. (() -> a ! {Concurrent.Async(a), Fail, e0}) -> a ! {Fail, e0}

The policy-neutral entry point: run main under the deployment’s default cooperative scheduler. It is run_async (FIFO) by default, and the --scheduler flag (or PRISM_SCHEDULER) retargets it to another shipped policy such as run_lifo with no source change, because the scheduler is only a handler for Async and swapping it never touches the fibers. Call this when you want the configured default; call run_async or run_lifo directly to pin a policy.

run_lifo

run_lifo : forall e0 a. (() -> a ! {Concurrent.Async(a), Fail, e0}) -> a ! {Fail, e0}

A second scheduling policy over the same Async effect: LIFO (depth-first), which runs the most-recently-forked or most-recently-woken fiber next by pushing it to the front of the run queue. It discharges fork/yield/await/channels exactly as run_async does and returns the same result for a determinate computation; only the interleaving (and so the order of observable effects like prints) differs. This is the concrete proof that policy is a handler: the fibers are unchanged, only the run function is swapped.

scope

scope : forall e0 a. (List(() -> a ! {Concurrent.Async(a), e0})) -> List(a) ! {Concurrent.Async(a), e0}

Structured nursery: run tasks concurrently and join them all, returning the results in order. Every task completes before scope returns, so no fiber escapes the call. The nursery is fail-fast: if one task fails (an unhandled fail()), its siblings are cancelled (their on_cancel finalizers run) and the failure is re-raised at the scope boundary.

run_clock

run_clock : forall e0 a. (() -> a ! {Concurrent.Clock, e0}) -> a ! {e0}

Run action against a logical clock starting at 0, returning its result. now() reads the current time; sleep(d) advances it by d. Time is a pure threaded counter (the parameter-passing answer Int -> a), so the run is deterministic and reproducible under Replay.