Async Verbs¶

Prove provides structured concurrency via cooperative coroutines. Async verbs form a third family alongside pure and IO verbs.

Key rules: - listens/renders bodies must not call blocking inputs/outputs functions directly — they run cooperatively and blocking would stall the yield cycle - listens/renders arms can call attached functions via & to perform IO safely in a child coroutine - detached and attached may call blocking IO freely since they have their own coroutine stacks - Concurrency is cooperative — no threads, no data races - Runtime backed by prove_coro stackful coroutines (ucontext_t on POSIX, sequential fallback on Windows)

The & Marker¶

& marks an async call at the call site. It mirrors ! for failable calls:

The verb (detached, attached, listens) declares intent at the function level. & only appears at call sites inside async bodies where work is dispatched to another async function.

detached — Fire and Forget¶

Spawns a coroutine and returns immediately. The caller does not wait for completion. Cannot declare a return type (E374). May call blocking IO freely since it runs independently.

/// Log an event — fire and forget, caller moves on immediately.
detached log(message String)
from
    console(message)

attached — Spawn and Await¶

Spawns a coroutine and blocks the caller until the result is ready. Must declare a return type (E370). May call blocking IO (inputs/outputs) since it runs in its own coroutine stack. When an IO-bearing attached function is called via &, it must be from a listens or another attached body (E398).

/// Read a file — attached does the IO in its own coroutine.
attached load(path String) String
from
    file(path)!

/// Fetch and parse data — caller waits for the result.
attached fetch(url String) String
from
    load(url)&

listens — Event Dispatcher¶

The listens verb declares an event dispatcher that receives typed events from registered attached worker coroutines and dispatches them to match arms.

Signature pattern:

listens name(workers List<Attached>)
    event_type AlgebraicType
from
    VariantA        => ...
    VariantB(data)  => ...
    Exit            => Unit

Key rules:

• First parameter, if present, must be List<Attached> — the registered worker functions
• event_type annotation declares the algebraic type for dispatch (required)
• Each registered attached function's return type must be a variant of the event_type
• Match arms exhaust the event_type variants
• One arm must match Exit (terminates the dispatcher)
• Cannot call blocking IO directly (E371) — use & in match arms
• Attached functions in the worker list can have arguments: [worker(arg)]

The from block uses implicit match — bare arms dispatch on events received from the internal event queue. Workers are spawned as coroutines and send events back to the dispatcher. When the Exit variant is matched, the loop terminates.

Full Example — Event Processor¶

module EventProcessor
  narrative: """Process events using all three async verbs."""
  System outputs console
  Log detached debug

  type Event is Data(payload Integer)
    | Exit

/// Fire and forget — log without blocking.
detached fire(msg String)
from
    console(msg)

/// Produce data events for the dispatcher.
attached double(x Integer) Data<Integer>
from
    Data(x * 2)

/// Event dispatcher — receives events from workers.
listens handler(workers List<Attached>)
    event_type Event
from
    Data(payload) =>
        debug(f"got: {string(payload)}")&
        Exit()
    Exit => Unit

main()
from
    fire("hello from detached")&
    handler([double(2)])&

renders — Event-Driven UI Loop¶

The renders verb declares an event-driven UI loop with mutable state. It follows the same pattern as listens but adds a state singleton that persists across frames.

Signature pattern:

renders name(listeners List<Listens>)
    event_type MyAppEvent
    state_init MyState(initial_value)
from
    Draw(state)  => ...    // render the frame
    Tick(state)  => Draw(state)
    Exit(state)  => Unit   // terminate

Annotations:

• event_type — the algebraic event type (must extend TerminalAppEvent or GraphicAppEvent, not bare AppEvent)
• state_init — initial state value (required — E408); type is inferred (e.g. state_init MyState(0) → state type is MyState)

Annotations on attached callbacks:

• event_type — which event this callback handles (e.g. KeyDown)
• state_type — the state type to access (must match the parent renders state)

Implicit bindings:

• state — mutable application state singleton, available in renders and attached bodies where state_init/state_type is declared
• event — the received event, available in attached bodies

Key rules:

• First parameter must be List<Listens>
• from block must be a single implicit match with an Exit arm
• No return type — renders always returns Unit
• Backend resolved from event_type type chain (TerminalAppEvent → TUI, GraphicAppEvent → GUI)
• state is a singleton created once by state_init — mutable, fields updated in place (exclusive to renders state)
• Draw(state) is the render event — user code describes the frame here
• Tick(state) is the runtime heartbeat — default handler triggers Draw(state)
• Exit terminates the loop

See UI & Terminal for the full type reference and example.

Streams — Blocking IO Loop¶

The streams verb declares a blocking loop over an IO context. It runs until an Exit arm is matched, an error propagates via !, or the IO source is exhausted (e.g. stdin EOF). It is the synchronous counterpart to listens in the async family.

How it works:

The parameter carries the loop context — a value that holds whatever the loop needs each iteration (a file handle, a socket, a prompt string). The match arms execute IO using the context on every iteration. The Exit arm terminates the loop; all other arms loop back.

streams read_and_write(ctx Context)
from
    Exit     => ctx                   // terminates loop
    Active(…) =>                      // IO arm — runs each iteration
        data = read_from(ctx.source)  // blocking read using context
        write_to(ctx.dest, data)      // blocking write

Key rules:

• The from block must be a single implicit match with an Exit arm
• The match subject is the first parameter type
• streams is a blocking IO verb — it cannot be called from listens bodies
• streams bodies may use & to fire-and-forget detached calls (e.g. logging)
• On EOF from an inputs read, the loop exits automatically

REPL Example — Read stdin line by line¶

System outputs console inputs console

type Session is Active(prompt String)
  | Exit

/// Echo stdin lines with a prompt. Exits on EOF.
streams repl(session Session)
from
    Exit           => session
    Active(prompt) =>
        console(prompt)               // write: print prompt
        line as String = console()    // read: next stdin chunk
        console(f"< {line}")          // write: echo it

main()
from
    repl(Active("> "))

Each iteration the Active(prompt) arm performs a blocking console() read. When stdin is exhausted the loop exits cleanly.

Network Server Example — Accept connections in a loop¶

// conn is the loop context; Accept(listener) arm calls accept() each iteration
streams serve(conn Connection)!
from
    Exit              => conn
    Accept(listener)  =>
        client as Socket = accept(listener)!
        data as ByteArray = message(client, 1024)!
        message(client, data)!
        socket(client)

Safety Rules¶