mpl/DECISIONS.md
2026-07-10 00:09:03 -04:00

40 lines
8.9 KiB
Markdown
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

# Design decisions
One line per decision, with the rejected alternatives named. Governing
principles, in order: One Right Answer, the Fatima test, minimal churn
against the existing examples.
- **Conditionals are guarded alternatives** `(condition ⟹ result) | fallback`, wired in as a `condExpr` precedence level; rejected: C-style ternary `cond ? a : b` (programmer convention, fails the Fatima test), standalone left-recursive `conditional` rule (ANTLR error 119).
- **Exception handling is a postfix operator** `expr ↴ { … }`; rejected: standalone `exceptionHandler` rule reachable from `atomExpr` (mutual left recursion, ANTLR error 119).
- **λ has one token, `LAMBDA_VAR`**, used both as a variable and to open a lambda; rejected: separate `LAMBDA` token (identical alternatives, fully shadowed, ANTLR warning 184).
- **`\implies` maps to ⟹ and `\Rightarrow` maps to ⇒** — one escape, one glyph; rejected: `\Rightarrow` as an alias of ⟹ (shadowed EXPORT's escape, ANTLR warning 184).
- **The Java package for generated code comes from `-package` in build.gradle only**; rejected: `@header` package declaration in the grammar (combined with `-package` it generates a duplicate `package` statement that does not compile).
- **ANTLR warnings fail the build** (`-Werror` in build.gradle); rejected: warnings as advisory output (they hid the shadowed-token bugs).
- **The choice-type rule is `⟨ expr ⟩`** with the interior `|` consumed by `condExpr`; rejected: explicit `⟨ expr | expr ⟩` (the interior expr already consumes the bar, making the explicit BAR unreachable).
- **Function calls are `f(a, b)` — a postfix argument list, nullary `f()` included**; rejected: Haskell juxtaposition `f x` (programmer convention, fails the Fatima test — children learn `f(x)` in school).
- **SEMICOLON has one role: sequence separator (trailing `;` permitted)**; the program, blocks, `(...)`, `⌈...⌉`, `...`, `⌜...⌝`, `⌞...⌟` and `⟳(...)` all contain one `seqExpr`; rejected: a separate statement-terminator rule duplicating the same token (two roles for one symbol).
- **Braces disambiguate structurally**: `IDENTIFIER :` → record, two-plus comma-separated exprs → set, everything else (incl. `{}` and `{x}`) → block; a singleton set literal cannot be written (deferred to M1); rejected: parser-order coin flips left undocumented.
- **`≜` defines, `←` assigns; both wired into the chain** with `≜` binding looser than `←`, both right-associative; rejected: `≜` tokenized but unreachable.
- **`⊕`/`⊖` are postfix resource operators** (`database ⊕`, `conn ⊖`), matching every example; rejected: prefix form `⊕open(path)` that appeared only in the whitepaper.
- **Channel operations are subscripted prefix operators** `⇀_ch expr` / `↽_ch expr`; rejected: leaving SEND/RECEIVE orphaned.
- **`‧` is qualified module access** (`Mathematics‧sin(angle)`), a postfix `‧IDENTIFIER`; rejected: leaving MIDDOT orphaned, or `.` (removed — one access syntax).
- **Handler clauses are `↯pattern ⟹ expr`, semicolon-separated**, where pattern is an identifier (binds the exception) or a string (matches a message); rejected: `↯e ⇒ expr` (⇒ is EXPORT; the clause arrow should mirror the guarded-alternative arrow ⟹).
- **IDENTIFIER may not start with `_`**, so subscripts (`⌉_db_lock`, `↽_socket`) lex as UNDERSCORE + IDENTIFIER; rejected: identifiers with a leading underscore (made every subscript lex as one identifier token).
- **`/` is an ASCII alias of ÷ (DIV)** so `π/4` parses; rejected: ÷-only division (unreachable on most keyboards).
- **Unary minus exists** (`-x`), sharing the MINUS token at prefix level; rejected: binary-only minus (cannot write negative numbers); unary plus was NOT added (`x ++ y` stays invalid).
- **`pathLiteral` accepts `🖫"…"` and `🖫identifier`**, as required by `readFile(🖫path)` in example 03.
- **Deleted tokens: `?` (QUERY), `∃` (EXISTS), `⇐` (IMPORT), `→` (ARROW), `.` (DOT)** — defined but used by no parser rule and no example; dead operators are debt; each returns in M1 only with a documented semantic. Rejected: keeping them tokenized-but-unreachable.
- **Exactly one ASCII escape per glyph** (`\lambda` not `\lam`, `\leftarrow` not `\gets`, `\neq` not `\ne`, `\nat` not `\N`, …); rejected: alias sets (two ways to write the same token).
- **`%` (modulo), `∑`, `√`, `²`, `|x|`, ranges `[a..b]`, indexing/slicing, `where`, and record field access are NOT in M0** — every document says so instead of using them; deferred to M1 with semantics, not smuggled in via prose.
- **Lambda parameters are a bare comma-separated pattern list** (`λa, b: body`); rejected: parenthesized parameter lists `λ(a, b):` (two ways to write parameters).
- **`‧` gets the escape `\middot`** so the "every glyph has an ASCII escape" claim stays true; rejected: leaving MIDDOT as the one escape-less glyph.
- **`glyph-escapes.md` and `precedence.csv` are the only symbol/precedence tables**; the whitepaper appendix points at them instead of duplicating them; rejected: parallel tables that drift (the old appendix disagreed with the lexer on several code points and escapes).
- **Documentation code blocks are fenced ```mpl only if they parse today**; M1+ sketches are fenced as plain text with an explicit "not yet parseable" caption, and a CI test enforces the rule for README, spec, and whitepaper.
- **Interpreter repatriation: `js/mpl.js` lives in this repo** as the single source of truth; mpl.codes consumes it by pinned commit SHA + sha256 checksum; rejected: making the site repo public as-is (splits truth across two repos), git submodule (invisible drift, clone friction).
- **Byte identity: repo file == image file == served file**, enforced by checksum at image build time and a post-deploy check; rejected: minified serving (a second artifact that can drift).
- **Interpreter tests run on `node:test` + `node:assert` with zero npm dependencies**; rejected: third-party test frameworks (a supply chain the site's own footer brags about not having).
- **Stage-1 exception: the imported interpreter's header comment was corrected in place** (`tested: 18/18` → the provable `10 tests in js/test/`) — a falsified claim inside the canonical artifact outranks byte identity with the pre-Stage-1 deploy; end-state identity is restored when the site deploys the pinned file.
- **Stage-3 ratification (2026-07-09): the 26 judgment calls are ruled; JUDGMENT_CALLS.md is the semantic record of MPL M0.** Per-ruling record: (1) ÷0 is `err_div0`; (2) a `∀` expression is always `⊥`; (3) an unmatched guard yields `⊥` unless caught by `|`; (4) numbers are exact rationals — BigInt num/den, lowest terms, den > 0, decimal literals exact, display `n` or `n/d` (re-evaluates to itself); IEEE doubles rejected; (5) `✎` rendering spec'd per type; (6) `⊥` is first-class, arithmetic on it `err_num`; (7) equality is structural on data, cross-type `=` false, `0.5 = 1/2` true, any function in `=`/`≠` raises `err_fn_eq`; (8) ordering is number×number and string×string (code-point) only, else `err_compare`; (9) closures capture the environment; (10) λ-application depth counter, limit 10000, `err_depth` — no keyless host error may remain reachable; (11) the 500000-step budget is an environment resource limit, not semantics — corpus entry 053 moved to js/test; (12) string escapes are exactly `\n \t \" \\`, anything else `err_escape` (grammar ESC amended to match); (13) guard conditions must be boolean, else `err_bool`; (14) `∧ ` short-circuit and demand booleans on evaluated operands (`err_bool`); (15) braces group, binders scope; (16) `≜` binds once per scope (`err_redef`; inner shadowing legal), `←` mutates an existing binding only (`err_unbound`); (17) type constraints parse, unenforced; (18) nullary `λ: e` admitted (grammar amended); (19) ```×`; (20) the empty program is valid; (21) `( seqExpr )` — the interpreter now implements it; (22) `∘` is composition, `(f ∘ g)(x…) = f(g(x…))`, non-function operand `err_notfn`; (23) set literals parse, evaluate to `err_notyet`; (24) record literals likewise; (25) `λ(a, b):` rejected everywhere; (26) `λ` is reserved — never an identifier — while other Greek letters remain identifiers.
- **Standing M1 decisions logged at ratification**: `√` vs (irrationals); an explicit local-binding construct (let/where); set semantics; record semantics; comprehension notation; `‖` parallel semantics.
- **Grammar-only surface gaps are on the record** (SURFACE.md "Grammar-only surface" section): `≈`/`` comparisons, `"""raw strings"""`, hex/binary/exponent literals, and `_` as a λ pattern all parse in the grammar and fail in the Stage-3 interpreter — Stage 4+ material, no ruling; `err_comment` is dead pending removal at the next legitimate interpreter change.
- **Ruling 12's enumeration governs string escapes**: the grammar's ESC fragment was narrowed to exactly `\n \t \" \\``\r`, `\0` and `\u{hex}` were removed from the grammar; they were never in the ratified set.