|
| 1 | +<!-- SPDX-License-Identifier: MPL-2.0 --> |
| 2 | +<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> --> |
| 3 | + |
| 4 | +# Ephapax vs AffineScript — these are different languages |
| 5 | + |
| 6 | +> ⚠️ **STOP.** If you arrived here because you were about to apply a lesson, snippet, fact, or tactic learned in one of these two repos to the other — **don't**. They share zero source-level structure. The only thing in common is the compile target. |
| 7 | +
|
| 8 | +## The one-sentence rule |
| 9 | + |
| 10 | +**Ephapax** and **AffineScript** are two unrelated languages from the same author. They both happen to use type systems with *affine-flavored* substructural properties — which is true of nearly every modern resource-safe language — and the lexical overlap of the word "affine" is the entire reason agents and humans confuse them. |
| 11 | + |
| 12 | +| | Ephapax | AffineScript | |
| 13 | +|---|---|---| |
| 14 | +| **What it is** | Research language for compile-time WebAssembly memory safety | Successor to JS / TypeScript / ReScript | |
| 15 | +| **Repo** | `hyperpolymath/ephapax` | `hyperpolymath/affinescript` | |
| 16 | +| **Audience** | Formal-methods researchers, systems verifiers | Application developers, JS-ecosystem users | |
| 17 | +| **Surface syntax** | `.eph` (Coq-like / ML-shaped) | `.affine`, plus brand-faces: jaffascript / rattlescript / lucidscript / cafescripto / pseudoscript | |
| 18 | +| **AST/IR** | `src/ephapax-syntax/src/lib.rs`, `src/ephapax-ir` | `lib/ast.ml`, `lib/borrow.ml` | |
| 19 | +| **Type checker** | `ephapax-linear/src/{linear,affine}.rs` (Rust, dyadic — see below) | `lib/borrow.ml` (OCaml, single discipline with capabilities) | |
| 20 | +| **Structural rule** | Linear (strict) + Affine (companion) — same AST, two checkers | Affine with explicit borrow/copy/drop, NLL-style scopes | |
| 21 | +| **Binding forms** | `let-linear`, `region r in …`, regions/exits | `let`, `borrow`/`copy`/`drop`, no first-class regions | |
| 22 | +| **Effects** | Region-typed; tracked in type system | Capabilities (`io`, `dom`, `pixi`, `tea`, …); host-facing | |
| 23 | +| **Compiler stack** | Cargo workspace; Rust + Idris2 + Coq | Dune project; OCaml + ReScript runtime | |
| 24 | +| **Codegen** | typed-wasm via `src/ephapax-wasm`, formal correctness lemma WIP | typed-wasm via `lib/tw_*.ml`, plus Deno-ESM and Node-CJS direct emit | |
| 25 | +| **Faces / frontends** | None — one surface syntax | Many (jaffascript, rattlescript, lucidscript, cafescripto, pseudoscript) — all desugar to the same core | |
| 26 | +| **Formal semantics** | Mechanized in Coq (`formal/Semantics.v`, `formal/Linearity.v`) + Idris2 ABI (`src/abi/Ephapax/…`) | Operational; soundness arguments in `lib/borrow.ml` comments + `docs/CAPABILITY-MATRIX.adoc`; tracking via `docs/TECH-DEBT.adoc` and issue #177 (CORE-01) | |
| 27 | +| **Proof obligations** | `formal/PRESERVATION-HANDOFF.md`, `ROADMAP.adoc` § "Preservation closure plan", PR ephapax#146 | None mechanized; `verification/proofs/` dirs are RSR template scaffolding only | |
| 28 | +| **Standard library** | `ephapax-linear/src/`, `examples/` | `stdlib/`, `vendor/`, bindings (`affinescript-dom`, `affinescript-pixijs`, `affinescript-tea`) | |
| 29 | +| **Editor support** | `editors/`, `idris2/` LSP work | `vscode-ext/`, NPM-published `@hyperpolymath/affine-vscode` | |
| 30 | +| **Status** | Research-active; preservation theorem in flight | Application-active; multiple PRs/release cycle | |
| 31 | + |
| 32 | +## What is shared |
| 33 | + |
| 34 | +**Two things, both via `hyperpolymath/typed-wasm`:** |
| 35 | + |
| 36 | +1. Both languages compile (or are moving towards compiling) to typed-wasm. |
| 37 | +2. Both languages interface with the same Rust verifier crate `crates/typed-wasm-verify/` inside the typed-wasm repo. |
| 38 | + |
| 39 | +That is the entire shared surface. They are **sibling languages standing on a common verification substrate** — not an implementation ↔ proof pair, not a parent ↔ dialect pair, not a frontend ↔ backend pair. |
| 40 | + |
| 41 | +## The dyadic-ephapax internal naming trap |
| 42 | + |
| 43 | +Ephapax is *itself* dyadic. Inside the ephapax repo there are two sublanguages: |
| 44 | + |
| 45 | +- **ephapax-linear** — the strict, formally-verified core. |
| 46 | +- **ephapax-affine** — a more versatile prototyping companion that works **with** ephapax-linear. |
| 47 | + |
| 48 | +Both are *ephapax-internal*. They share one AST, one Rust crate (`ephapax-linear/`), one grammar directory (`ephapax-linear/grammar/{linear,affine}.ebnf`). The "affine" in "ephapax-affine" names the *structural discipline* — one of two type-checking modes in one crate. |
| 49 | + |
| 50 | +**ephapax-affine is NOT AffineScript.** The word `affine` overlapping in both names is a coincidence of substructural-logic terminology, not a relationship. AffineScript is a separate language with its own AST, its own borrow checker, its own faces. |
| 51 | + |
| 52 | +## Why the confusion happens |
| 53 | + |
| 54 | +Three traps stacked on each other: |
| 55 | + |
| 56 | +1. **Lexical**: both names contain `affine`. |
| 57 | +2. **Conceptual**: both use type systems with affine-logic properties, because nearly every resource-safe language does (Rust, Linear Haskell, F*, Idris with QTT, Granule, …). The mere presence of "affine" in a description is not a fingerprint. |
| 58 | +3. **Single-author**: both projects come from the same author, so cross-references and shared idioms appear in commit messages, docs, and chat. Don't read those as evidence of structural relationship. |
| 59 | + |
| 60 | +## How to tell which you're in |
| 61 | + |
| 62 | +Quick visual signals, in priority order: |
| 63 | + |
| 64 | +| Signal | Ephapax | AffineScript | |
| 65 | +|---|---|---| |
| 66 | +| Repo URL | `github.com/hyperpolymath/ephapax` | `github.com/hyperpolymath/affinescript` | |
| 67 | +| Build tool | `Cargo.toml` at root | `dune-project` at root | |
| 68 | +| Main language | Rust (+ Coq + Idris2) | OCaml (+ ReScript runtime) | |
| 69 | +| File extension under work | `.eph`, `.v`, `.idr` | `.affine`, `.ml`, `.res` | |
| 70 | +| Top-level dirs | `formal/`, `idris2/`, `ephapax-linear/`, `src/` | `lib/`, `vendor/`, `stdlib/`, face-directories | |
| 71 | +| Headline file | `formal/Semantics.v`, `ROADMAP.adoc` | `lib/borrow.ml`, `docs/CAPABILITY-MATRIX.adoc` | |
| 72 | +| Open soundness ticket | preservation 11 admits (Brief C / PR ephapax#146) | issue affinescript#177 (CORE-01) | |
| 73 | + |
| 74 | +If you can't tell from the repo URL alone, you are in the wrong context for the work. |
| 75 | + |
| 76 | +## Specific guidance for AI agents |
| 77 | + |
| 78 | +**Do:** |
| 79 | +- When switching context between the two, state it explicitly: "switching context from AffineScript to ephapax" (or vice versa). This forces the user-visible audit trail. |
| 80 | +- Treat memory entries written about one as inadmissible for the other unless the cross-reference is explicit and recent. |
| 81 | +- When you read a snippet mentioning "affine", look at *which file path* it lives in before assuming you know which language is meant. |
| 82 | +- Cross-reference the canonical disambiguation memory entry: `feedback_affinescript_ephapax_siblings_not_impl_proof.md`. |
| 83 | + |
| 84 | +**Don't:** |
| 85 | +- Apply borrow-checker tactics from `lib/borrow.ml` (OCaml, AffineScript) to `formal/Semantics.v` (Coq, ephapax) or vice versa. |
| 86 | +- Re-use proof-obligation framings across the two. Ephapax has Coq/Idris2 mechanized proofs; AffineScript has compiler-correctness arguments. |
| 87 | +- Conflate `ephapax-affine` (the sublanguage *inside* ephapax) with `AffineScript`. They have nothing in common beyond the syllable. |
| 88 | +- Assume that a typed-wasm-side change in one repo implies anything about the other. The verifier crate is shared, but the consumers are independent. |
| 89 | + |
| 90 | +## Cross-pointers |
| 91 | + |
| 92 | +- **Ephapax**: `hyperpolymath/ephapax` — README.adoc, ROADMAP.adoc, formal/PRESERVATION-HANDOFF.md. |
| 93 | +- **AffineScript**: `hyperpolymath/affinescript` — README.adoc, docs/ECOSYSTEM.adoc, docs/CAPABILITY-MATRIX.adoc. |
| 94 | +- **Shared target**: `hyperpolymath/typed-wasm` — README.adoc. Documents both languages as independent producers. |
| 95 | +- **Canonical disambiguation memory entry**: `feedback_affinescript_ephapax_siblings_not_impl_proof.md` (in the user's auto-memory; durable across sessions). |
| 96 | + |
| 97 | +## When this doc is wrong |
| 98 | + |
| 99 | +The canonical statement is the source code. If this doc and the source disagree, update this doc. Keep the disambiguation specific and current: |
| 100 | + |
| 101 | +- If ephapax adds a third sublanguage, update the dyadic-naming-trap section. |
| 102 | +- If AffineScript adds a face, update the faces row in the comparison table. |
| 103 | +- If the two ever share more than typed-wasm + the Rust verifier, update the "What is shared" section before anything else. |
| 104 | +- If a new confusion class emerges (e.g., a third language with `affine` in the name), extend this doc rather than fork. |
| 105 | + |
| 106 | +Last revised: 2026-05-26. |
0 commit comments