Scala 3 Capture Checking

§1 Provenance

• Lead: Martin Odersky and the EPFL LAMP group. Capture-checking research and Capybara extension led by Oliver Bračevac.
• Reference docs (experimental): https://docs.scala-lang.org/scala3/reference/experimental/cc.html . Advanced: https://docs.scala-lang.org/scala3/reference/experimental/cc-advanced.html . Nightly basics: https://nightly.scala-lang.org/docs/reference/experimental/capture-checking/basics.html .
• Scala Days 2025 talk: Oliver Bračevac (EPFL/LAMP), https://bracevac.org/assets/pdf/scaladays2025_annot.pdf and https://scaladays.org/editions/2025/talks/capture-checking-a-new-approach .
• Conference papers:
  • “What’s in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures”, OOPSLA 2025 (System Capless). https://2025.splashcon.org/details/OOPSLA/133/…
  • “System Capybara: Capture Tracking for Ownership and Borrowing”, Scala Workshop 2025. https://2025.workshop.scala-lang.org/details/scala-2025/6/…
• Practitioner write-ups: SoftwareMill, https://softwaremill.com/understanding-capture-checking-in-scala/ ; Tanishiking blog, https://tanishiking.github.io/posts/introduction-to-scala-3s-capture-checking-and-separation-checking/ .
• Status flag: import scala.language.experimental.captureChecking or -Ycc. Still highly experimental as of May 2026.

§2 Core type discipline

A capability is a syntactic role: a method parameter, a class parameter, a local variable, or this. Every capability has a type with a non-empty capture set.

Types take the form T^{c1, ..., cn} where {c1, …, cn} is the capture set — a set of references to capabilities that the value of type T may capture. A universal capability cap (or any in some docs) sits at the top of the lattice; every capability is derived from cap.

Function arrows split:

• A -> B — pure function arrow, captures nothing.
• A => B — impure (legacy), captures arbitrary capabilities.
• A ->{c,d} B — captures exactly c and d. Shorthand for (A -> B)^{c,d}.

Annotation surface: capture sets in postfix ^{ … } notation on any type. Functions, classes, methods, type aliases. Empty capture set means “pure”; absence means “any”.

Judgement form: a constraint-based propagation. Constraint variables stand for unknown capture sets; constraint flow follows variable bindings; explicit annotations become constants. The check runs as a separate compiler phase after typing.

Classifiers (2025 addition) organise capabilities into a hierarchy with two roots: SharedCapability (the standard capture-checking root) and ExclusiveCapability (Capybara/separation-checking root, capabilities that must be unaliased). The .only[C] operator filters capture sets to keep just the capabilities of a chosen class.

Principal example — a logger capability that should not escape its scope:

def withLog[T](body: Log^ => T): T = ...
val r = withLog { log =>
  () => log.info("hi")              // function captures log
}
// r : (() -> Unit)^{log}            // capture set leaks log
// but log has gone out of scope; this is rejected

The capture-checker rejects the leak because log is not in scope at the call site of r.

§3 Memory-safety invariant

• Capability isolation: a capability cannot escape its lexical scope.
• Effect safety: if a capability represents “I can do IO”, capture tracking ensures that the IO authority does not leak.
• (With separation checking, System Capybara): aliasing-XOR-mutation on ExclusiveCapability-typed values. Same property as Rust’s &mut, surfaced through capabilities.

What it does not preserve (without Capybara): aliasing constraints on ordinary data. Standard capture checking is about what references are visible, not who can write.

§4 Compiler implementation cost

• A separate compiler phase after typing. Implemented as a constraint solver over capture-set variables; the constraint graph is small in practice (one variable per binding).
• Diagnostics: scoped-to-capability messages (“function value captures log which is out of scope”). Better than Rust’s lifetime errors because the capability name is local and meaningful.
• Migration cost has been the wall: the Scala 3.8 milestone required capture-checking the entire collections library. The OOPSLA'25 System Capless paper covers exactly this migration effort and the reach capabilities mechanism that made it ergonomic.
• The full Capybara extension (separation checking) adds further per-capability flow analysis; cost is modest because the underlying machinery already exists.

§5 Production / language adoption status (May 2026)

• Capture checking remains experimental (opt-in import / -Ycc).
• Scala 3.8 (2025) ships:
  • Capture-checked standard library.
  • Classifier hierarchy.
  • Reach capabilities (System Capless).
• Capybara (separation checking) is research-stage, with a working prototype.
• No major Scala framework requires capture checking yet; experimental adopters include Gears (async library), parts of the Scala compiler itself.

§6 Mochi adaptation note

Capture checking and Mochi’s MEP-15 effect system are conceptually the same machinery seen from different angles. MEP-15 attaches {io, fs, net, time, meta} to each function; capture checking attaches {c1, c2, …} (per-capability references) to each function. Both are propagated bottom-up through the call graph; both are checked against declared upper bounds at signature points.

The mapping is:

Pieces that map cleanly:

• Capabilities as values, not as labels. MEP-41 promotes MEP-15’s labels to first-class values: io: IoCap, fs: FsCap, etc. Functions take capability parameters; effect inference is then “does the body refer to a capability the signature did not list?”.
• Separation checking (Capybara) for handle-mutable types. An ExclusiveCapability-equivalent on a Mochi linear handle gives aliasing-XOR-mutation.
• .only[C] filtering. Useful for restricting effect surfaces in MEP-15 (e.g. “this function may touch the FS but not the network”).

Incompatible:

• The full capture-set syntax ^{c, d} everywhere. Verbose; better suited to Scala’s denser type surface. Mochi should keep the post-fix ! from MEP-15 and grow it with capability references rather than label strings.
• Reach capabilities (System Capless). They solve a problem about generic data structures that Mochi does not yet have.

Surface-syntax change for MEP-41: extend MEP-15’s ! clause to accept capability values as well as labels. E.g. fun open(p: Path, fs: FsCap): File ! fs. The fs after ! names the capability that authorises the effect.

vm3 tie-in: capability values are normal handle Cells (probably in ArenaStruct or a new ArenaCap slab). The runtime cost is minimal; the static check does the work.

MEP-16 tie-in: Option<FsCap> lets a function gracefully degrade if the capability is absent.

§7 Open questions for MEP-41

1. Should MEP-41 promote MEP-15’s labels to capability values, or leave them as labels and add capabilities separately?
2. How does the Capybara separation-checking extension interact with Mochi’s GC? (Likely: not at all; the static check is independent of the runtime.)
3. Is reach-capability machinery worth the complexity for Mochi’s current generic surface?
4. Can vm3 share representation between capability values and ordinary structs, or do we need a dedicated ArenaCap?

Sources: https://docs.scala-lang.org/scala3/reference/experimental/cc.html ; https://bracevac.org/assets/pdf/scaladays2025_annot.pdf ; OOPSLA 2025 System Capless paper ; Scala Workshop 2025 System Capybara paper ; https://softwaremill.com/understanding-capture-checking-in-scala/ .