Async Verbs¶

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

Key rules: - listens bodies must not call blocking inputs/outputs functions directly — they run cooperatively and blocking would stall the yield cycle - listens 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(event.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 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 declare a return type (E374)
• 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)])&

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¶