Skip to content

Home

Jump to bottom
Jonathan D.A. Jewell edited this page May 21, 2026 · 4 revisions

Ephapax — once for all

ἐφάπαξ: every resource used exactly once.

A dyadic linear+affine type system for compile-time WebAssembly memory safety. Compiler-enforced — no garbage collector, no allocator runtime, no use-after-free, no leaks.

The core calculus is mechanically formalised in both Coq (dynamic semantics + soundness) and Idris2 (region-linearity theorems + provably-total parser/typechecker). Both run on every push.

Start here, by audience

You are… Read
Browsing — what's this even? What is Ephapax? below, then README
About to write .eph code QUICKSTART-USER → examples/
Hacking on the compiler QUICKSTART-DEV → TOPOLOGY.md
Working on the formal proofs formal/PRESERVATION-HANDOFF.md → PROOF-NEEDS.md
Doing release / governance QUICKSTART-MAINTAINER
Curious about the design docs/vision/EPHAPAX-VISION.adoc → docs/specs/DESIGN-DECISIONS.adoc

What is Ephapax?

A programming language with:

  • Dyadic discipline — each binding is either affine (let — used at most once, weakening allowed) or linear (let! — used exactly once, weakening forbidden). The type checker enforces.

  • Region-based memory — allocations live in named regions (region r: ...); when the scope ends, the runtime bulk-frees every resource in it. No per-object allocator metadata, no per-object frees.

  • Second-class borrows — &x gives temporary access without consuming x. Borrows cannot be stored, cannot escape, cannot outlive the borrowed resource.

  • WebAssembly target — wasm32-unknown-unknown primary, Cranelift native secondary.

  • No GC, no allocator runtime — region exits do bulk deallocation. No tracing collector, no refcounting, no per-object frees.

region r:
    let s1 = String.new@r("hello, ")
    let s2 = String.new@r("world")
    let len = String.len(&s1)              -- borrow: doesn't consume s1
    let result = String.concat(s1, s2)     -- consumes both
    result
-- region exits; any remaining allocations bulk-freed

Proof status at a glance (2026-05-20)

Coq (formal/)

Theorem Status
no_leaks ✅ Qed
subst_preserves_typing ✅ Qed
typing_ctx_transfer ✅ Qed
region_env_perm_typing, region_add_typing, region_shrink_preserves_typing ✅ Qed
preservation 🟡 12 open / 910 closed (in flight)

The preservation reduction story is recent and load-bearing:

  • 910 → 29 goals via the standard preservation pattern (PR #102)
  • 29 → 22 goals via universal-IH revert (PR #106)
  • Region-invariance lemma step_R_eq_or_touches_region landed (PR #114) — infrastructure for the per-case work
  • 22 → 12 goals via 10 per-case manual closures (PR #116) using the new lemma
  • Phase 1 scaffold of the closure plan landed (PR #121): Lemma B step_output_context_eq stated; per-case discharges next
  • 12 → 0 is the canonical 5-phase plan in ROADMAP §"Preservation closure plan". ~3 sessions of focused work. See PRESERVATION-HANDOFF.md.

An earlier in-file comment claimed preservation was Qed-closed 2026-04-27. That claim was unsubstantiated; coqc 8.18.0 rejects. PR #92 (2026-05-20) corrected the status. The reduction chain above is the honest closure work.

Idris2 (idris2/src/Ephapax/ + src/formal/)

Frontend — parser, typechecker, IR codec. All 9 files compile under %default total (8 files) or %default covering (1 file, the recursive-descent parser).

Module Default
IR/SExpr, Parse/Stream, Parse/Util, Parse/Lexer, Affine/Typecheck %default total
IR/AST, IR/Decode, Affine/Emit %default total + 14 retained covering (documented SCT limits)
Parse/Parser %default covering (LL(k) Stream-recursion; fuel refactor deferred)

Zero believe_me, zero assert_total, zero assert_smaller in the entire frontend. Outcome of the 9-PR campaign #89–#100 merged 2026-05-20.

Region-linearity theorems (src/formal/): noEscapeTheorem, regionSafetyExtract, noGCExtract, orthogonalityLemma, splitLinearCoverage. All complete with zero unsafe patterns.

Documentation by topic

Language design

Formal proofs

Implementation

Project status

Contributing

Highest-leverage open work

In priority order, for someone looking to contribute substantively:

  1. Close preservation to Qed. Multi-day proof engineering; 22 of 910 goals remain. See PRESERVATION-HANDOFF.md for the per-case checklist. Three lemmas to write: (a) region invariance for non-region step constructors, (b) linearity- context preservation for sibling premises in congruence cases, (c) region-env weakening for non-values. The last is the documented language-design item.

  2. Fuel-refactor Parse/Parser.idr from %default covering to %default total. ~30 mutually-recursive parser combinators threaded through a Stream record; the recursion is real structural recursion the Idris2 SCT can't trace. Fueling all of them is a substantial refactor, deferred to a later campaign.

  3. Type-checker completion (ephapax-typing) and WASM codegen for lambda/app (ephapax-wasm). These are the v0.1 release blockers on the implementation side.

  4. Native backend via Cranelift (v0.2.0).

Related projects (hyperpolymath ecosystem)

  • Gossamer — Zig + WebKitGTK desktop app shell that uses Ephapax for its backend.
  • typed-wasm — 10-level type safety for WASM memory; companion library.
  • proven — formal-verification library; Ephapax depends on it for hardened string handling at the IR boundary.
  • echo-types — constructive Agda formalization of fiber-based structured loss. Sister project: Agda where Ephapax is Coq+Idris2.
  • nextgen-languages — parent repository tracking 14+ experimental languages including Ephapax.

Licence

PMPL-1.0-or-later. MPL-2.0 fallback available.

"Once for all" — every resource used exactly once.

Ephapax wiki

Topic guides

In the repository

Quickstarts

Clone this wiki locally