Ephapax

ἐφάπαξ — once for all

image:[Rust 1.83+] image:[Coq 8.18+]

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

Surface Syntax (Locked)

Ephapax uses a compact, statement-delimited block syntax. Newlines act as statement separators (equivalent to ;).

// Function declaration
fn main() -> i32 {
    let x = 1 + 2;
    let y = x * 3;
    y
}

// Linear let-binding
let! z = copy(x) in z

Grammar highlights:

• Functions: fn name(params) → Ty { …​ } or fn name(params) : Ty { …​ }

• Let bindings: let x = expr in expr

• Linear let bindings: let! x = expr in expr

• Block expressions: { expr1; expr2; …​; exprN } (final expr is the result)

• Comments: // to end-of-line

Quickstart

just idris-build
just smoke

This compiles examples/hello.eph end-to-end and produces a WASM artifact.

Current Limitations

• The WASM backend currently assumes i32 representation for pairs/sums.

• Lambda/app compilation is stubbed (closure conversion not yet implemented).

Seam Analysis

Key interfaces where correctness and stability matter:

• Idris2 → S-expression IR (Ephapax.IR.Decode encoding/decoding).

• Zig FFI token buffer → Idris2 parser stream (Ephapax.Parse.ZigBuffer).

• S-expression IR → Rust/WASM backend (ephapax-ir and ephapax-wasm).

We now include the proven library as a dependency to harden string handling paths over time (e.g., JSON-style escaping for IR boundaries).

Overview

Ephapax is a programming language with a linear type system that guarantees:

Guarantee	Mechanism
No use-after-free	Linear resources cannot be accessed after consumption
No memory leaks	Linear resources must be consumed exactly once
Region-based deallocation	Bulk memory management without garbage collection
Zero-cost abstractions	Safety guarantees enforced at compile time

Design Principles

Principle	Mechanism
Linearity	Every linear value used exactly once
Regions	Scoped allocation with bulk deallocation
Second-class borrows	Temporary access without ownership transfer
Explicit copies	Duplication requires explicit syntax

Example

region r:
    let s1 = String.new@r("hello, ")
    let s2 = String.new@r("world")

    -- Borrow s1 to get length (does not consume)
    let len = String.len(&s1)

    -- Concatenation consumes both strings
    let result = String.concat(s1, s2)

    -- result is consumed by returning
    result
-- Region exits: any remaining allocations freed

Project Structure

ephapax/
├── formal/              # Coq formalisation of type system
│   ├── Syntax.v         # AST and types
│   ├── Typing.v         # Linear typing rules
│   └── Semantics.v      # Operational semantics & soundness
├── src/                 # Implementation
│   ├── ephapax-syntax/  # AST definitions
│   ├── ephapax-typing/  # Linear type checker
│   ├── ephapax-lexer/   # Tokenizer (logos)
│   ├── ephapax-parser/  # Parser (chumsky)
│   ├── ephapax-interp/  # Tree-walking interpreter
│   ├── ephapax-wasm/    # WASM code generation
│   ├── ephapax-runtime/ # Runtime support
│   ├── ephapax-repl/    # Interactive shell
│   └── ephapax-cli/     # Command-line interface
├── conformance/         # Type system conformance tests
│   ├── pass/            # Programs that should type-check
│   └── fail/            # Programs that should be rejected
├── spec/                # Language specification
├── .machine_read/       # Machine-readable specs for tooling
└── docs/                # Documentation

Build Targets

Target	Description	Status
WebAssembly	wasm32-unknown-unknown	Primary
Native	Via Cranelift	Secondary

Formal Foundations

The type system is grounded in:

• Intuitionistic linear logic — Resource-sensitive reasoning

• Separation logic — Memory ownership and framing

• Region calculus (Tofte-Talpin) — Scoped allocation

See formal/ for Coq mechanisation.

Quick Start

Prerequisites

• Rust 1.83+ with wasm32-unknown-unknown target

• Coq 8.18+ (optional, for proof verification)

• just (task runner)

Build

# Build all crates
just build

# Build for WASM
just build-wasm

# Build Idris2 affine stage
just idris-build

# Verify Coq proofs (optional, requires Coq 8.18+)
just proofs

Test

# Run all tests
just test

# Run conformance test suite
just conformance

# Run golden path (test + build + proofs)
just golden

Documentation

• Language Specification

• Wiki Documentation

• Coq Documentation (generated)

Two-Phase Compiler (Idris2 → WASM)

Ephapax includes an experimental two-stage pipeline:

• Stage 1 (Idris2): parse concrete Ephapax syntax (or S-expression IR) and type-check in affine or linear mode.

• Stage 2 (Rust): compile the checked IR to WebAssembly.

Run:

# Compile a module through Idris2 + WASM backend (concrete syntax)
just compile-affine input.eph affine output.wasm

# Compile an S-expression module through Idris2 + WASM backend
scripts/compile-affine.sh input.sexpr --mode affine --out output.wasm --sexpr

# Or call the CLI directly for Stage 2
cargo run -p ephapax-cli -- compile-sexpr input.sexpr -o output.wasm

Parser Tests & Bench

# Run Idris2 parser tests
just idris-parse-test

# Benchmark Idris2 parser (parse-only)
just idris-parse-bench input.eph 10

# Build Zig token buffer (FFI)
scripts/build-zig-ffi.sh

Status

🚧 Early Development

Component	Status
Core type system design	✅ Complete
Formal semantics (Coq)	✅ Complete
Lexer	✅ Complete
Parser	✅ Complete
Type checker	🚧 In Progress
WASM code generation	🚧 In Progress
Interpreter	✅ Complete
REPL	✅ Complete
CLI	✅ Complete
Standard library	🔲 Planned

Related Work

• Rust — Ownership and borrowing

• Linear Haskell — Linear types in GHC

• MLKit — Region-based memory management

• Cyclone — Safe C dialect with regions

Contributing

Contributions are welcome! Please see:

• Contributing Guide

• Code of Conduct

Licence

EUPL-1.2 — See LICENSE.txt

Author

Jonathan D.A. Jewell

---

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