diff --git a/docs/specs/FACE-CONTRACT.adoc b/docs/specs/FACE-CONTRACT.adoc new file mode 100644 index 0000000..1d0c59b --- /dev/null +++ b/docs/specs/FACE-CONTRACT.adoc @@ -0,0 +1,226 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) += AffineScript Face Contract — the normative binding between faces and the canonical +Jonathan D.A. Jewell +:toc: macro +:toclevels: 2 + +Status: DRAFT (2026-07-08) — Milestone A keystone of the face-sealing plan. + +This document is the *single normative source* for how a language _face_ binds to +the canonical AffineScript compiler. Where `docs/specs/faces.adoc` describes the +_design_ of the face architecture (ADR-010), this document fixes the _contract_: +the roster, the file/pragma model, the CLI names, the shim protocol, the canonical +pin, and the conformance + proof obligations every face must meet. Brand-surface +repos link here rather than restating any of it. + +toc::[] + +== The face roster (normative) + +A _face_ earns a place on this roster only if it serves a *distinct, living surface +community* whose idioms map meaningfully onto AffineScript's affine/linear + +effect + typed-wasm semantics. Near-duplicate surfaces and dead-runtime dialects +do not qualify as standalone faces (see <>). + +[cols="1,2,1,1", options="header"] +|=== +| Brand | Source language | `--face` | Status + +| (canonical) | AffineScript itself | `canonical` | Stable (default) +| RattleScript | Python | `rattle` | Shipped +| JaffaScript | JavaScript | `jaffa` | Shipped +| ProperScript | TypeScript (+ AS3 preset) | `proper` | *New — planned* +| RealScript | ReScript | `real` | *New — planned* +| CafeScripto | CoffeeScript | `cafe` | Shipped +| LucidScript | PureScript / Haskell | `lucid` | Shipped +| PseudoScript | pseudocode | `pseudo` | Shipped +|=== + +=== The naming decoder ring + +Each brand name is a lateral pun on its source language — either a *synonym* +(`cafe`≈coffee, `lucid`≈pure) or an *associative leap* (`rattle`→snake→Python, +`jaffa`→Java). The two new ECMAScript-descended faces form a coherent trio with +JaffaScript: + +* *JaffaScript* — raw JavaScript, untyped. +* *ProperScript* — TypeScript, now typed _properly_. TypeScript's types are + structural and erased; routed through the affine core + typed-wasm they become + sound. "The TypeScript that is finally typed properly." +* *RealScript* — ReScript, whose ML-family types were _real_ (sound, + non-nullable, no `any`) all along. The name is a homophone tribute + (Re→Real), not a corrective. + +ProperScript and RealScript are the "typed twins" of the JaffaScript family. + +== Binding model: one extension, a pragma per face + +*Ratified (supersedes the `.pyaff/.jsaff/...` prose in older docs).* Every face +shares the canonical `.affine` file extension. The active face is selected, in +priority order: + +. an explicit `--face ` flag (always wins), then +. a first-line `face:` pragma in the source, then +. canonical (default). + +The legacy per-face extensions (`.pyaff`, `.jsaff`, `.pseudoaff`, …) and the +`--face pyaff|jsaff|pseudoaff` spellings are *deprecated* (the compiler already +emits a deprecation warning for them, `bin/main.ml`). New material MUST use +`.affine` + pragma. + +.Pragma grammar +The pragma is the file's first meaningful line, written in that face's own comment +syntax, of the form ` face: `: + +[source] +---- +# face: rattlescript (Python-style comment) +// face: jaffascript (JS-style comment) +// face: properscript +// face: realscript +-- face: pseudoscript (or lucidscript) +# face: cafescripto +---- + +== Face identity table (normative) + +[cols="1,1,1,2,1", options="header"] +|=== +| Brand | `--face` short | pragma long | transformer + `Face` variant | brand repo + +| RattleScript | `rattle`, `python` | `rattlescript` | `lib/python_face.ml` · `Face.Python` | `hyperpolymath/rattlescript` +| JaffaScript | `jaffa`, `js`, `javascript` | `jaffascript` | `lib/js_face.ml` · `Face.Js` | `hyperpolymath/jaffascript` +| ProperScript | `proper`, `typescript` | `properscript` | `lib/proper_face.ml`* · `Face.Proper`* | `hyperpolymath/properscript`* +| RealScript | `real`, `rescript` | `realscript` | `lib/real_face.ml`* · `Face.Real`* | `hyperpolymath/realscript`* +| CafeScripto | `cafe`, `coffee` | `cafescripto` | `lib/cafe_face.ml` · `Face.Cafe` | `hyperpolymath/cafescripto` +| LucidScript | `lucid` | `lucidscript` | `lib/lucid_face.ml` · `Face.Lucid` | `hyperpolymath/lucidscript` +| PseudoScript | `pseudo`, `pseudocode` | `pseudoscript` | `lib/pseudocode_face.ml` · `Face.Pseudocode` | `hyperpolymath/pseudoscript` +|=== + +`*` = does not exist yet; created under Part 2 of the plan. The CLI already +accepts the brand short aliases `rattle`/`jaffa` alongside the canonical +`python`/`js` names; it MUST be extended to accept `proper`/`real` (and +`typescript`/`rescript`) once those `Face` variants land. Note: `bin/main.ml` +already carries partial `is_rescript` error-vocabulary plumbing that RealScript +will absorb. + +== Shim protocol (hardened) + +Each brand repo ships a `bin/` shim carrying *no compiler* — it locates the +canonical `affinescript` binary and injects `--face `. The shim MUST resolve +the binary in this order and fail with an actionable message if none is found: + +. `--affinescript ` / `$AFFINESCRIPT`, else +. `affinescript` on `$PATH`, else +. the sibling canonical checkout + (`../γ-affinescript/affinescript/_build/default/bin/main.exe`), else +. print: `affinescript not found — install via opam, or set $AFFINESCRIPT`. + +This replaces the current bare-`affinescript` shims, which fail with a raw +`command not found`. + +== Canonical pin + +Every brand repo pins the canonical compiler as a *git submodule* (the mechanism +RattleScript already uses) and bumps it via `just update-affinescript`. No brand +repo floats against "whatever is on `$PATH`". All language, face, and bug-fix +changes flow through a single submodule-pointer bump, so a face can never silently +drift from the compiler it targets. + +[[actionscript]] +== ActionScript: welcomed in, but not a standalone face + +*Decision (2026-07-08): ActionScript is NOT a standalone face.* It is folded into +ProperScript as a migration preset. This retires the "ActionScript-face (strategic +priority)" roadmap item in `docs/specs/faces.adoc §194`. + +*Why not a face.* A face must serve a distinct, living surface community. AS3 fails +both halves: its surface is an ECMAScript-4 dialect (`var x:Type`, +`function f():R`, classes, packages) that is essentially *JaffaScript + +ProperScript already*, and its runtime (Flash) died in 2020, so there is no +community writing new AS3 to rehome. Its `-Script` is native (like TypeScript / +JavaScript), the tell that it is a product name, not a face-brand. + +*But the door is open.* Flash / Flex / AIR developers were displaced by platform +death, not language quality, and they are genuinely welcome. Their on-ramp is +*ProperScript plus an AS3-idioms migration preset* — `extends` → traits, +`package { … }` stripped, `trace(x)` → `IO.println(x)`, `Number`/`int` → `Float`/ +`Int`, `Array.`/`Vector.` → `Array[T]`, `null` → `()`. The mapping already +drafted in `faces.adoc §194` is retargeted from a hypothetical `action_face` onto +this preset. + +*Honest scope.* A dedicated `action_face` with its own brand repo is deferred +indefinitely. This is a one-person, unfunded project; the resource-responsible +choice is a preset that reuses the ProperScript machinery, not a whole face we +cannot maintain. It will be reassessed only if a funded AS3 cohort materialises. + +== Conformance obligations + +A face is _conformant_ only when all of the following are green: + +. *Snapshot* — `tools/run_face_transformer_tests.sh` (the face's + `tests/faces/hello-.expected.txt` matches its `preview-` output). +. *Round-trip parse* — the face's examples parse via the normal + pragma-auto-detecting pipeline. +. *Same-cube* — `hyperpolymath/invariant-path/scripts/verify-same-cube.sh` + places the face in the *single* canonical wasm equivalence class. ++ +[IMPORTANT] +This gate is *currently RED (exit 1)*: the six existing faces split into two +wasm classes — `{lucid, pseudo, rattle}` (tail-expression) vs +`{cafe, canonical, jaffa}` (statement) — because terminator-free faces guess a +unit-typed trailing call as a tail expression and drop the `;` +(canonical issue *#601*). Closing it (Milestone B) is a plan deliverable, via a +post-typecheck tail-normalisation pass, so the text transformer's guess no longer +reaches codegen. + +Same-cube MUST be promoted from an external script to a *required CI check* in the +canonical repo, and each brand repo MUST run a per-face conformance gate against +its pinned submodule. + +== Proof obligations + +The canonical core is being proved against the real `lib/ast.ml` / `lib/wasm.ml` +denotation (the "real lift"). The faces must ride that same rigour. Current status +(`docs/PROOF-NEEDS.adoc`): + +[cols="1,3,1", options="header"] +|=== +| Obligation | Statement | Status + +| F-1 | every `lib/_face.ml` transform preserves the typed-wasm denotation | *partial* (toy model only) +| F-2 | tail/statement normalisation preserves denotation | *partial* (unit-tail case, `SameCube.agda`) +| F-6 | preview round-trip totality (transform always yields parseable canonical) | *absent* +| F-7 | face/canon confluence (all faces of one program reach one canonical AST) | *absent* +|=== + +Sealing the connection "for real" (Milestone D) means moving F-1 to per-face +preservation against the real AST, generalising F-2 to the normalisation pass of +#601, and discharging F-6/F-7. Until then the real transformers are grounded by +tests only; this table is the honest statement of that gap. + +== Open implementation tasks (tracked by the plan) + +* *P1.2* — add `proper`/`real` (+ `typescript`/`rescript`) to the CLI `--face` + alias table and `Face` variant type. +* *P2 (js_face split)* — JaffaScript narrows to plain JavaScript; ProperScript + gets its own transformer + TS-idiom error vocabulary (interfaces→traits, `type`, + `as`, generics→type params, `| null` unions). `lib/js_face.ml`'s current + "JS/TS" double duty is split. +* *Create brand repos* `properscript` and `realscript` (brand-surface only, per + this contract). +* *Span fidelity* (ADR-010 §4) — error spans map back to original face source, + not transformed canonical text. +* *Path* — `lucidscript` + `cafescripto` currently live under `γ-languages/`; + ratify or relocate to match the flat `repos/` siblings. +* *AFFIRMATION* — absent from all brand repos; add if RSR-required. + +== Provenance + +* Roster + names ratified in session 2026-07-08 (RattleScript/JaffaScript/ + CafeScripto/LucidScript/PseudoScript pre-existing; ProperScript, RealScript, and + the ActionScript fold-in decided this session). +* Supersedes: `.pyaff`-style extensions; the ActionScript standalone-face roadmap + item (`faces.adoc §194`). +* Companion design doc: `docs/specs/faces.adoc` (ADR-010). diff --git a/docs/specs/faces.adoc b/docs/specs/faces.adoc index 9b85063..dc59d70 100644 --- a/docs/specs/faces.adoc +++ b/docs/specs/faces.adoc @@ -120,16 +120,19 @@ agree on trailing-statement lowering would yield byte-level same-cube. == Roadmap Faces -ActionScript-face remains on the roadmap (CoffeeScript has since shipped as -CafeScripto — see Active Faces above). The face architecture makes -implementation cheap once the surface mapping is settled; the bottleneck is -design, not code. +ActionScript is *no longer a roadmap face*. As of 2026-07-08 it has been folded +into ProperScript (the TypeScript face) as an AS3-idioms migration preset — see +`docs/specs/FACE-CONTRACT.adoc`, "ActionScript: welcomed in, but not a standalone +face". The surface mapping retained in the section below now describes that +preset, not a standalone `action_face`. No standalone faces remain on the +roadmap; the two new faces (ProperScript / TypeScript, RealScript / ReScript) are +tracked as active planned work in the Face Contract, not here. === CoffeeScript-face — SHIPPED as CafeScripto NOTE: This face is now *established* (`lib/cafe_face.ml`, `--face cafe`; see the Active Faces table and `hyperpolymath/cafescripto`). The design notes below are -retained as historical reference; only ActionScript-face remains on the roadmap. +retained as historical reference. No standalone faces remain on the roadmap. *Rationale:* CoffeeScript has a loyal displaced community that never loved JavaScript and were forced away when the ecosystem moved on. Their syntax @@ -191,9 +194,18 @@ WASM output. *File:* `lib/coffee_face.ml`, `--face coffee` / `--face coffeescript` -=== ActionScript-face (strategic priority) +=== ActionScript — ProperScript AS3 migration preset (not a standalone face) -*Rationale:* ActionScript 3 was a capable, statically-typed OO language +NOTE: *Decision 2026-07-08* (`docs/specs/FACE-CONTRACT.adoc`): ActionScript is not +a standalone face. AS3's surface is an ECMAScript-4 dialect essentially covered by +JaffaScript (JavaScript) + ProperScript (TypeScript), and its runtime (Flash) is +dead, so there is no living community to rehome into a dedicated face. Flash / +Flex / AIR developers are genuinely welcome — their on-ramp is ProperScript +(`--face proper`) plus the AS3-idioms preset described by the mapping below. A +dedicated `action_face` is deferred indefinitely as a resource-responsible choice +for a solo, unfunded project. + +*Rationale (historical):* ActionScript 3 was a capable, statically-typed OO language with a loyal community (Flash game developers, Flex/AIR developers). It was killed by platform death (Flash end-of-life), not by language quality. AS3 developers are comfortable with explicit types, classes, and access @@ -253,7 +265,8 @@ modifiers — all of which map naturally to AffineScript concepts. - Event model (`addEventListener`) — emit a hint pointing to effects. - `Vector.` vs `Array.` — both map to `Array[T]`? -*File:* `lib/action_face.ml`, `--face action` / `--face actionscript` +*Realised as:* an AS3-idioms preset / migration guide under ProperScript +(`--face proper`), not a standalone `lib/action_face.ml`. == Python Face Details