A Friendly Tour of Substructural, Uniqueness, Ownership, and Capabilities Types — and more!

This post is part of The Eter programming Language series.

Edit: Take a look at the discussion in the Programming Languages subreddit.

This is the third post in the series dedicated to the Eter programming language, a side project that allows me to take my mind off the research I have to conduct. The previous posts are Mutable Value Semantics (MVS) or Ownership & Borrowing: A Trade-off Analysis and The Mutable Value Semantics (MVS): A Non-superficial Study. If you are interested in the project, you can find more information in the Eter compiler monorepo. The Eter language reference and the Eter Doxygen documentation, although not yet complete, are also good starting points.

The first post, in its prelude, introduces what we are currently researching for the Eter language. Then, it discusses the mutable value semantics (MVS) and how the popular programming languages (e.g., Swift , Hylo ) implement it. The second post covers the trade-offs between MVS and ownership & borrowing, examining friction points in Rust, Hylo, and Swift while searching for common ground between the two memory models.

Contrary to what I mentioned in the previous two posts, this post is once again not part of the Eter language itself. I needed to provide this post to clarify some concepts I consider fundamental to the language's design, semantics, and type system.

What follows is meant to be a friendly tour. We start from the logical roots of why ordinary type systems fall short, walk through linear, affine, and uniqueness types, and then visit the broader family—regions, effects, capabilities, typestate, and the very recent work on reachability and separation. I keep the theory light on purpose; the goal is intuition and a map of the landscape, with pointers to the literature for the details.

Resources are not Truths

Classical logic treats propositions as eternal truths. If you know that \(A\) holds, you may use that fact as many times as you like, pass it around freely, and ignore it when you don't need it. This is exactly the behavior we want from mathematical knowledge—and exactly the behavior we get from values in a conventional type system.

Programs, however, spend much of their time juggling resources: file handles, memory, locks, network connections. Resources do not behave like truths. A file handle used twice may corrupt state; a lock acquired but never released deadlocks; memory freed and then read invites undefined behavior. The type systems we inherit from the simply-typed \(\lambda\)-calculus have no vocabulary for "this value must be used exactly once" or "there must never be two copies of this reference".

This is the gap that an entire family of type systems sets out to close. Their common ancestor is a branch of logic—substructural logic—and their descendants include Rust's ownership system, Haskell's linear types, Scala's capabilities, and the object-capability security model. The rest of this post is a tour of that family.

Restricting Use: Substructural Types

The first family asks a deceptively simple question: how many times may a variable be used? By giving up some of the structural rules we are about to meet, these systems turn ordinary hypotheses into resources that have to be spent carefully—and that is already enough to make memory, file handles, and locks safe.

Substructural Type Systems

Let me give an informal introduction to substructural type systems, uniqueness types, and fractional uniqueness, for those who are not familiar with them. Substructural type systems resemble the idea of substructural logic. They are based on the following structural rules (where \(\Gamma\) is the context of assumptions):

• Exchange, the order of assumptions in \(\Gamma\) does not matter. That is, the order of variable declarations does not influence the semantics of the program. \[ \frac{\Gamma_1, x : A, y : B, \Gamma_2 \vdash t : C} {\Gamma_1, y : B, x : A, \Gamma_2 \vdash t : C} \]
• Weakening, assumptions can be discarded (ignored). That is, variables can be declared but not used in the program. \[ \frac{\Gamma \vdash t : A} {\Gamma, x : B \vdash t : A} \quad x \notin FV(t) \]
• Contraction, assumptions can be duplicated. That is, two "copies" of the same variable are equivalent. \[ \frac{\Gamma, x : A, x : A \vdash t : B} {\Gamma, x : A \vdash t : B} \]

Substructural type systems arise by selectively restricting these rules. Removing different rules yields different disciplines for how often a variable may appear:

To cite a few, linear type systems (resembling linear logic ) disallow both weakening and contraction, while affine systems disallow contraction but permit weakening. Intuitively, these combinations tell us how many times a variable can be used in the program: exactly once for linear types , at most once for affine types, and so on.

Linear Types

Linear types are the computational reading of linear logic, introduced by Girard . Girard's insight was that the structural rules weakening and contraction are precisely what give classical logic its "idealist" character—propositions you can freely copy and discard. Drop them, and you obtain a logic of resources, where every hypothesis must be used exactly once. The familiar conjunction even splits in two: a multiplicative \(A \otimes B\) ("both, separately") and an additive \(A \mathbin{\&} B\) ("your choice"), while linear implication \(A \multimap B\) consumes one \(A\) to produce one \(B\).

Operationally, the "exactly once" discipline shows up in how the typing context is handled. An ordinary type system copies the context freely into every subterm; a linear one splits it, so each assumption flows to exactly one place. Function application is the rule to watch: \[ \frac{\Gamma_1 \vdash e_1 : A \multimap B \qquad \Gamma_2 \vdash e_2 : A} {\Gamma_1, \Gamma_2 \vdash e_1\,e_2 : B} \] The context \(\Gamma_1, \Gamma_2\) is a disjoint split: a variable given to \(e_1\) is no longer available to \(e_2\), and with no contraction rule to copy it back, that is exactly what stops a resource from being used twice.

Wadler's "Linear types can change the world!" showed how to turn this into a type system for functional languages. The headline application: linear types make in-place mutation safe. If the type system guarantees you hold the only reference to an array, you may update it destructively without breaking referential transparency—nobody else can observe the change.

The price is bureaucracy. Because a linear value is consumed by use, it has to be threaded explicitly through the program—each operation hands you back a fresh handle:

read2 :: MArray a ⊸ (Ur a, Ur a)
read2 arr0 =
  let (arr1, x) = read arr0 0
      (arr2, y) = read arr1 1
      ()        = free arr2
  in (x, y)

Modern incarnations include Linear Haskell (GHC 9.0+) and Idris 2's quantitative type theory. Reducing this threading overhead is one of the motivations for the linear constraints we meet further down.

Affine Types

Affine types relax linearity by allowing weakening but not contraction: a variable may be used at most once, and may also be discarded without being used. Rust's ownership system is the most prominent affine type system in practice. A value can be moved (consumed once) or dropped (discarded); what is forbidden is duplicating it without an explicit clone. The Copy trait marks the types that are allowed to be implicitly duplicated—i.e., it reintroduces contraction for specific types.

The difference between linear and affine is simply whether discarding is allowed. Linear: you must use the resource—useful for protocols that demand explicit termination (e.g., sending a final message before closing a connection). Affine: you may drop it—Rust leans on this because the destructor (drop) runs automatically at scope exit, so the resource is cleaned up rather than truly lost. These affine guarantees are what give Rust no use-after-free, no double-free, and no data races, all at compile time with zero runtime overhead.

The discipline is easiest to see by tripping over it. Assigning a non-Copy value moves it—the source binding is consumed, and the compiler statically rejects any later use:

let s1 = String::from("hi");
let s2 = s1;            // String is affine: the value MOVES out of s1
// println!("{s1}");    // ✗ error: borrow of moved value: `s1`

let n1: i32 = 7;        // i32 is Copy
let n2 = n1;            // copied, not moved
println!("{n1} {n2}");  // ✓ n1 is still usable

The move is the missing contraction rule made concrete; the Copy trait is the controlled exception that hands it back for small, cheaply-duplicated types.

Restricting Aliasing: Uniqueness and Ownership

Counting uses controls how often a value is consumed, but it says nothing about how many references point at it. The next family shifts the question from use to aliasing: how many views of a value may coexist, and which of them is allowed to mutate it.

Uniqueness Types

The key issue here is that linearity, even when combined with affine weakening, remains fundamentally a usage discipline. It controls how values are consumed in a derivation, but it does not prevent the possibility that a value has been duplicated before it enters the linear fragment of the type system (cf. the Clean language). In systems that include unrestricted values,¹ linearity alone cannot reconstruct global aliasing information: a linear assumption may still correspond to a value that has been shared elsewhere in the program.

This limitation becomes particularly evident when reasoning about mutation. If multiple references to the same underlying structure exist outside the linear scope, then allowing in-place updates becomes unsafe, even if the linear fragment itself enforces single-use discipline. In other words, linearity guarantees local resource consumption, but not global uniqueness of access.

Uniqueness types address precisely this gap. Instead of constraining how a value is used within a derivation, they constrain whether a value can be observably shared at all. A unique value is not merely one that is used exactly once, but one for which the type system guarantees the absence of aliasing in the entire program context.

This distinction explains why uniqueness behaves asymmetrically with respect to unrestricted values. While it is not possible to derive uniqueness from an unrestricted value—since duplication may already have occurred—it is always safe to forget uniqueness information once it has been established. In this sense, uniqueness types can be seen as a strengthening of ownership information, rather than a restriction on usage. This makes uniqueness particularly well-suited for modeling destructive updates in functional languages, where referential transparency must be preserved despite the presence of in-place mutation. Please refer to Linearity and Uniqueness: An Entente Cordiale for a more in-depth discussion on the topic, as well as how the uniqueness is enforced.

Granule turns this into surface syntax. A value of type *a is uniquely owned—the type system guarantees no other reference exists, which is exactly what licenses updating it in place—and the asymmetry above appears as an operation with no inverse:

-- `*a` : a uniquely-owned a (no other reference can exist).
-- Uniqueness is one-directional:
share : *a -> a [r]     -- forgetting it is always sound
-- …but there is no  unshare : a [r] -> *a  —
-- an already-shared value can never be made unique again.

Fractional Uniqueness

Consider a huge array and 2 parts of the same program that access it (eventually in parallel) in read-only mode. With the classical uniqueness model, either you lose the uniqueness guarantee (non-unique, no mutation), or you keep the uniqueness guarantee (1 unique, 1 mutation). This friction has been solved by Marshall et al. in the paper Functional Ownership through Fractional Uniqueness . They leverage graded modal types to model the granularity of uniqueness.

The central idea is that uniqueness should not be viewed as a binary property, but rather as a resource that can be partially shared. Instead of distinguishing only between "unique" and "non-unique", fractional uniqueness assigns degrees of ownership to references, allowing the system to track how much of the original uniqueness guarantee is preserved.

Intuitively, a fully unique value corresponds to full ownership, while borrowed views correspond to partial ownership. These partial views can coexist safely, as long as their combined permissions do not exceed the original uniqueness guarantee. This provides a controlled form of aliasing: references may exist simultaneously, but only with explicitly tracked permissions.

This perspective aligns closely with fractional permissions in separation logic , where ownership of a resource can be split into fractions that individually allow read access, but only the full fraction permits mutation. In this setting, mutation is not forbidden by aliasing itself, but by the absence of full ownership.

In Granule this shows up directly in the borrowing interface. A borrowed reference &p a carries a permission p — a fraction in \((0, 1]\), with \(1\) meaning full ownership. Reading needs any positive fraction; writing needs the whole thing:

readArray  : &p (Array Float) -> Int -> (Float, &p (Array Float))         -- any p
writeArray : &p (Array Float) -> Int -> Float -> &p (Array Float)         -- requires p = 1

-- Permissions split for read-sharing and recombine for exclusive access:
split : &p a -> (&(p/2) a, &(p/2) a)
join  : &p a -> &q a -> &(p+q) a            -- only when p + q ≤ 1

The constraint \(p + q \le 1\) on join is the whole game: many immutable borrows can coexist (their fractions sum to at most one), but a write demands \(p = 1\), which is reachable only once every other share has been given back.

From a programming perspective, this gives a precise explanation of borrowing: an immutable borrow corresponds to splitting ownership into fractional shares , while a mutable borrow requires temporarily regaining the full ownership fraction. Once the mutation is completed, ownership can be re-split or restored to a unique state.

In this sense, Rust's borrow checker can be understood as enforcing a dynamic discipline over a static fractional ownership system: it ensures that at any point in time, the sum of all active references never exceeds full ownership, and that exclusive access is available whenever mutation occurs.

Connecting Fractional Uniqueness to Linearity and Uniqueness

The introduction of fractional uniqueness clarifies the relationship between linear and uniqueness types. Rather than treating these as fundamentally different systems, we can view them as two limiting cases of the same underlying structure: a graded notion of ownership.

Linear types correspond to the extreme case in which ownership cannot be split at all. A value must be consumed exactly once, and therefore no fractional views are permitted. In this sense, linearity enforces a single-threaded usage discipline over resources.

Uniqueness types, in contrast, correspond to the case where full ownership is required for mutation, but ownership itself can be temporarily weakened by forgetting uniqueness information. This introduces a directional asymmetry: uniqueness can be safely discarded, but cannot be reconstructed from unrestricted values.

Fractional uniqueness refines this picture by making the "strength" of ownership explicit in the type system. Instead of treating aliasing as a boolean property, we index ownership by a graded structure that tracks how permissions are distributed across the program.

From Ownership to Borrowing

In this setting, borrowing is no longer a primitive concept, but a derived operation on ownership fractions. An immutable borrow corresponds to splitting a unique resource into multiple fractional views, each of which carries read-only permission. A mutable borrow corresponds to temporarily reassembling all fractions into a single exclusive ownership token.

This explains why mutation in systems like Rust requires exclusivity: mutation is not prohibited because of type-theoretic restrictions alone, but because it requires reconstructing a full ownership fraction that cannot coexist with any other active view.

Consequently, borrowing can be seen as a controlled decomposition of uniqueness rather than an exception to it. The type system does not abandon uniqueness during borrowing; instead, it refines it into a structured set of permissions that evolve over time.

A Unifying Perspective

We can now summarize the relationship between the three systems as follows:

From this perspective, linearity and uniqueness are not competing notions, but orthogonal projections of a more general system of graded resource reasoning. Linearity constrains temporal usage, uniqueness constrains global aliasing structure, and fractional uniqueness mediates between them by tracking how both evolve under composition.

Region-based Types

A different route to memory safety without a garbage collector is to use regions. Introduced by Tofte and Talpin (see also ), region-based systems associate every value with a region—a named scope of memory. Values are allocated into a region and freed all at once when the region's scope ends. The type system tracks, as an effect, which regions each expression reads from and writes to, and guarantees that no value outlives its region, ruling out dangling-pointer dereferences.

Concretely, a region is introduced by a scoped letregion binder, and allocation says where a value lives with at:

letregion ρ in
  let p = (1, 2) at ρ      (* the pair is allocated in region ρ *)
  in fst p + snd p         (* …and read back from it *)
(* ρ, and everything in it, is freed here at the letregion boundary *)

A function type then carries a latent effect recording the regions a call touches—for example \((\textsf{int}, \rho_1) \xrightarrow{\{\,\mathsf{get}\,\rho_1,\ \mathsf{put}\,\rho_2\,\}} (\textsf{int}, \rho_2)\)—and the checker uses those effects to prove that no value ever escapes its region.

Regions are the intellectual ancestor of Rust's lifetimes: the borrow checker enforces that a reference cannot outlive the scope of the data it points to. The lineage is explicit—Rust's design was informed by work on regions and on alias types .

Ownership Types

Long before Rust made the word famous, ownership was developed as a way to understand aliasing in object-oriented languages . The aim is to give a high-level structural view of objects and references—much as ordinary types give a structural view of data—by recording which object "owns" which, and forbidding references that would let an object's internals leak out. A whole family of related notions grew around this idea: islands , which fence a cluster of objects off behind a single bridge; balloon types , which keep an object's entire reachable state private; and external uniqueness , which only requires the one reference into a structure from the outside to be unique, while internal aliasing stays free.

Rust is where ownership now sees the most use, as the mechanism behind its memory safety. Several formalizations pin down what the model actually means: RustBelt gives a lower-level, machine-checked semantics aimed at verification, while Oxide offers a higher-level encoding meant for theoretical work; Stacked Borrows proposes a concrete aliasing model for the unsafe fragment, and lighter-weight accounts of lifetimes and borrowing exist too . Rust is not alone here—Swift incorporates similar ideas, and ownership keeps spreading into new settings.

Day to day, that model surfaces as the shared-XOR-mutable rule: at any moment a value may have any number of read-only borrows or exactly one mutable borrow, but never both:

let mut v = vec![1, 2, 3];
let r = &v;             // shared (read-only) borrow of v
// v.push(4);           // ✗ error: cannot borrow `v` as mutable
println!("{r:?}");      //          while the shared borrow r is live

let m = &mut v;         // once no shared borrow remains, an
m.push(4);              // exclusive borrow re-enables mutation

That spread is the interesting part for us. Ownership is being pushed into languages with manual memory management , used to decide which functional programs can run in place without allocation , and—as a later section explores—scaled to higher-order and polymorphic code through reachability types . Seen this way, ownership is less a single feature than a recurring answer to the question the whole post circles around: who is allowed to see, and to change, a given piece of state.

Linear Capabilities and Alias Types

A turning point in this story was the realization that the pointer to a piece of memory and the permission to use it need not be the same thing. The calculus of capabilities and alias types pry the two apart: a pointer becomes an ordinary, freely-copyable value, while a separate capability—a linear token, written \(\{\rho \mapsto \tau\}\)—grants the right to dereference (and to deallocate) the location \(\rho\) it names.

That one move buys a great deal over Wadler-style linearity, where "pointer" and "permission to dereference" are one and the same. Here you may keep as many aliases to an object as you like—copy them, store them—provided the single capability that authorises access stays unique. Because the capability also records the content's type, it licenses a strong update: overwriting a location with a value of a different type, and updating the location's type to match.

The borrowing trick we keep meeting reappears here in its sharpest form: a linear capability can be temporarily weakened to a shared one and then recovered—the focus operation of Fähndrich and DeLine , a close cousin of Wadler's let! and of C99's restrict keyword—while their adoption mechanism lets a freshly-allocated unique object be handed to a region and aliased thereafter. This lineage is what made Cyclone , a memory-safe dialect of C with regions and unique pointers, practical, and it feeds directly into the reachability and separation systems later in this tour.

A word of warning, since the post is by now thick with the term: "capability" is overloaded. The linear capabilities here are permissions to dereference memory; the reference capabilities below are qualifiers on a reference; and object capabilities are unforgeable references that carry authority. The first kind is, in fact, almost exactly a separation-logic assertion : \(\{\rho \mapsto \tau\}\) is a points-to fact, and combining two capabilities is separating conjunction. This whole branch of the family is surveyed beautifully in Pottier's tutorial .

Restricting Access: Effects and Capabilities

So far the bookkeeping has lived on values and references. This family moves it elsewhere—onto the typing judgment itself, or onto the tokens a piece of code is handed—to constrain not just what may be touched, but what a computation is allowed to do with it.

Effect Systems

An effect system enriches the typing judgment so that it describes not only the type of a value but also the effects—the observable actions—that producing it may perform. The judgment takes the shape \(\Gamma \vdash e : \tau \mathbin{!} \varepsilon\), where \(\varepsilon\) records reads, writes, I/O, exceptions, and so on. Effects compose bottom-up: a compound expression's effect is the join (least upper bound) of its parts.

Effect systems were introduced by Gifford and Lucassen , with polymorphic effects following shortly after . Modern descendants include Koka's row-polymorphic effects and the algebraic effects of OCaml 5 and Eff, with handlers that give operations their semantics. In Koka, the effect a function may perform is part of its type, and a handler is what discharges it:

effect exc
  ctl throw(msg : string) : a    // a control operation

fun risky() : exc int            // the type advertises the `exc` effect
  throw("oops")

fun main() : console ()
  with ctl throw(_) -> -1        // the handler discharges `exc`…
  println(risky())               // …so `main` itself is exc-free, and prints -1

Their strength is precision: effect systems are bottom-up analyses that inspect what code actually does. Their weakness is the flip side—reasoning about global invariants and aliasing through effects alone needs heavy naming machinery . Keep this "bottom-up vs. top-down" contrast in mind; it is the key to the capability systems below.

Qualified Types and Type Qualifiers

Qualified types, formalized by Jones , extend types with predicates that must hold before a type can be used. Haskell's type-class constraints are the canonical example: Eq a => a -> a -> Bool reads "works for any a that satisfies Eq". The predicate is not magic—it elaborates into an extra dictionary argument the compiler inserts and fills in for you:

member :: Eq a => a -> [a] -> Bool          -- qualified type, predicate `Eq a`
-- elaborates (conceptually) to an explicit evidence argument:
member ::   EqDict a -> a -> [a] -> Bool    -- the dictionary is passed implicitly

That "implicit evidence, inserted by the compiler" pattern is exactly what linear constraints reuse—only there the evidence is linear.

Type qualifiers, due to Foster, Fähndrich, and Aiken , instead attach annotations such as const or readonly directly to types and propagate them by subtyping. It is a lightweight way to express many useful properties without touching the core type language.

The two ideas meet in linear constraints : constraints carrying a multiplicity (linear or unrestricted). A linear constraint must be consumed exactly once, like a linear argument, but the compiler passes it implicitly instead of making you thread it by hand. This recovers much of the convenience lost to linear bureaucracy—enough to encode Rust-style ownership as a Haskell library rather than a language feature.

Reference Capabilities

A reference capability system attaches a permission qualifier to a reference rather than to the object it points at. Two references to the same object can therefore carry different capabilities—in contrast to linear types, where it is the value itself that is restricted. A common vocabulary :

The type system propagates capabilities transitively: reading a field through a readable reference yields a readable result, even if the field was declared writable. These systems power safe parallelism—if no thread holds a writable reference shared with another, data races are impossible —as well as method-purity inference and deep object immutability. Capability ideas for uniqueness and borrowing go back to Haller and Odersky .

Pony turns this vocabulary into six keywords written on each reference—iso (isolated: the only reference, sendable), val (deeply immutable, freely shareable), ref (mutable but not sendable), box (read-only view), trn (writable now, convertible to val), and tag (identity only, no read or write):

let greeting: String val = "hello"                   // immutable: any actor may share it
let buffer:   Array[U8] iso = recover Array[U8] end  // the ONLY reference; sendable

fun size(s: String box): USize =>                    // box: read-only view — accepts a val OR a ref
  s.size()

The defining trade-off is that reference capabilities perform top-down analysis: they reason about what flows into code without inspecting its internals, which keeps them simple and lets them work even on precompiled libraries. The cost is a use–mention confusion: holding a writable capability means you could write, not that you do—an effect system, by contrast, can tell mentioning a reference apart from actually using it.

Object Capabilities (ocap)

Object-capability systems (ocap) are an architectural security model rather than a type system. Rooted in operating-systems work by Lampson and systematized by Levy , the central idea is that a capability is an unforgeable token that simultaneously names a resource and authorises access to it.

In an object-capability language, object references are capabilities: if you cannot obtain a reference, you cannot call the object's methods or observe its state. There is no ambient authority—no global mutable state, no System.getenv, no unrestricted reflection—so security follows from the topology of the object graph. Miller's thesis formalizes this and states the Principle of Least Authority (POLA): hand each component only the capabilities it strictly needs, which defuses the "confused deputy" problem. Languages and runtimes in this tradition include E, Joe-E, Caja, and Deno (with its --allow-net / --allow-read permission flags).

Deno is the most familiar taste of POLA today: a script starts with no ambient authority and is granted only the capabilities you name, scoped as tightly as you like:

deno run app.ts          # no authority: any fetch() or Deno.readFile() is denied

# grant only what's needed — and only for the exact host / path:
deno run --allow-net=api.example.com --allow-read=./data app.ts

Tracking State and Separation

The final family watches how things change. Instead of fixing a value's permissions once and for all, these systems track how its state—or its web of aliases—evolves over time, and use that to keep genuinely separate things provably apart, even across closures and threads.

Typestate

Typestate adds to a variable's type information about its state at a given program point. A File might move through typestates Closed and Open; the type system tracks the transitions, so read is only well-typed on an open file, and a file must be closed before it leaves scope. Even without native support, Rust encodes this by making the state a type parameter:

struct Open; struct Closed;                  // states as zero-sized marker types
struct File<S> { fd: i32, _state: PhantomData<S> }

impl File<Closed> {
    fn open(path: &str) -> File<Open> { /* … */ }
}
impl File<Open> {
    fn read(&self) -> String { /* … */ }
    fn close(self) -> File<Closed> { /* … */ }  // consumes the Open file
}
// `read` exists only for File<Open>; calling it on a File<Closed> is a type error.

Typestate is orthogonal to linearity but pairs naturally with it: a linear file handle cannot be duplicated (no double-close) nor silently dropped (no leak). The challenge is aliasing—if two references point to the same file, transitioning one invalidates the other's assumption—which is exactly what linear or affine disciplines rule out.

Reachability Types

Reachability types tackle a long-standing problem: how to reason about aliasing and separation in higher-order languages, where closures can capture references and escape their defining scope—something Rust's "shared XOR mutable" rule cannot express without runtime reference counting. The idea is to give every type a qualifier: the set of program variables transitively reachable from the value.

val x = new Ref(0)   // type: Ref[Int]{x}     — reachable only via x
val y = x            // type: Ref[Int]{x, y}  — reachable via x and y

The key property is preservation of separation: if two values have disjoint qualifiers, their object graphs are guaranteed disconnected at runtime—precisely what you need to hand one of them to another thread without risking a data race. This inverts the usual ownership philosophy: rather than starting from a strict unique-access invariant and relaxing it via borrowing, separation falls out as a derived property of qualifier disjointness, which scales more gracefully to functional abstraction.

Concretely, disjointness of qualifiers is the side-condition the checker verifies before letting two computations run in parallel:

val a = new Ref(0)        // Ref[Int]{a}
val b = new Ref(0)        // Ref[Int]{b}
par(a := 1, b := 2)       // ✓ {a} ∩ {b} = ∅   — disjoint, safe in parallel
par(a := 1, a := 2)       // ✗ {a} ∩ {a} ≠ ∅   — overlap rejected: would race

The original system, \(\lambda^{*}\), is monomorphic, and a naïve polymorphic extension turns out to be unsound. Polymorphic reachability types, \(\lambda^{\Diamond}\) , fix this by tracking only single-step reachability and computing transitive closures on demand, with a freshness qualifier \(\Diamond\) for values whose reachable set may still grow. In parallel, Capture Types for Scala (the calculus CC<:□) track the directly captured variables of a value and use boxing to cross generic boundaries soundly; their primary application is safe scoped effects via capabilities. A complementary line by Milano et al. tracks a heap-domination invariant: an iso reference dominates its whole reachable subgraph, so it can be sent to another thread atomically, with temporary violations tolerated until a transfer forces recovery.

Degrees of Separation: the Capture Separation Calculus

Most systems so far enforce a strict anti-aliasing invariant globally and relax it locally. The Capture Separation Calculus (CSC) takes the opposite stance, which its authors call the control-as-you-need paradigm: aliases to mutable state are permitted by default and merely tracked, and separation is enforced only where data races are actually possible.

The tradition CSC reacts against is broad: linear and uniqueness types keep at most one live reference; ownership types stop aliases from crossing object boundaries; fractional permissions split a write permission into read-only shares that must be recombined before the next write. All of these enforce a strong invariant globally and relax it locally—so adopting any of them into an existing codebase usually means non-trivial refactoring.

The control-as-you-need principle has a deep ancestor in Reynolds's Syntactic Control of Interference (later revisited ), which makes interference syntactically detectable rather than forbidding it outright. CSC builds directly on Capture Types, adding a separation degree: a type-level annotation on a parameter saying how much of the current context that argument must be separated from. With no annotation, aliases are free; annotations—usually inferred—appear only where parallelism makes data races possible. The main concurrency construct is parallel composition, written || (sugar for a parallel let); a separation degree sep{a} on a parameter declares it must stay separated from a:

def resetBoth(a:        Ref[Int]^{cap},
              sep{a} b: Ref[Int]^{cap}): Unit =
  a.set(0) || b.set(0)    // || runs both sides at once; sep{a} proves they cannot race

The checker verifies that the two sides of a || touch sufficiently separated state—here, that b is disjoint from a—so that no mutable state is reached concurrently from both sides. A reader capability behaves like a fraction of a full capability, but, unlike traditional fractional permissions, it may coexist with the full capability and be used together sequentially; only their parallel use is prohibited.

Concretely, what is forbidden is putting a reader and the full capability—or two full capabilities—on the two sides of a || at once:

val r: Ref[Int]^{cap} = new Ref(0)   // {cap} = may read AND write r;  {rdr} = a read-only fraction

r.get    || r.get      // ✓ reader ∥ reader  — two reads never race
r.get    || r.set(1)   // ✗ reader ∥ writer  — a read racing a write is a data race
r.set(1) || r.set(2)   // ✗ writer ∥ writer  — two writes race

val x = r.get           // here r is used as a reader…
r.set(x + 1)            // …then with the full capability — fine: the two uses are sequential

The Landscape, Summarized

These systems are not competing alternatives so much as complementary tools for different problems:

The deeper pattern across all of these: they make the flow of authority, access, or resources explicit and checkable at compile time. They differ in where the information lives (on the value, the reference, the type context, the effect annotation, or the reachability qualifier), which structural rules they restrict, and how the analysis runs—bottom-up from expressions, top-down from contexts, or via the shape of the heap graph itself.

A closing pointer for the curious: for a guided tour of the capability-and-region branch, the F. Pottier's tutorial slides are an excellent, and delightfully readable, companion to this post.

¹ An unrestricted value is one that satisfies all structural rules of classical logic, allowing contraction, weakening, and exchange without restriction. ↩