Home

Ephapax

A dyadic language -- one part affine, the other linear -- with safe memory management targeting WebAssembly.

Quick Start

See the main README for installation and usage.

just idris-build    # Build Idris2 ABI
just golden         # Run golden tests

Key Concepts

• Dyadic binding modes -- let x = ... (affine: use at most once, implicit cleanup) and let! x = ... (linear: use exactly once, compiler enforces it). This two-mode system gives fine-grained control over resource lifetimes without a garbage collector.
• Region-linear fusion -- Combines region-based memory management with linear types. Resources are allocated in regions and consumed linearly, giving deterministic cleanup with zero runtime overhead.
• WASM-first compilation -- Targets WebAssembly as its primary backend, with a Rust compiler frontend (15 crates) and __ffi() intrinsic for foreign function calls.

Architecture

The compiler is written in Rust (15 crates). Formal proofs of progress and preservation are in Coq. The Idris2 ABI layer defines interface correctness, and the Zig FFI layer provides C-ABI compatible exports.

See docs/ for architecture details.

Related Projects

• Gossamer -- Desktop app shell that uses Ephapax for its backend
• typed-wasm -- 10-level type safety for WASM memory
• nextgen-languages -- Parent repository tracking 14+ experimental languages including Ephapax
• proven -- Formal verification library

Contributing

See CONTRIBUTING.md.

License

PMPL-1.0-or-later