Typed Revertible Effects: Inverse-or-Emit as a Checked Guarantee

Pitch

A compiler can make "every effect is undoable or visibly irreversible" a checked property by classifying effects as acquire, pure, witnessed or emission, and can then derive component lifecycle and LIFO undo from the dependency graph so the author never writes teardown code.

Abstract

Systems that load and unload components at run time depend on undo code that is written once, exercised rarely and wrong quietly. Resource-safety disciplines such as RAII, bracket and defer help, but nothing forces a mutation to name its inverse, and nothing separates an effect that can be undone from one that crossed the system boundary. We present revl, a language where reversibility is part of the type structure. Every effect is classified as acquire, pure, witnessed or emission. The checker's central rule (G4): a mutation either carries a well-shaped inverse or is an explicit, approval-gated emission. The rule is refined by capability scopes, so a service declaration emission[db] bounds where any provider may cross, and the bound is computed as a least fixed point over the call graph. Because code outside effect forms is pure, the teardown accumulator holds every mutation at the head granularity the proof ledger certifies, and lifecycle (activation, deactivation, LIFO undo) is derived from the dependency DAG with no author-written lifecycle code. Typed holes let a draft type-check around missing parts while noting them as unmet obligations that admission and every backend refuse. We describe the rule set, the decode table that separates guarantees inherited from the Cordis paradigm, revl-original ones and ordinary type theory, and the implementation and test corpus (186 rejection reproducer files, 47 of them with g4 in the name). We state what is not claimed: inverse semantics are checked for presence and shape, not correctness, and the foreign-code boundary is trusted but enumerable. Lean models of the rules and a differential oracle against the shipped checker are reported in a companion paper.

Problem and claim

Cordis (the paradigm revl descends from) has revertible effects as a discipline: its theorems rest on hypotheses a library can only ask programmers to respect (README.md:36-41). In practice that means undo logic is a write-only code path, and the distinction between "reversible" and "crossed the boundary" lives in programmer memory. Existing resource-safety mechanisms (RAII, bracket, defer, saga libraries) pair an acquisition with a release at best by convention; none is a type-level obligation with a checked escape hatch.

The claim is narrow and checkable: in revl, (1) every mutation form is classified, (2) a mutation without a declared inverse is refused unless it is marked as an emission, (3) the set of host boundaries a provider may cross is bounded by its service declaration and that bound is checked transitively, and (4) lifecycle and undo order are derived, not written. The paper does not claim that an undo expression truly reverts its effect; the project docs say this is undecidable in general and opt-in (verified) (docs/vision.md:95-99).

The positioning sentence the project itself uses is "Cordis has revertible effects as a discipline; revl makes them a type system", and the same page adds "Everything beyond that is roadmap, not claim" (docs/vision.md:113-114). The paper adopts that restraint. The RAII-to-Rust analogy is rhetorical framing for the introduction, not a result.

Contributions

1. An effect classification (acquire, pure, witnessed, emission) with rule G4, inverse-or-emit, and its capability-scoped refinement: a provider's reachable capability set must be a subset of the scope in its service declaration (docs/capabilities.md:126-170; src/revl/lower.py:15055-15083).
2. A transitive analysis for that rule: a least fixed point over the call graph, lifted from a boolean to a set of capabilities, with recursion terminating (src/revl/emission_analysis.py:157-200).
3. Implicit lifecycle: activation and deactivation derived from the dependency DAG, with G2 (one provider per key, per realm) and G3 (acyclic) checked at link time (DESIGN.md:154-160, DESIGN.md:223-235).
4. Checked undo: because code outside effect forms is pure (G6), the accumulator is complete at head granularity; host acquisitions must undo as their release on the bound handle, and no_residue fails when a bracket's undo did not reverse its write (README.md:127-135; docs/rejections.md:173-232; CHANGELOG.md:472-477).
5. A decode table that assigns refusal codes an enforcement point and, where sourced, an origin (Cordis-inherited, revl-original, standard type theory) (docs/guarantees.md).
6. Typed holes as a first-class unmet obligation: checked around, noted, refused at admission and by every backend (docs/holes.md; src/revl/holes.py:72-93; tests/test_holes.py:261-327). Sound typing with Opt[T] absence and a documented gradual frontier is a supporting piece (docs/roadmap-archive/02-done-dependency-order-as-built.md:29-31).

Related work

Evidence on main

Numbers that exist

• 186 files in examples/rejections. 47 have g4 in the filename; the rest are other rules.
• G4 differential-oracle rows reported by the proof status file: 182 G rows, 25 P rows, 6 agree-G4, 36 approval-floor refusals filed under agree-G4 (formal/STATUS.md, G4 row). These are corpus sizes, not accuracy figures.
• G4 Lean layer: 2 + 7 + 10 theorems per the status file; formal/RevL/Theorems/G4_ClassifiedInverseOrEmit.lean contains 7 theorem declarations.
• No measurement exists of how many real bugs G4 prevents, of author burden, or of false-positive rate on third-party code.

Paper outline

1. Introduction: undo as the write-only path; the discipline-to-type-system pitch, stated with the docs' own restraint.
2. Model: components, services, effect ... undo, emit, the four classes.
3. The G4 rule and its capability refinement, with the transitive analysis (set-valued least fixed point).
4. Derived lifecycle and checked undo: G2, G3, G6, G7 as consequences; what "the accumulator is complete" depends on.
5. Typed holes and admission: drafts that check but cannot run.
6. Decode table: which guarantees are inherited, original, or ordinary typing.
7. Implementation and corpus: where each rule is enforced; the rejection corpus; mechanized models and the differential oracle in brief (details in the companion paper).
8. Evaluation: a study on code not written for the rule, and a bug-detection comparison against existing languages, once run.
9. Related work and limits.

Threats to validity and limits

• Semantic inverse correctness is not decided: "The checker proves an inverse is present and well-shaped (G4)" and no more (docs/vision.md:95-99).
• The extern boundary is trusted, not verified, though enumerable (docs/vision.md:100-102). Host body reversal "is still the declaration's assertion" (docs/rejections.md:228).
• G7 (derived LIFO teardown) is "by lowering" and exercised by runtime scenarios; the only checker-side lever is totality of verified fn (docs/rejections.md:530-538). The "derived, hence correct" claim therefore rests on the lowering and runtime, not on a checker rule.
• The metatheorems "transfer by construction, they are not re-proved here" (docs/vision.md:103-110). The Lean layer covers part of the admission judgment; G1 and G6 are partial, and T1-T3 have no theorem (formal/STATUS.md).
• Several origin labels in docs/guarantees.md are "unconfirmed", so the Cordis-inherited split is not fully sourced.
• The corpus is the authors' own; no third-party study exists yet, so the paper cannot say the rules are low-burden.
• The first-class dispatch case is conservatively read as * (unnameable boundary), which can over-refuse.
• The status file (G6 row) says G6 is "full at head granularity", while docs/vision.md:109 says G1 and G6 are "partial".

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 15 checked, 9 corrected.

Cite this draft

@misc{revlp01,
  author       = {Thomas Moussajee},
  title        = {Typed Revertible Effects: Inverse-or-Emit as a Checked Guarantee},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P01.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.