Language: Isolated[T] wrapper for actor message types (Nim-inspired)

[paul-hammant]

Motivation

Aether's actor model already declares message types — LLM.md notes this as the contrast with Erlang's duck-typed mailboxes:

Actor model is Erlang-ish but message types are declared, not duck-typed. receive + send, not ! / mailbox-matching.

Declared types catch shape errors at compile time, but they do not catch shared-aliasing-across-send. Today, nothing in the type system stops a sender from holding a reference to a heap-allocated field of a just-sent message while the receiver mutates it. With ref-counted strings (AetherString*), this is mostly papered over by reference counting; with pointer-bearing struct payloads (file handles, future capability tokens, byte buffers from fs.read_binary), it is a real race.

Nim's Isolated[T] (which is itself a descendant of Pony's reference capabilities) is the cleanest small-surface answer: a wrapper type that asserts at compile time "this value's transitive heap graph has exactly one owner; sending it transfers that ownership; the sender cannot use the value after send." Move-only at the language level. No runtime cost.

Why this fits Aether specifically

• Actor-aligned. Aether is already type-checking messages; Isolated[T] adds an axis (linearity) without adding a new construct.
• Capability-discipline-aligned. A Capability / GrantedFD distinct type wrapped in Isolated[…] is the natural shape for "a capability token that one actor passes to another, exactly once." Matches the design intent of the LD_PRELOAD grant list — capabilities should not be silently shareable.
• Non-GC-friendly. Isolated[T] is not a runtime structure. The whole check is in the type checker / sigmatch. Lowers to plain C with no overhead.
• Composes with the split-accessor / TLS-buffer pattern (LLM.md § "Split-accessor pattern for multi-return"): a *StringSeq that was just built from a TLS drain can be wrapped Isolated[*StringSeq] and sent, with the sender losing its local handle in the same compile-time step.

Sketch — surface

type Msg = struct {
    body: *StringSeq,
    op:   int
}

actor Worker {
    on msg: Isolated[Msg] => {
        // msg.consume() unwraps once; subsequent access is a compile error
        let m = msg.consume()
        ...
    }
}

func send_work(w: actor Worker, body: *StringSeq, op: int) {
    let m = Msg{ body: body, op: op }
    // wrap. After this line, `m` and `body` cannot be referenced by name.
    let iso = isolate(m)
    send(w, iso)
}

Open design questions for docs/isolated.md:

• Is the wrapper a built-in type (Isolated[T] known to the compiler) or a stdlib type with a compiler-recognised pragma?
• How does isolate(...) prove the graph is unaliased? Likely the same dataflow Aether already does for refcount drop-vs-borrow.
• Does receive auto-unwrap (clean) or hand the user the wrapper (explicit)?
• Interaction with *StringSeq's structural sharing — seq_cons-shared tails are not isolated. Probably the answer is "isolation is shallow; deep-share types can't be wrapped" with a clear diagnostic.

What's required

1. docs/isolated.md design doc covering the four questions above.
2. Parser + type checker support for the Isolated[T] shape.
3. Dataflow check at isolate(...) site (no other live refs to the value).
4. consume() lowering (compile error on second consume; no runtime token).
5. tests/regression/actor_isolated_*.ae — pass cases, fail cases, and a "tries to use after send" case that must produce a specific diagnostic.

Why file this now, not later

Aether has at least two downstream-known motivating cases already documented:

• Actor message heap-string ownership (runtime: actor message heap-string ownership protocol (UAF or leak today) #466, closed) — solved by reference counting for strings, but the general pointer-payload problem reopens whenever a non-string heap type lands in a message.
• The capability-grant story (per LLM.md § sandbox) wants single-use, non-shareable tokens; Isolated[Capability] is the type-level expression of that.

Acceptance criteria for this issue

This issue is for agreeing the design, not shipping the feature. Closing it produces:

• docs/isolated.md answering the four open questions.
• A follow-up issue per implementation phase (parser → typer → codegen → tests).

References

• LLM.md § "Actor model is Erlang-ish" — current message-type story
• LLM.md § "Ownership of ptr-typed returns" — the borrowed-vs-ref-counted distinction Isolated[T] extends
• runtime: actor message heap-string ownership protocol (UAF or leak today) #466 (closed) — actor message heap-string ownership, the precursor problem
• Nim lib/std/isolation.nim — reference implementation in a non-GC-by-default language
• Pony reference capabilities — the prior art Nim is descended from