Region calculus

Region calculus

What / why / where. Ephapax has no garbage collector and no allocator runtime. Instead, every dynamic allocation lives in a named region introduced by region r:; when the region's scope ends, the runtime bulk-frees every resource in it, no per-object metadata required. The discipline is due to Tofte and Talpin (1997). The Coq side proves it preserves typing (region_env_perm_typing, region_add_typing, region_shrink_preserves_typing in formal/Semantics.v). The Idris2 side proves it can't leak (noEscapeTheorem, regionSafetyExtract in src/formal/Ephapax/Formal/RegionLinear.idr).

If you want the language-user view of regions, read Linear and affine first for the per-binding discipline that interacts with this one. For the full pipeline picture, see Two-phase compiler.

---

What a region is

A region is a lexical scope plus an allocation arena. Syntactically:

region r:
    let s1 = String.new@r("hello, ")
    let s2 = String.new@r("world")
    let result = String.concat(s1, s2)
    result
-- region r exits here: any leftover allocations are bulk-freed

(from conformance/valid/region_basic.eph)

Three pieces matter:

1. region r: introduces a fresh region name r and opens a scope. The name r is in scope only within the indented body.

2. String.new@r("...") allocates a String into region r. The @r is an allocation-site annotation, not a type annotation — the resulting value is just a String, but its storage lives in r.

3. When the body finishes, the region exits. Every allocation tagged @r is freed in one shot. There is no per-object destructor, no refcount decrement, no tracing scan — the region's underlying buffer is reset to empty.

This is what "no GC, no allocator runtime" actually means in Ephapax: the runtime ships one function, region_exit, that frees a whole arena. Nothing else manages memory.

---

The escape rule

The dangerous case is returning a region-allocated value past the region's exit:

fn example() -> String {
    region r:
        let s = String.new@r("hello")
        s   // ERROR: s lives in r, cannot escape r's scope
}

(from conformance/invalid/region_escape.eph, error E003)

The typechecker rejects this. The rule is that the body of region r: ... may not have a type that mentions r. In ephapax-typing/src/lib.rs, the function check_region enforces this:

// Rule 1: NoRegionInType
if body_ty.references_region(name) {
    return Err(self.at(s, TypeError::RegionEscape { region: name, ty }));
}

// Rule 2: AllLinearsConsumed
for (var_name, entry) in &self.ctx.vars {
    if entry.region.as_ref() != Some(name) { continue; }
    if entry.demands_consumption() && !entry.used {
        return Err(self.at(s, TypeError::RegionLinearNotConsumed { ... }));
    }
}

Two checks fire on region exit:

• No escape — the body's result type may not reference r. This is what stops s (of type String@r) from being returned.
• All linears consumed — every let! binding allocated in r must have been used. This is what stops a leaked database handle from disappearing when its region exits. (Error E004, conformance/invalid/region_linear_not_consumed.eph.)

The second check is what makes regions interact correctly with the linear discipline of let!. Affine let bindings can be dropped at region exit (they're bulk-freed with the arena); linear let! bindings cannot (they have to be explicitly consumed first, e.g. by Db.close(conn)).

---

Nested regions and outlives

Regions nest. An inner region can borrow values from an outer region — the outer outlives the inner:

fn nested_regions() -> i32 {
    region outer:
        let! db = Db.connect@outer("postgres://localhost/test")
        region inner:
            let result = Db.query(&db, "SELECT count(*) FROM users")
            result
        // inner exits: result freed; db still alive in outer
        Db.close(db)
        0
}

(from conformance/valid/nested_regions.eph)

The borrow &db is OK because db lives in outer, which outlives inner. The reverse — borrowing from an inner region in an outer scope — would fail the no-escape rule.

---

What the Coq side proves about regions

formal/Semantics.v has three closed theorems about the region environment R (the list of currently-active regions in the operational semantics):

Theorem	What it says	Where
region_env_perm_typing	Typing is invariant under permutation of R. The region environment is a set; the order Coq happens to store it in doesn't matter.	Semantics.v:2960
region_add_typing	Adding a fresh region to R preserves the typing of any well-typed body. This is what lets region r: open a scope safely.	Semantics.v:3042
region_shrink_preserves_typing	Removing a region from R preserves typing — but only for value-form bodies. This is what makes S_Region_Exit typing-preserving when the body has reduced to a value.	Semantics.v:3107

The last one is restricted to value forms because shrinking a region is unsound for non-values: an unreduced EBorrow against a location in the shrunk region would silently start ranging over the wrong arena. The restriction is what makes the proof go through, and the corresponding open case in preservation (S_Region_Step + T_Region_Active, see PRESERVATION-HANDOFF.md) needs a non-value weakening lemma to close — see Proof status.

---

What the Idris2 side proves about regions

src/formal/Ephapax/Formal/RegionLinear.idr is a separate, Idris2-side development. Where Coq proves dynamic properties of the reduction relation, Idris2 proves structural properties of region-scoped types.

The headline result is noEscapeTheorem:

0 noEscapeTheorem : (r : RegionId) -> NoRegionInType r (Scoped r a) -> Void

In English: there is no proof that a Scoped r a (a type tagged with region r) is "free of region r". The type-level encoding of region-tagging makes escape not expressible, not just forbidden. The proof is two lines of case analysis; the construction proves itself.

Companion theorems regionSafetyExtract, noGCExtract, orthogonalityLemma, and splitLinearCoverage establish that:

• A region block carries the proof that its result is region-free (regionSafetyExtract).
• The pair (region-free result, all linears consumed) is packaged together at region exit, with no runtime tracing (noGCExtract).
• Changing a binding's qualifier (linear ↔ affine) doesn't change what can escape from a region (orthogonalityLemma).
• Splitting a context's linear bindings across a binary operation covers every linear binding exactly once (splitLinearCoverage, PR #85) — generalises the older nonDiminishment lemma from head-position to all linear bindings.

All five are under %default total with zero believe_me, zero postulates, zero assert_total.

---

How regions compare elsewhere

The Tofte-Talpin region calculus was originally developed for MLKit: Standard ML compiled with regions instead of GC. Three differences from MLKit:

• MLKit infers regions automatically; Ephapax requires them to be named and introduced explicitly. The trade-off is predictability vs. ergonomics — Ephapax users always know which region their allocation lives in.
• MLKit doesn't have a linear discipline. Region exit can drop values silently; Ephapax requires linear values to be explicitly consumed first.
• MLKit targets native code; Ephapax targets WASM (wasm32-unknown-unknown primary, Cranelift native secondary).

Other points of reference:

• Cyclone had regions and pointer-arithmetic safety, but no linear discipline.
• Rust does not have regions — lifetimes plus the borrow checker cover overlapping ground, but with a different ergonomic profile. Rust lifetimes are properties of types; Ephapax regions are properties of scopes.
• ATS2 has optional regions (and linear types), but the language is much heavier overall.

See Comparison to other languages for a paragraph-each summary, and docs/specs/LANGUAGE-COMPARISON.adoc for the full matrix.

---

Cross-references

• Linear and affine — the per-binding discipline that regions interact with
• What can go wrong — full catalogue of what the region rules catch
• Two-phase compiler — how regions flow through the pipeline to WASM
• Proof status — what's mechanically proven about regions; what's still open
• Glossary — "region", "region-env weakening", "no-escape", "Tofte-Talpin"