-
-
Notifications
You must be signed in to change notification settings - Fork 0
Comparison to other languages
What / why / where. Ephapax sits in a crowded neighbourhood:
linear types (Linear Haskell, ATS2, Clean, Granule), affine types
(Rust), regions (MLKit, Cyclone), region-and-linearity together
(ATS2, Alms). What Ephapax offers that none of the others have in
the same combination is: dyadic per-binding selection between
linear and affine, plus Tofte-Talpin regions, plus a target of
WebAssembly. This page is a wiki-friendly summary of the
per-language detail in
docs/specs/LANGUAGE-COMPARISON.adoc. If you
want the quality-attribute matrix (dependability / security /
performance / versatility scored 1–10), go to that file.
If you want the underlying mechanisms, read Linear and affine and Region calculus first.
What's similar. Rust has affine ownership: every value is moved by default, and using a moved value is a compile-time error. The basic shape — type system rejecting use-after-move, no GC, predictable destruction — matches Ephapax closely.
What's different. Three big things.
First, Rust is only affine. Every value can be implicitly
dropped at end-of-scope via Drop::drop. There is no way in Rust
to write a type whose values must be consumed — you can write
a destructor that runs on drop, but you cannot statically prevent
the drop from happening. Ephapax's let! form is exactly that:
opt-in to "must be consumed, no implicit drop". See
Linear and affine.
Second, Rust handles scoped memory via lifetimes, which are type-level annotations on references. Ephapax handles it via regions, which are scope-level introductions. Lifetimes are more general (they're properties of arbitrary references); regions are simpler (they're properties of allocation arenas). Cyclone and MLKit are the spiritual ancestors of Ephapax regions; see Region calculus.
Third, Rust's substructural discipline is fixed per-type (every
non-Copy type is affine). Ephapax makes it per-binding (the
same i32 can be let-bound affinely in one place and
let!-bound linearly in another).
What Rust has that Ephapax doesn't. A mature ecosystem,
native backend, SIMD, async/await, decade of production use.
Ephapax targets WASM only (wasm32-unknown-unknown primary,
Cranelift native secondary planned for v0.2.0).
What's similar. Linear Haskell (GHC 9.0+) adds linear
arrows — f :: a %1-> b means f consumes its argument
exactly once. The exactly-once discipline matches Ephapax's
let!.
What's different. Linear Haskell puts the discipline on the function arrow, not on the binding site. A linear function signature says "I treat my argument linearly"; the caller has no say. Ephapax inverts this: the binder decides, and the same value can be bound linearly in one call site and affinely in another. Whether this is better is a real design trade-off — arrow multiplicities propagate further into the type system, while per-binding choices are more local.
Linear Haskell is also non-strict (lazy by default), still has GC, and has no regions. Ephapax is strict, has no GC, and has regions.
What Linear Haskell has that Ephapax doesn't. Vastly more mature typeclasses, Template Haskell, the entire Hackage ecosystem. Linearity is a recent addition to a 35-year-old language; Ephapax is a new language designed around it.
What's similar. MLKit is the canonical region-based implementation of an ML-family language. The region calculus (Tofte-Talpin 1997) is shared between MLKit and Ephapax — same no-escape rule, same region-exit-frees-arena story. MLKit is where the region discipline was first shown to work as a production-grade GC replacement.
What's different. MLKit infers regions automatically;
Ephapax requires them to be named and introduced explicitly
with region r:. The trade-off is predictability vs.
ergonomics: MLKit code looks like normal SML, but the inferred
regions can surprise the author with unexpected long lifetimes;
Ephapax code carries @r allocation tags but the author always
knows which region their allocation lives in.
MLKit also doesn't have a linear discipline at all — region exit
silently drops everything in the arena. Ephapax requires every
let!-bound value to be consumed before the region exits (the
AllLinearsConsumed rule in
check_region).
What MLKit has that Ephapax doesn't. Decades of real deployment, a full SML standard library, region inference. The SML compiler proper.
What's similar. Cyclone (early 2000s, defunct) was the first serious attempt to retrofit substructural safety onto a C-family language, with regions for scoped allocation. The region story in Ephapax is a direct intellectual descendant.
What's different. Cyclone had regions but no linear types
(every pointer was affine by default; consumption was implicit).
It also targeted a C ABI, not WASM, and had to deal with
arbitrary pointer arithmetic — Ephapax just doesn't permit
arbitrary pointer arithmetic, which sidesteps a large fraction
of Cyclone's complexity. Cyclone had @region annotations on
pointers; Ephapax has @region annotations on allocation
sites.
What Cyclone has that Ephapax doesn't. A C-source-compatible front end (Cyclone was meant to be a drop-in safer C). Ephapax is not source-compatible with anything; it's a new language.
What's similar. Granule is a research language with graded modal types — variables carry a quantity (a semiring element) that tracks how many times they may be used. The discipline is finer-grained than Ephapax's: Granule can express "this value may be used at most 3 times" or "this value is used linearly in the imaginary part and affinely in the real part". The exactly-once and at-most-once cases of Ephapax are special cases of Granule's grading.
What's different. Granule's grading is per-binder, like Ephapax's, but the grade is a semiring element rather than a two-valued enum. This is much more expressive and much harder to write. Granule has no regions; it has no codegen story (it's a research vehicle, not a production language). Ephapax is the production-language version of the small fragment of Granule that's easy to use.
What Granule has that Ephapax doesn't. Arbitrary semirings,
graded modal types, a serious theoretical apparatus. Idris 2's
QTT (quantitative type theory) occupies a related point in design
space; see
LANGUAGE-COMPARISON.adoc for the Idris 2
section.
The unique combination, restated:
- Dyadic per-binding linear + affine — no other production language has both disciplines selectable per-binder.
-
Tofte-Talpin regions with explicit naming + the
AllLinearsConsumedrule at exit — region-and-linearity together, with the rule that prevents linear leaks when a region exits. -
WebAssembly target —
wasm32-unknown-unknownprimary; Cranelift native secondary planned for v0.2.0. - No GC, no allocator runtime — region exits do bulk deallocation. No tracing collector, no refcounting, no per-object frees.
- Mechanically formalised — Coq (substitution-based small-step semantics + soundness work) and Idris 2 (region-linearity structural theorems, plus a totality-checked frontend implementation). See Proof status for the honest "910 closed, 12 open" picture on preservation.
Other languages have subsets of this. The combination is
distinct. Whether that combination is worth having — versus
sticking with Rust + GC, or going to a dependently-typed system —
is the question
docs/vision/EPHAPAX-VISION.adoc tries to answer.
- Linear and affine — the dyadic discipline
- Region calculus — the Tofte-Talpin region rules
- Two-phase compiler — Idris2 frontend + Rust backend split
- What can go wrong — the failure modes this all catches
- Proof status — what's mechanically proven
- Glossary — underlying terms
-
docs/specs/LANGUAGE-COMPARISON.adoc— full quality-attribute matrix + 10-language detail -
docs/vision/EPHAPAX-VISION.adoc— why this combination