diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.machine_readable/6a2/AGENTIC.a2ml index cd1fb1d..08d22b2 100644 --- a/.machine_readable/6a2/AGENTIC.a2ml +++ b/.machine_readable/6a2/AGENTIC.a2ml @@ -20,6 +20,11 @@ can-create-files = true # - Never use banned languages (TypeScript, Python, Go, etc.) # - Never place state files in repository root (must be in .machine_readable/) # - Never use AGPL license (use MPL-2.0) +# - Never break VISIBLE DECOMPOSITION for Echo types: +# * do not make echo_to_residue a silent cast +# * do not let EchoR behave like / coerce to Echo +# * do not hide the erasure stability debit ([Stab-Erase]) +# (see docs/Echo-Decomposition.adoc, spec/type-system.md §7) [maintenance-integrity] fail-closed = true diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/6a2/ECOSYSTEM.a2ml index 78c4e0f..5eedf67 100644 --- a/.machine_readable/6a2/ECOSYSTEM.a2ml +++ b/.machine_readable/6a2/ECOSYSTEM.a2ml @@ -8,13 +8,17 @@ last-updated = "2026-04-11" [project] name = "Error Lang" -purpose = "" -role = "" +purpose = "A dissembling/decompositional educational language that makes the decay and structured loss of programs, semantics, and types VISIBLE." +role = "Operational, stability-aware embedding of the Echo (structured-loss) lineage; the decomposition-visible member of the Echo family." [position-in-ecosystem] -category = "" +category = "educational-programming-language" [related-projects] projects = [ - # No related projects recorded + # The Echo (structured-loss) lineage that Error-Lang's Echo/EchoR embed. + # Error-Lang stays Error-Lang-specific (visible decomposition); it does not + # re-export these repos' exposition. + { name = "echo-types", owner = "hyperpolymath", role = "source of mechanized truth (Agda): Echo f y := Σ(x:A), (f x ≡ y)" }, + { name = "EchoTypes.jl", owner = "hyperpolymath", role = "finite-domain executable model (Julia) — a model, not a proof" }, ] diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index cad0188..6d2ba25 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.machine_readable/6a2/META.a2ml @@ -12,7 +12,15 @@ author = "Jonathan D.A. Jewell (hyperpolymath)" [architecture-decisions] decisions = [ - # No ADRs recorded + # ADR-0001: Echo types model structured loss as first-class, VISIBLE decomposition. + # Echo = retained witness + visible output; EchoR = residue after + # irreversible erasure; echo_to_residue is an explicit decomposition step that + # debits stability ([Stab-Erase]). Invariant: decomposition must be visible — + # no silent cast, EchoR is not Echo-with-a-missing-field, debit not hidden. + # Runtime is single-witness (VEcho{input,output} / VResidue{output}); whole-fibre + # waits for first-class functions. Builtin names mirror EchoTypes.jl. + # Refs: docs/Echo-Decomposition.adoc, spec/type-system.md §7. + { id = "ADR-0001", title = "Echo types as visible structured-loss decomposition", status = "accepted" }, ] [development-practices] diff --git a/.machine_readable/6a2/NEUROSYM.a2ml b/.machine_readable/6a2/NEUROSYM.a2ml index e1d34c0..45377b8 100644 --- a/.machine_readable/6a2/NEUROSYM.a2ml +++ b/.machine_readable/6a2/NEUROSYM.a2ml @@ -14,6 +14,16 @@ report-format = "logtalk" [symbolic-rules] # Custom symbolic rules for this project # - { name = "no-unsafe-ffi", pattern = "believe_me|unsafeCoerce", severity = "critical" } +# +# Echo decomposition must remain VISIBLE (see docs/Echo-Decomposition.adoc): +# - echo_to_residue must debit stability — it is never a silent cast +# - EchoR must not unify with / be coerced to Echo +# - echo_input must be rejected on a residue (the witness is gone) +rules = [ + { name = "echo-erasure-must-cost", concern = "echo_to_residue must apply the [Stab-Erase] stability debit", severity = "high" }, + { name = "echo-residue-no-coercion", concern = "no implicit Echo->EchoR or Echo->B coercion; EchoR does not unify back into Echo", severity = "high" }, + { name = "echo-input-not-on-residue", concern = "echo_input is illegal on EchoR (non-recoverable residue)", severity = "high" }, +] [neural-config] # Neural pattern detection settings diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index fc0923a..b66d146 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -4,41 +4,79 @@ # STATE.a2ml — Error Lang project state [metadata] project = "error-lang" -version = "0.4.0" -last-updated = "2026-02-07" +version = "0.5.0" +last-updated = "2026-06-02" status = "active" -session = "converted from scheme — 2026-04-11" +session = "Echo types (structured loss) — 2026-06-02" [project-context] name = "Error Lang" -purpose = """Merge error-lang-playground into main repo""" +purpose = """ +Add Echo types (Echo / EchoR) as Error-Lang's first-class, visible +form of structured loss. Port the echo-types (Agda) / EchoTypes.jl (Julia) +lineage into the compiler pipeline, type checker, VM, and documentation. +Governing invariant: decomposition must be visible. +""" completion-percentage = 100 [position] phase = "production-ready" # design | implementation | testing | maintenance | archived -maturity = "experimental" # experimental | alpha | beta | production | lts +maturity = "experimental" # experimental | alpha | beta | production | lts -[route-to-mvp] -milestones = [ - # No milestones recorded +[what-was-done] +# Session 2026-06-02 — Echo types (structured loss) +additions = [ + "Echo and EchoR types added to: lexer (keywords), parser (type annotations), type checker (TyEcho/TyEchoR, unification, builtins), codegen (dedicated opcodes), VM (VEcho/VResidue, stability debit)", + "Five builtins mirroring EchoTypes.jl: echo, echo_to_residue, echo_input, echo_output, residue_strictly_loses", + "Stability debit: echoEraseCost = 15.0 charged by OpEchoToResidue, never on projection", + "Irreversibility: TyEcho never unifies with TyEchoR; echo_input is type+runtime error on EchoR", + "Tests: type-checker (10), parser (1 comprehensive), lexer (2), runtime (5) across three decomposition planes", + "New docs: docs/Echo-Decomposition.adoc (authoritative), spec/type-system.md §7, docs/Design-Philosophy.adoc section, docs/Error-Lang.adoc section, docs/Curriculum.adoc Lesson 11, docs/Educational-Framework.adoc, docs/Error-Categories.adoc echo-erasure row", + "New example: examples/11-echo-decomposition.err (narrated, with gutter zone)", + "Updated manifests: 0-AI-MANIFEST.a2ml (core narrative + invariants), META.a2ml (ADR-0001), NEUROSYM.a2ml (3 symbolic rules), ECOSYSTEM.a2ml (lineage), AGENTIC.a2ml (constraint)", + "README.adoc decompositional framing and Echo introduction", + "EXPLAINME.adoc created (human/agent orientation document)", + "contractiles/ updated: Mustfile (Error-Lang invariants), Dustfile (recovery handlers), trust/Trustfile.hs (verification), lust/Intentfile (roadmap)", + "CI hardening: casket-pages.yml, codeql.yml, hypatia-scan.yml get timeout-minutes (separate PR #18)", ] +[current-ci-status] +# As of 2026-06-02, PR #17 (Echo types) check status: +passing = [ + "Hypatia Neurosymbolic Analysis", + "CodeQL Analysis (javascript-typescript)", + "governance / Licence consistency", + "governance / Guix primary / Nix fallback policy", + "governance / Well-Known (RFC 9116 + RSR)", + "governance / Workflow security linter", + "governance / Trusted-base reduction policy", + "governance / Validate Hypatia baseline", + "governance / Code quality + docs", + "governance / Security policy checks", +] +failing = [ + "governance / Language / package anti-pattern policy", +] +failing-reason = """ +The anti-pattern policy bans ReScript (.res files) estate-wide. This failure +is PRE-EXISTING on main — it fails identically there. It is NOT caused by +Echo types or any recent work. Resolution: AffineScript re-target (INTENT-001, +ADR-pending). Do NOT attempt to fix by removing .res files. +""" + [blockers-and-issues] issues = [ - "Backend architecture decision: bytecode VM vs transpile to JS", + "governance / Language / package anti-pattern policy — permanent pre-existing failure (ReScript ban); resolves only with AffineScript re-target", ] [critical-next-actions] actions = [ - "Decide on backend strategy (bytecode vs transpile)", - "Complete Zig FFI bindings", - "Start LSP server skeleton", - "Design computational haptics visualization protocol", - "Complete backend/codegen", - "Complete LSP server", - "Create VS Code extension prototype", + "AffineScript re-target: migrate compiler/src/*.res to standard dialect (INTENT-001)", + "First-class functions in VM: enable whole-fibre Echo (INTENT-002)", + "LSP hover for Echo decomposition tracking (INTENT-005)", ] [maintenance-status] -last-run-utc = "2026-02-07T00:00:00Z" -last-result = "unknown" # unknown | pass | warn | fail +last-run-utc = "2026-06-02T00:00:00Z" +last-result = "pass" # unknown | pass | warn | fail +notes = "All checks pass except the pre-existing governance ReScript ban." diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 18b9e71..0fa4b03 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -1,7 +1,7 @@ # SPDX-License-Identifier: MPL-2.0 # 0-AI-MANIFEST.a2ml — error-lang # Universal AI Agent Gateway — Read This First -# Generated: 2026-03-14 +# Last updated: 2026-06-02 ## Identity @@ -9,59 +9,129 @@ project: error-lang type: programming-language owner: hyperpolymath description: > - Error-first programming language with graduated error levels and ReScript playground compiler. + A dissembling / decompositional educational programming language. Programs, + syntax, semantics, and types can decay, decompose, and destabilise over time, + and the language EXPOSES that decomposition (consequence amplification + + stability scoring) rather than hiding it. Echo types give structured loss a + first-class shape. Error-first with graduated error levels. license: MPL-2.0 +## Core Narrative (read before reasoning about features) + +Error-Lang is not merely "a language with errors." It is decompositional: +the distinctive claim is that decomposition is itself something the language +exposes and reasons about. Echo types make STRUCTURED LOSS first-class: + - Echo retained witness + visible output (a fibre witness) + - EchoR residue after irreversible erasure (witness gone) + - echo_to_residue explicit decomposition step; debits stability ([Stab-Erase]) +Governing invariant: DECOMPOSITION MUST BE VISIBLE — echo_to_residue is never a +silent cast, EchoR is never an Echo with a missing field, and the stability +debit is never hidden. See docs/Echo-Decomposition.adoc and spec/type-system.md §7. + ## Critical Invariants +- Decomposition must be visible: never make echo_to_residue a silent cast, + never let EchoR behave like Echo, never hide the erasure stability debit - SCM files ONLY in `.machine_readable/` (root copies are symlinks) -- NEVER delete spec files: grammar, SPEC.core.scm +- NEVER delete spec files: spec/grammar.ebnf, spec/SPEC.core.scm - NEVER use banned languages: TypeScript, Node.js, npm, Go, Python - All GitHub Actions must be SHA-pinned -- All source files must have SPDX headers +- All source files must have SPDX-License-Identifier: MPL-2.0 headers - Root symlinks MUST be maintained when moving files +- NEVER use the AGPL license (use MPL-2.0) +- DO NOT remove compiler/*.res files — they are a legacy reference frontend + pending AffineScript re-target. The governance CI failure is pre-existing. + +## Known Pre-existing CI Failure + +governance / Language / package anti-pattern policy FAILS on every PR and on +main because compiler/src/*.res files exist. This is intentional/legacy — the +compiler is a reference frontend in a non-standard early ReScript dialect. The +runnable implementation is in cli/. Resolution: AffineScript re-target +(contractiles/lust/Intentfile INTENT-001). Do NOT work around it by removing +.res files or patching governance.yml. ## Canonical File Locations -### Machine-Readable Metadata (.machine_readable/) -- `.machine_readable/AGENTIC.scm` -- `.machine_readable/ECOSYSTEM.scm` -- `.machine_readable/META.scm` -- `.machine_readable/NEUROSYM.scm` -- `.machine_readable/PLAYBOOK.scm` -- `.machine_readable/STATE.scm` +### Human Orientation +- `EXPLAINME.adoc` — Comprehensive human/agent orientation (read this too) +- `README.adoc` — GitHub landing page overview + +### Machine-Readable Metadata (.machine_readable/6a2/) +- `.machine_readable/6a2/STATE.a2ml` — Current project state and session history +- `.machine_readable/6a2/META.a2ml` — Architecture decisions (ADR-0001: Echo types) +- `.machine_readable/6a2/AGENTIC.a2ml` — Agent permissions and constraints +- `.machine_readable/6a2/ECOSYSTEM.a2ml` — Ecosystem position and related projects +- `.machine_readable/6a2/NEUROSYM.a2ml` — Hypatia symbolic rules for Echo invariants +- `.machine_readable/6a2/PLAYBOOK.a2ml` — Operational playbook +### Operational Framework (contractiles/) +- `contractiles/must/Mustfile` — Required invariants and validation checks +- `contractiles/dust/Dustfile` — Recovery and rollback handlers +- `contractiles/trust/Trustfile.hs` — Trust model and verification steps +- `contractiles/lust/Intentfile` — Roadmap and intent (INTENT-001 through 005) ### Specification (spec/) -- `spec/grammar.ebnf` — Canonical EBNF grammar (@taxonomy: spec/grammar) +- `spec/grammar.ebnf` — Canonical EBNF grammar (@taxonomy: spec/grammar) +- `spec/type-system.md` — Type system spec including §7 Echo Types +- `spec/README.adoc` — Specification index -- `spec/README.adoc` — Specification index +### Key Documentation (docs/) +- `docs/Echo-Decomposition.adoc` — Echo types authoritative narrative +- `docs/Design-Philosophy.adoc` — Why the language is designed this way +- `docs/Error-Lang.adoc` — Full language reference +- `docs/Error-Categories.adoc` — Nine error categories + stability debits +- `docs/Curriculum.adoc` — Lesson sequence (Lessons 1–11) ### Verification (verification/) -- `verification/proofs/` — Formal proofs -- `verification/tests/` — Test suite ../compiler/test -(symlink) -- `verification/conformance/` — Conformance tests ../conformance -(symlink) -- `verification/benchmarks/` — Performance benchmarks ../bench -(symlink) -- `verification/fuzzing/` — Fuzz targets ../compiler/fuzz -(symlink) -- `verification/README.adoc` — Verification index +- `verification/proofs/` — Formal proofs +- `verification/tests/` — Test suite (symlink → ../compiler/test) +- `verification/conformance/` — Conformance tests (symlink → ../conformance) +- `verification/benchmarks/` — Performance benchmarks (symlink → ../bench) +- `verification/fuzzing/` — Fuzz targets (symlink → ../compiler/fuzz) -## Taxonomy Index +### Compiler (reference frontend — non-standard ReScript dialect) +- `compiler/src/Types.res` — Token + type AST (TyEcho, TyEchoResidue) +- `compiler/src/Lexer.res` — Tokenizer (Echo, EchoR keywords) +- `compiler/src/Parser.res` — AST builder (type expression parser) +- `compiler/src/TypeChecker.res` — Type inference + unification (Echo rules) +- `compiler/src/Bytecode.res` — VEcho/VResidue values + Echo opcodes +- `compiler/src/VM.res` — Stack VM (echoEraseCost = 15.0) +- `compiler/src/Codegen.res` — AST → bytecode -- `spec/grammar.ebnf` — @taxonomy: spec/grammar +### CLI (runnable implementation) +- `cli/runtime.js` — Main runtime (Deno) +- `cli/analyze.js` — Stability analysis +- `cli/five-whys.js` — Root cause tracing +- `cli/layer-navigator.js` — Five-layer view -- `spec/README.adoc` — @taxonomy: spec/index -- `verification/README.adoc` — @taxonomy: verification/index -- `playground/compiler/src/lexer/Lexer.res` — @taxonomy: compiler/lexer -- `playground/compiler/src/parser/Parser.res` — @taxonomy: compiler/parser -- `editors/error-lang.tmLanguage.json` — @taxonomy: editors/textmate-grammar +### Examples +- `examples/01-hello-world.err` — Baseline +- `examples/11-echo-decomposition.err` — Echo types (full demo with gutter zone) + +## Taxonomy Index + +- `spec/grammar.ebnf` — @taxonomy: spec/grammar +- `spec/type-system.md` — @taxonomy: spec/type-system +- `spec/README.adoc` — @taxonomy: spec/index +- `docs/Echo-Decomposition.adoc` — @taxonomy: docs/echo-decomposition +- `verification/README.adoc` — @taxonomy: verification/index +- `compiler/src/Lexer.res` — @taxonomy: compiler/lexer +- `compiler/src/Parser.res` — @taxonomy: compiler/parser +- `compiler/src/TypeChecker.res` — @taxonomy: compiler/typechecker +- `compiler/src/VM.res` — @taxonomy: compiler/vm ## Session Startup Sequence 1. Read this manifest (0-AI-MANIFEST.a2ml) -2. Read `.machine_readable/STATE.scm` for current progress -3. Read `.machine_readable/META.scm` for architecture decisions -4. Read `.machine_readable/ECOSYSTEM.scm` for ecosystem context +2. Read `EXPLAINME.adoc` for comprehensive orientation +3. Read `.machine_readable/6a2/STATE.a2ml` for current project state +4. Read `.machine_readable/6a2/META.a2ml` for architecture decisions +5. Read `.machine_readable/6a2/AGENTIC.a2ml` for agent constraints +6. Read `.machine_readable/6a2/ECOSYSTEM.a2ml` for ecosystem context + +## Session Exit Sequence + +1. Update `.machine_readable/6a2/STATE.a2ml` with session outcomes +2. Ensure all new files have SPDX-License-Identifier: MPL-2.0 headers +3. Ensure Echo decomposition invariants are intact (run contractiles/must/Mustfile checks) diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc new file mode 100644 index 0000000..2411584 --- /dev/null +++ b/EXPLAINME.adoc @@ -0,0 +1,314 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += EXPLAINME — Error-Lang +:toc: left +:toclevels: 3 +:sectnums: +:icons: font +:source-highlighter: rouge + +This document is the starting point for anyone — human or AI agent — arriving at this +repository without context. Read it before touching code. + +== What is Error-Lang? + +Error-Lang is an *educational programming language* built around one idea: +**make the ways programs go wrong visible, measurable, and explorable**. + +Most teaching languages hide complexity until it bites you. Error-Lang does the opposite +— it surfaces failure modes as first-class citizens. You write programs, they partially +decay, type structures collapse, stability scores drop, and you see exactly why. + +The result is that learners develop *intuition* about language design, type systems, +and failure semantics before those failures become production incidents. + +=== The one-sentence pitch + +____ +A dissembling, decompositional programming language where programs, types, and semantics +can decay over time — and the language makes that decay *visible* rather than hiding it. +____ + +=== What makes it unusual + +[cols="1,2"] +|=== +| Feature | What it means + +| **Stability Score** +| Every program execution produces a 0–100 stability score. Code choices (and decay) + debit this score in real time, like a craftsperson's quality gauge. + +| **Echo Types** +| Structured loss is first-class: `Echo` is a *retained witness* + visible output; + `EchoR` is the *non-recoverable residue* after the witness is erased. + Decomposition is always visible — never silent. + +| **The Gutter Zone** +| The `gutter` (ошибка) block is a pedagogically-safe space where deliberate errors are + injected and their effects made observable without crashing the program. + +| **Computational Haptics** +| An animated stability bar, color coding, and sparkline history give you visceral + feedback about code quality — you *feel* the consequences of design decisions. + +| **Paradoxes** +| Ten deliberate quirks (positional operators, scope leakage, temporal corruption…) + make implicit language assumptions *explicit* through contradiction. +|=== + +== Core Concepts + +=== Stability Score + +Every program starts at 100. Actions that introduce uncertainty, complexity, or +structured loss debit the score. The score is visible at all times and cannot be +hidden — that's the point. + +Key debits (from `docs/Error-Categories.adoc`): + +[cols="1,1"] +|=== +| Action | Score Debit + +| Security error | −20 +| Logical error / Interface error | −15 +| Echo erasure (`echo_to_residue`) | −15 +| Runtime / Resource / Arithmetic error | −10 +| Semantic error | −10 +| Syntax / Linker error | −5 +|=== + +=== Echo Types (`Echo` / `EchoR`) + +Echo types are Error-Lang's first-class shape for *structured loss* — situations where +information is necessarily shed, but where that loss must be *visible* and *costed*. + +==== The governing invariant + +____ +*Decomposition must be visible.* `echo_to_residue` is never a silent cast. `EchoR` is +never an `Echo` with a missing field. The stability debit is never hidden. +____ + +==== The two types + +[source,error-lang] +---- +let e : Echo = echo(42, "answer") + # e carries BOTH the witness (42) and the output ("answer") + # echo_input(e) → 42 + # echo_output(e) → "answer" + +let r : EchoR = echo_to_residue(e) + # Stability: 100 → 85 (the [Stab-Erase] debit fires here) + # r carries ONLY the output — the witness is genuinely gone + # echo_output(r) → "answer" (output survives) + # echo_input(r) → TYPE ERROR and RUNTIME ERROR (non-recoverable) +---- + +==== The five builtins (mirror EchoTypes.jl) + +[cols="1,2,2"] +|=== +| Builtin | Signature | Notes + +| `echo(x, y)` | `(A, B) → Echo` | Construct witness + output +| `echo_to_residue(e)` | `Echo → EchoR` | Erase witness; debits stability +| `echo_input(e)` | `Echo → A` | Illegal on `EchoR` +| `echo_output(e)` | `Echo \| EchoR → B` | Output survives erasure +| `residue_strictly_loses(r)` | `EchoR → Bool` | Always `true` +|=== + +==== Why irreversibility matters + +`Echo` and `EchoR` are *distinct types* — they never unify. You cannot cast +a residue back into an Echo. This models real information loss: once a hash replaces a +plaintext, or a summary replaces a document, the original is gone. Error-Lang makes +that boundary visible at compile time and enforces it at runtime. + +See link:docs/Echo-Decomposition.adoc[docs/Echo-Decomposition.adoc] and +link:spec/type-system.md[spec/type-system.md] §7 for the full specification. + +=== The Paradoxes + +Ten core quirks make implicit language assumptions explicit: + +1. **Type Quantum Superposition** — unannotated variables exist in multiple types until first use +2. **Scope Leakage** — variables escape blocks on prime-numbered lines +3. **Positional Operator Semantics** — `+` adds on even columns, concatenates on odd +4. **Context-Collapse Keywords** — `maybe`, `sometimes`, `usually` affect runtime semantics +5. **Temporal Corruption** — previous run history infects current execution +6. **Reserved Word Roulette** — keywords shift meaning by context +7. **Arithmetic Drift** — math accumulates small deterministic errors +8. **Null Propagation Cascade** — null spreads like a virus through dependent variables +9. **Global State Entanglement** — globals affect each other in non-local ways +10. **Memory Phantom** — freed memory sometimes persists + +=== The Gutter Zone + +[source,error-lang] +---- +main + let e = echo(42, "answer") + let r = echo_to_residue(e) # stability 100 → 85 + + gutter + # Code here is executed but errors are contained. + # A residue cannot recover its witness — this is both + # a type error and a runtime error: + println(echo_input(r)) + end + + println("Still running after the gutter.") +end +---- + +The `gutter` block is the pedagogically-safe error zone: errors inside it are +injected, observed, and then *recovered from* — the program continues. It teaches +error handling without halting the learning session. + +== How to Run Programs + +=== Prerequisites + +* https://deno.land[Deno] (runtime) + +=== Quick start + +[source,bash] +---- +git clone https://github.com/hyperpolymath/error-lang.git +cd error-lang +deno run -A cli/runtime.js examples/01-hello-world.err +deno run -A cli/runtime.js examples/11-echo-decomposition.err +---- + +=== Available CLI tools + +[source,bash] +---- +deno run -A cli/runtime.js # Run a program +deno run -A cli/analyze.js # Stability analysis +deno run -A cli/five-whys.js # Root cause trace +deno run -A cli/layer-navigator.js # Five-layer view +deno run -A cli/visual-feedback.js # Haptics output +---- + +== Architecture + +=== The pipeline + +[source] +---- +Source (.err) + │ + ▼ [Lexer — tokenizes; Echo/EchoR are keywords] + │ + ▼ [Parser — produces AST; parses Echo type annotations] + │ + ▼ [Type Checker — unifies types; enforces Echo/EchoR irreversibility] + │ + ▼ [Codegen — emits bytecode; Echo builtins map to dedicated opcodes] + │ + ▼ [VM — executes; echo_to_residue debits stability score] + │ +Output + Stability Score + Haptics +---- + +=== Key source locations + +[cols="1,2"] +|=== +| Path | What lives there + +| `compiler/src/Types.res` | Token and type AST definitions (including `TyEcho`, `TyEchoResidue`) +| `compiler/src/Lexer.res` | Tokenizer; `Echo`/`EchoR` keyword map +| `compiler/src/Parser.res` | AST builder; type expression parser (handles `>>` splitting) +| `compiler/src/TypeChecker.res` | Type inference + unification; Echo builtin rules +| `compiler/src/Bytecode.res` | `VEcho`/`VResidue` runtime values; Echo opcodes +| `compiler/src/VM.res` | Stack VM; `echo_to_residue` debits `echoEraseCost = 15.0` +| `compiler/src/Codegen.res` | AST → bytecode; Echo builtins → dedicated opcodes +| `compiler/test/` | Type-checker, parser, lexer, and runtime tests +| `cli/` | Deno-based CLI tools (the runnable implementation) +| `examples/` | Annotated `.err` programs (01–11 + others) +| `spec/` | EBNF grammar, type-system spec, axiomatic/operational semantics +| `docs/` | Human-readable design documents (AsciiDoc) +| `contractiles/` | Operational invariants, recovery semantics, trust, roadmap +| `.machine_readable/6a2/` | Machine-readable manifests (STATE, META, AGENTIC, etc.) +|=== + +NOTE: `compiler/src/*.res` is a *reference frontend* written in a non-standard ReScript +dialect. The runnable implementation is `cli/`. The ReScript tree does not build against +mainstream ReScript — this is a pre-existing intentional choice pending AffineScript +re-target. Do not attempt to fix it by removing `.res` files. + +=== The Compiler note (important for contributors) + +The `compiler/` directory uses an early, non-standard ReScript dialect: +`return`/`break` statements, `dict` with non-string keys, and element-returning +`arr[i]`. This dialect predates any standard toolchain. A formal +*AffineScript re-target* (ADR-pending) will migrate the reference frontend to standard +tooling. Until then, follow each file's established idioms when extending the compiler. + +== Documentation Map + +[cols="1,2"] +|=== +| Document | Purpose + +| link:README.adoc[README.adoc] | Project overview and quick-start (GitHub landing page) +| link:EXPLAINME.adoc[EXPLAINME.adoc] | This file — comprehensive orientation +| link:spec/type-system.md[spec/type-system.md] | Type system specification (including §7 Echo Types) +| link:spec/grammar.ebnf[spec/grammar.ebnf] | Canonical EBNF grammar +| link:docs/Echo-Decomposition.adoc[docs/Echo-Decomposition.adoc] | Echo types — authoritative narrative +| link:docs/Design-Philosophy.adoc[docs/Design-Philosophy.adoc] | Why the language is designed this way +| link:docs/Error-Lang.adoc[docs/Error-Lang.adoc] | Full language reference +| link:docs/Error-Categories.adoc[docs/Error-Categories.adoc] | Nine error categories + stability debits +| link:docs/Curriculum.adoc[docs/Curriculum.adoc] | Lesson sequence (Lessons 1–11) +| link:docs/Educational-Framework.adoc[docs/Educational-Framework.adoc] | Pedagogy and learning theory +| link:contractiles/README.adoc[contractiles/README.adoc] | Operational framework overview +| link:.machine_readable/6a2/STATE.a2ml[.machine_readable/6a2/STATE.a2ml] | Current project state (for AI agents) +| link:0-AI-MANIFEST.a2ml[0-AI-MANIFEST.a2ml] | AI agent gateway manifest (read first) +|=== + +== What Comes Next + +=== Imminent (ADR-pending) + +* **AffineScript re-target** — migrate `compiler/src/*.res` to a standard, buildable + dialect. This resolves the `governance / Language / package anti-pattern policy` CI + failure (ReScript ban) that currently hits every PR from `main`. + +=== Medium-term + +* **First-class functions in VM** — enables whole-fibre `Echo` (the full Agda proof + that `f x ≡ y`, not just a pairing); the current single-witness runtime is a stepping + stone. + +=== Long-term + +* **Formal Echo soundness proof in Agda** — the `echo-types` repo carries the Agda + mechanization; Error-Lang will eventually include a formal bridge between its runtime + model and the Agda proof. +* **Benchmark lineage chains** — measure erasure cost against the theoretical + Landauer bound; link Error-Lang's `echoEraseCost` to the physics. + +== For AI Agents + +Read link:0-AI-MANIFEST.a2ml[0-AI-MANIFEST.a2ml] first — it is the canonical gateway +for AI agents. Then read link:.machine_readable/6a2/STATE.a2ml[STATE.a2ml] for current +project state. + +Key constraints (from link:.machine_readable/6a2/AGENTIC.a2ml[AGENTIC.a2ml]): + +* Never make `echo_to_residue` a silent cast +* Never let `EchoR` unify with or coerce to `Echo` +* Never hide the erasure stability debit (`[Stab-Erase]`) +* Never delete spec files (`spec/grammar.ebnf`, `spec/SPEC.core.scm`) +* Never use banned languages (TypeScript, Python, Go, Node.js) +* Never commit secrets +* All new GitHub Actions must be SHA-pinned +* All new source files must have SPDX-License-Identifier headers +* Never use the AGPL license (use MPL-2.0) +* SCM files live ONLY in `.machine_readable/` — root copies are symlinks diff --git a/README.adoc b/README.adoc index df35cf0..8b78ef5 100644 --- a/README.adoc +++ b/README.adoc @@ -61,6 +61,8 @@ Error-Lang makes programming learnable the way crafts are learnable - through di Unlike traditional teaching languages that hide complexity, Error-Lang **exposes complexity** and makes it explorable through **computational haptics** - visual feedback that lets you _feel_ code quality like a craftsperson feels their materials. +Error-Lang is a *dissembling*, *decompositional* language: programs, syntax, semantics, and types can decay, decompose, and destabilise over time — and the language makes that decomposition **visible** rather than hiding it. Its `Echo` types give *structured loss* a first-class shape (`Echo` retained witness + visible output; `EchoR` the non-recoverable residue after `echo_to_residue`, which debits stability). The governing rule is **decomposition must be visible**. See `docs/Echo-Decomposition.adoc`. + === The Craftsperson Analogy [quote, The Design Philosophy] diff --git a/compiler/test/EchoRuntimeTest.res b/compiler/test/EchoRuntimeTest.res new file mode 100644 index 0000000..1adec4a --- /dev/null +++ b/compiler/test/EchoRuntimeTest.res @@ -0,0 +1,105 @@ +// SPDX-License-Identifier: MPL-2.0 +// EchoRuntimeTest.res — semantic / runtime decomposition plane for Echo types. +// +// Proves the runtime half of "decomposition must be visible": +// - echo(x, y) builds VEcho{input, output} +// - echo_input works on VEcho, FAILS on a residue (witness genuinely gone) +// - echo_output works on BOTH VEcho and VResidue (output survives) +// - echo_to_residue yields VResidue and debits stability EXACTLY ONCE +// - projection (echo_input / echo_output) never debits stability + +open Bytecode +open TestHelpers + +let dummyLoc: Types.location = { + start: {line: 1, column: 1, offset: 0}, + end_: {line: 1, column: 1, offset: 0}, + file: "", +} + +// Build a chunk from a bare opcode list (locations unused by these opcodes). +let chunkOf = (code: array): chunk => { + code, + constants: [], + locations: [], +} + +// Run a chunk; return (result, final stability score). +let runChunk = (code: array): (result, float) => { + let vm = VM.make(chunkOf(code)) + let r = VM.run(vm) + (r, vm.stabilityScore) +} + +// echo(1, "a") — input pushed first, output second (OpEcho pops output then input). +let echoProgram: array = [OpPush(VInt(1)), OpPush(VString("a")), OpEcho] + +let testEchoConstructsWitness = () => { + suite("Echo runtime: construction") + let (r, _) = runChunk(Array.concat(echoProgram, [OpHalt])) + assertEqual("echo(1, \"a\") builds VEcho{input:1, output:\"a\"}", r, Ok(VEcho({input: VInt(1), output: VString("a")}))) +} + +let testProjections = () => { + suite("Echo runtime: projection") + let (inp, _) = runChunk(Array.concat(echoProgram, [OpEchoInput, OpHalt])) + assertEqual("echo_input recovers the witness", inp, Ok(VInt(1))) + + let (out, _) = runChunk(Array.concat(echoProgram, [OpEchoOutput, OpHalt])) + assertEqual("echo_output recovers the output", out, Ok(VString("a"))) +} + +let testToResidue = () => { + suite("Echo runtime: decomposition to residue") + let (res, _) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpHalt])) + assertEqual("echo_to_residue yields VResidue{output:\"a\"}", res, Ok(VResidue({output: VString("a")}))) + + // Output still recoverable from the residue. + let (out, _) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpEchoOutput, OpHalt])) + assertEqual("echo_output survives erasure", out, Ok(VString("a"))) + + // residue_strictly_loses reports non-recoverability for a residue, not for an echo. + let (lossR, _) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpResidueStrictlyLoses, OpHalt])) + assertEqual("residue_strictly_loses(residue) = true", lossR, Ok(VBool(true))) + let (lossE, _) = runChunk(Array.concat(echoProgram, [OpResidueStrictlyLoses, OpHalt])) + assertEqual("residue_strictly_loses(echo) = false", lossE, Ok(VBool(false))) +} + +let testWitnessActuallyGone = () => { + suite("Echo runtime: witness is genuinely unavailable after erasure") + // echo_input on a residue must be a runtime error, not silently nil. + let (r, _) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpEchoInput, OpHalt])) + switch r { + | Error(_) => assertTrue("echo_input on residue fails at runtime", true) + | Ok(_) => assertTrue("echo_input on residue fails at runtime", false) + } +} + +let testStabilityDebitedExactlyOnce = () => { + suite("Echo runtime: stability debit is visible and charged exactly once") + // No erasure → no debit. + let (_, sPlain) = runChunk(Array.concat(echoProgram, [OpEchoOutput, OpHalt])) + assertEqual("projection alone does not debit stability", sPlain, 100.0) + + // One erasure → exactly one debit (echoEraseCost = 15.0). + let (_, sErase) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpHalt])) + assertEqual("echo_to_residue debits stability once", sErase, 100.0 -. VM.echoEraseCost) + + // Erasure then projection → still exactly one debit (projection is free). + let (_, sEraseThenProj) = runChunk(Array.concat(echoProgram, [OpEchoToResidue, OpEchoOutput, OpHalt])) + assertEqual("projection after erasure adds no further debit", sEraseThenProj, 100.0 -. VM.echoEraseCost) +} + +let runAll = () => { + Console.log("\n========================================") + Console.log(" ERROR-LANG ECHO RUNTIME TESTS") + Console.log("========================================") + testEchoConstructsWitness() + testProjections() + testToResidue() + testWitnessActuallyGone() + testStabilityDebitedExactlyOnce() + summarize() +} + +let _ = runAll() diff --git a/compiler/test/ParserTest.res b/compiler/test/ParserTest.res index 466cd8c..d83e523 100644 --- a/compiler/test/ParserTest.res +++ b/compiler/test/ParserTest.res @@ -1170,6 +1170,22 @@ let testEchoAnnotations = () => { } | _ => assertTrue("single-arg echo annotated let parsed", false) } + + // Nested form: the closing `>>` must be split, not read as a shift token. + let prog5 = parseSource("let e: Echo> = 1") + switch prog5.declarations[0] { + | Some(StmtDecl(LetStmt({type_}))) => + switch type_ { + | Some(TyEcho(Some(TyEcho(Some(TyInt), Some(TyString))), None)) => + assertTrue("nested Echo> parses (>> split)", true) + | _ => assertTrue("nested Echo> parses (>> split)", false) + } + | _ => assertTrue("nested echo annotated let parsed", false) + } + + // Malformed Echo annotation must fail clearly (a diagnostic is raised). + let (_, diags) = parseWithDiagnostics("let e: Echo 0) } // ============================================ diff --git a/compiler/test/TypeCheckerTest.res b/compiler/test/TypeCheckerTest.res index 6d58fa8..4775a67 100644 --- a/compiler/test/TypeCheckerTest.res +++ b/compiler/test/TypeCheckerTest.res @@ -648,6 +648,75 @@ let testResidueStrictlyLoses = () => { assertNoErrors(result, "residue_strictly_loses returns Bool") } +let testResidueDoesNotUnifyBackIntoEcho = () => { + // let e: Echo = echo_to_residue(echo(1, "a")) — residue is not an Echo + let prog: program = { + declarations: [ + StmtDecl( + LetStmt({ + mutable_: false, + name: "e", + type_: Some(Types.TyEcho(Some(Types.TyInt), Some(Types.TyString))), + value: Call( + Ident("echo_to_residue", dummyLoc), + [echoCall(IntLit(1, dummyLoc), StringLit("a", dummyLoc))], + dummyLoc, + ), + loc: dummyLoc, + }), + ), + ], + loc: dummyLoc, + } + let result = checkProgram(prog) + assertHasErrors(result, "EchoR does not unify back into Echo") +} + +let testNoImplicitEchoToOutputCoercion = () => { + // let s: String = echo(1, "a") — an Echo is not its output; no implicit Echo -> B + let prog: program = { + declarations: [ + StmtDecl( + LetStmt({ + mutable_: false, + name: "s", + type_: Some(Types.TyString), + value: echoCall(IntLit(1, dummyLoc), StringLit("a", dummyLoc)), + loc: dummyLoc, + }), + ), + ], + loc: dummyLoc, + } + let result = checkProgram(prog) + assertHasErrors(result, "no implicit Echo -> B coercion") +} + +let testEchoOutputOnResidue = () => { + // let s: String = echo_output(echo_to_residue(echo(1, "a"))) — output survives erasure + let residue = Call( + Ident("echo_to_residue", dummyLoc), + [echoCall(IntLit(1, dummyLoc), StringLit("a", dummyLoc))], + dummyLoc, + ) + let prog: program = { + declarations: [ + StmtDecl( + LetStmt({ + mutable_: false, + name: "s", + type_: Some(Types.TyString), + value: Call(Ident("echo_output", dummyLoc), [residue], dummyLoc), + loc: dummyLoc, + }), + ), + ], + loc: dummyLoc, + } + let result = checkProgram(prog) + assertNoErrors(result, "echo_output on a residue yields the retained output type") +} + // ============================================ // Run All Tests // ============================================ @@ -713,6 +782,9 @@ let runAllTests = () => { testEchoInputOnResidueFails() testEchoOutputRetained() testResidueStrictlyLoses() + testResidueDoesNotUnifyBackIntoEcho() + testNoImplicitEchoToOutputCoercion() + testEchoOutputOnResidue() Console.log("") Console.log("=== Tests Complete ===") diff --git a/contractiles/README.adoc b/contractiles/README.adoc index d19a387..989f312 100644 --- a/contractiles/README.adoc +++ b/contractiles/README.adoc @@ -1,19 +1,74 @@ -= Contractiles Template Set +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += Error-Lang Contractiles :toc: :sectnums: -This directory contains the generalized contractiles templates. Copy the `contractiles/` directory into a new repo to establish a consistent operational, validation, trust, recovery, and intent framework. +This directory contains the *operational contract* for the Error-Lang project. +Contractiles are the invariant, recovery, trust, and intent framework that +governs how the project evolves, how failures are recovered from, and where it +is going. -== Fill-In Instructions +== Contents -1. Update the Mustfile to reflect your real invariants (paths, schema versions, ports). -2. Replace Trustfile.hs placeholders with your actual key paths and verification commands. -3. Adjust Dustfile handlers to match your rollback and recovery tooling. -4. Update Intentfile to mirror the roadmap you want the system to evolve toward. +[cols="1,1,2"] +|=== +| File | Status | Purpose -== Contents +| `must/Mustfile` +| ✅ Active +| Required invariants — what must ALWAYS be true. Run these checks to verify + project health. + +| `dust/Dustfile` +| ✅ Active +| Recovery semantics — what to do when something breaks. Rollback handlers + and undo procedures. + +| `trust/Trustfile.hs` +| ✅ Active +| Trust and verification — cryptographic and semantic verification steps. + +| `lust/Intentfile` +| ✅ Active +| Intent and roadmap — where this project is going and why. +|=== + +== How to Use + +=== Verifying invariants (must/) + +[source,bash] +---- +# The Mustfile defines checks that must pass before any release. +# Run individual checks by extracting the `run:` commands. +# A `just` recipe (`just validate-rsr`) runs the composite check. +just validate-rsr +---- + +=== Recovery from failures (dust/) + +Consult `dust/Dustfile` when something breaks. Each handler names the +failure event, the undo action, and the verification step. + +The most critical handlers are: + +* `echo-invariant-violation` — the decomposition-must-be-visible invariant was broken +* `stability-debit-missing` — `echo_to_residue` ran but stability was not debited +* `residue-unified-with-echo` — the type checker let `EchoR` unify into `Echo` + +=== Critical invariants + +The non-negotiable invariants for this project: + +1. **SPDX headers** — every source file has a valid `SPDX-License-Identifier` header +2. **Echo decomposition is visible** — `echo_to_residue` always debits stability, + `EchoR` never unifies with `Echo`, `echo_input` is always rejected on a residue +3. **Grammar is canonical** — `spec/grammar.ebnf` is the single source of truth +4. **No banned languages** — TypeScript, Python, Go, Node.js are banned at runtime + boundaries (the existing `compiler/*.res` is legacy, pending AffineScript re-target) +5. **Spec files intact** — `spec/grammar.ebnf` and `spec/SPEC.core.scm` are never deleted -* `must/Mustfile` - required invariants and validations. -* `trust/Trustfile.hs` - cryptographic verification steps. -* `dust/Dustfile` - rollback and recovery semantics. -* `lust/Intentfile` - future intent and roadmap direction. +See link:../docs/Echo-Decomposition.adoc[docs/Echo-Decomposition.adoc] and +link:../spec/type-system.md[spec/type-system.md] §7 for the Echo decomposition contract. +See link:../0-AI-MANIFEST.a2ml[0-AI-MANIFEST.a2ml] for the full agent-readable invariant list. diff --git a/contractiles/dust/Dustfile b/contractiles/dust/Dustfile index 6f93c6a..4835fff 100644 --- a/contractiles/dust/Dustfile +++ b/contractiles/dust/Dustfile @@ -1,29 +1,123 @@ -# SPDX-License-Identifier: PLMP-1.0-or-later -# Dustfile template - recovery and rollback semantics +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# Dustfile — Error-Lang recovery and rollback semantics version: 1 +# Recovery handlers are ordered by severity (critical first). +# Each handler names the failure event, the undo action, a verification step, +# and notes explaining what went wrong. + recovery: - logs: - - name: decision-log - path: logs/decisions.json - reversible: true - handler: "log-replay --reverse logs/decisions.json" - - policy: - - name: policy-rollback - path: policy/policy.ncl - rollback: "git checkout HEAD~1 -- policy/policy.ncl" - notes: "Rollback policy to the previous known-good revision." - - gateway: - - name: bad-deployment - event: "deploy.failure" - undo: "kubectl rollout undo deployment/gateway" - notes: "Undo a failed deployment while preserving audit logs." - - dust-events: - - name: decision-log-to-dust - source: logs/decisions.json - transform: "dustify --input logs/decisions.json --output logs/dust-events.json" - notes: "Map gateway decision logs into reversible dust events." + + echo-invariant-violation: + name: echo-invariant-violation + event: "decomposition-must-be-visible invariant broken" + description: > + The core Echo invariant was violated: either echo_to_residue became a + silent cast (no stability debit), EchoR was allowed to unify with Echo, + or echo_input was accepted on a residue without error. + undo: "git revert HEAD --no-edit" + verify: > + bash -uc ' + grep -q "echoEraseCost = 15.0" compiler/src/VM.res && + grep -q "echo_input.*illegal\|non-recoverable" compiler/src/TypeChecker.res && + grep -q "Stab-Erase" spec/type-system.md + ' + notes: > + This is the most critical invariant in the project. See + docs/Echo-Decomposition.adoc and spec/type-system.md §7 for the full + contract. The three sub-invariants are: (1) echo_to_residue always costs + stability, (2) EchoR never unifies back into Echo, (3) echo_input is a + type and runtime error on EchoR. + + stability-debit-missing: + name: stability-debit-missing + event: "echo_to_residue executed but stability score was not debited" + description: > + The VM executed OpEchoToResidue but the echoEraseCost subtraction was + missing or bypassed. + undo: "git checkout HEAD -- compiler/src/VM.res" + verify: > + bash -uc 'grep -A3 "OpEchoToResidue" compiler/src/VM.res | grep -q "stabilityScore"' + notes: > + The debit must occur exactly once per erasure, never on mere projection + (echo_input / echo_output). If the debit fires on projection, that is + also a bug — check OpEchoInput / OpEchoOutput in VM.res. + + residue-unified-with-echo: + name: residue-unified-with-echo + event: "type checker allowed EchoR to unify with Echo" + description: > + The unification algorithm in TypeChecker.res accepted a constraint that + paired TyEcho with TyEchoR, making the residue type coerce back into + the witness type. This breaks irreversibility. + undo: "git checkout HEAD -- compiler/src/TypeChecker.res" + verify: > + bash -uc 'grep -q "TyEchoR.*TyEcho\|TyEcho.*TyEchoR" compiler/src/TypeChecker.res' + notes: > + The unification rule that should exist: TyEcho(a1,b1) unifies with + TyEcho(a2,b2) (recursively); TyEchoR(a1,b1) unifies with TyEchoR(a2,b2); + but TyEcho never unifies with TyEchoR. See TypeChecker.res unify function. + + compiler-pipeline-crash: + name: compiler-pipeline-crash + event: "any compiler phase panics or throws on valid input" + description: > + A lexer, parser, type checker, codegen, or VM operation crashes on + syntactically and semantically valid Error-Lang source. + undo: "git checkout HEAD~1 -- compiler/src/" + verify: > + bash -uc 'deno run -A cli/runtime.js examples/01-hello-world.err && + deno run -A cli/runtime.js examples/11-echo-decomposition.err' + notes: > + The reference program examples/11-echo-decomposition.err exercises the + full Echo pipeline. If that runs cleanly, the core pipeline is healthy. + examples/01-hello-world.err checks the baseline. + + grammar-divergence: + name: grammar-divergence + event: "spec/grammar.ebnf diverged from actual parser behaviour" + description: > + The EBNF grammar in spec/grammar.ebnf no longer matches what the + Parser.res accepts. This creates a spec/implementation split. + undo: "git checkout HEAD -- spec/grammar.ebnf" + verify: > + bash -uc 'test -s spec/grammar.ebnf' + notes: > + The canonical grammar is spec/grammar.ebnf. Any change to Parser.res + that extends the grammar must be reflected there. Do not delete or + truncate spec/grammar.ebnf — it is a protected spec file. + + ci-governance-failure: + name: ci-governance-failure + event: "governance / Language / package anti-pattern policy fails on PR" + description: > + The governance check fails because .res files exist in compiler/src/. + This is a PRE-EXISTING condition that also fails on main. It is NOT + caused by Echo types or any recent work. Resolution requires the + AffineScript re-target (ADR-pending). + undo: "no-op — this failure is expected and intentional until re-target" + verify: > + bash -uc 'git log --oneline main..HEAD | grep -q "." || echo "no new commits"' + notes: > + DO NOT attempt to fix this by removing .res files, renaming them, or + patching the governance workflow. The correct resolution is the + AffineScript re-target. The check fails identically on main. All other + CI checks (Hypatia, CodeQL, licence consistency, etc.) pass. + + spdx-header-missing: + name: spdx-header-missing + event: "a new source file was committed without an SPDX header" + description: > + A file was added to the repository without the required + SPDX-License-Identifier: MPL-2.0 header. + undo: > + Add the SPDX header to the affected file and amend or add a new commit. + Format: "# SPDX-License-Identifier: MPL-2.0" (first non-shebang line). + verify: > + bash -uc 'git ls-files | grep -E "\.(res|js|ts|zig|a2ml|scm|ncl)$" | + xargs grep -L "SPDX-License-Identifier" | grep -v node_modules' + notes: > + The licence consistency governance check will catch this on CI. + Use MPL-2.0 for all Error-Lang source. Never use AGPL. diff --git a/contractiles/lust/Intentfile b/contractiles/lust/Intentfile new file mode 100644 index 0000000..1b4aba3 --- /dev/null +++ b/contractiles/lust/Intentfile @@ -0,0 +1,113 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# Intentfile — Error-Lang roadmap and intent +# +# "Lust" in the contractiles framework means: what does this project *want* +# to become? These are not bug fixes — they are the evolutionary direction. +# Intent is aspirational; must/ is mandatory. + +version: 1 + +metadata: + name: error-lang-intent + last-updated: "2026-06-02" + author: "hyperpolymath" + +# The governing principle that all intent items must serve: +principle: > + Decomposition must be visible. Every path this project takes should make the + ways programs, types, and semantics can decay more observable, more + understandable, and more controllable — not less. + +intent: + + - id: INTENT-001 + title: "AffineScript re-target" + horizon: "short-term" + priority: "critical" + description: > + Migrate compiler/src/*.res from the non-standard early ReScript dialect + to AffineScript or standard ReScript. This resolves the estate-wide + `governance / Language / package anti-pattern policy` CI failure (ReScript + ban) that currently fails on every PR and on main identically. + why: > + The reference frontend currently uses return/break statements, non-string- + keyed Dict, and element-returning arr[i] — idioms from a pre-standard + dialect. Until re-targeted, CI will permanently report one failing check. + The runnable implementation (cli/) is unaffected. + acceptance: > + `governance / Language / package anti-pattern policy` passes on a PR + that migrates compiler/src/. The Echo type system additions are preserved + verbatim (same semantics, different syntax). + adr: "ADR-pending" + + - id: INTENT-002 + title: "First-class functions in the VM" + horizon: "medium-term" + priority: "high" + description: > + The current VM has no first-class functions. Echo is therefore a + single-witness pairing (VEcho{input, output}) rather than a full fibre + witness (fiber(f, domain, y) with proof f x ≡ y). First-class functions + unlock the whole-fibre model. + why: > + The Agda mechanization in echo-types proves Echo := Σ(x:A), (f x ≡ y). + The current runtime captures the pairing but not the function. Adding + first-class functions lets Error-Lang host the full fibre structure and + makes the educational story complete. + acceptance: > + `let f = fn(x) { x + 1 } in echo(f, 42, f(42))` type-checks and runs, + producing a full fibre witness that can be decomposed with echo_to_residue. + + - id: INTENT-003 + title: "Formal Echo soundness proof in Agda" + horizon: "long-term" + priority: "medium" + description: > + Produce a formal bridge between Error-Lang's runtime Echo model and the + Agda mechanization in hyperpolymath/echo-types. This would prove that + the VEcho/VResidue runtime values are a sound implementation of the + fibre type Echo := Σ(x:A), (f x ≡ y). + why: > + Error-Lang is a *model*, not a proof. The Agda repo is the source of + mechanized truth. A formal bridge ensures the model stays faithful and + gives students a path from the runnable language to the formal proof. + acceptance: > + An Agda module in verification/proofs/ that defines a semantics function + from Error-Lang VM states to Agda Echo types and proves that the semantics + function preserves the Echo/EchoR distinction. + + - id: INTENT-004 + title: "Landauer benchmark for erasure cost" + horizon: "long-term" + priority: "low" + description: > + Measure the runtime cost of echo_to_residue (memory, entropy, time) and + compare it to the theoretical Landauer bound for one bit of information + erasure at room temperature. + why: > + The echoEraseCost = 15.0 stability debit is pedagogically motivated, not + physically derived. Benchmarking against the Landauer bound would connect + the educational model to real thermodynamic cost of information erasure, + making the "loss is not free" lesson physically grounded. + acceptance: > + A benchmark in verification/benchmarks/ that measures echo_to_residue + wall-clock and memory, produces a cost-per-bit estimate, and compares it + to kT ln 2 at 300K (~3×10⁻²¹ J per bit). + + - id: INTENT-005 + title: "LSP server with Echo decomposition tracking" + horizon: "medium-term" + priority: "medium" + description: > + Extend the LSP server to report Echo/EchoR type information in hover + tooltips, and to highlight the stability debit in the editor gutter at + the echo_to_residue call site. + why: > + Computational haptics is the core educational mechanism. Showing the + stability debit *at the exact line* where echo_to_residue is called makes + the "decomposition must be visible" invariant physically present in the + editor, not just in the terminal. + acceptance: > + Hovering over `echo_to_residue(e)` in VS Code shows "EchoR — witness + erased; stability −15". The gutter shows the debit icon next to that line. diff --git a/contractiles/must/Mustfile b/contractiles/must/Mustfile index dc2c6b6..9b4023e 100644 --- a/contractiles/must/Mustfile +++ b/contractiles/must/Mustfile @@ -1,35 +1,98 @@ -# SPDX-License-Identifier: PLMP-1.0-or-later -# Mustfile - declarative state contract (template) +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# Mustfile — Error-Lang required invariants # See: https://github.com/hyperpolymath/mustfile version: 1 metadata: - name: project-state-contract - spec: v0.0.1 - description: "Invariant checks for config, policy, gateway, logs, and schema." + name: error-lang-state-contract + spec: v0.2.0 + description: > + Invariant checks for the Error-Lang project. These must pass before any + release. The most critical invariants concern Echo decomposition visibility + (decomposition must be visible — never silent, never free). parameters: - gateway_port: "8080" - schema_version: "v0.0.1" + echo_erase_cost: "15.0" + spec_version: "v0.2.0" checks: - - name: config-valid - description: "config/service.yaml must be valid." - run: "yq -e '.' config/service.yaml >/dev/null" + - name: spdx-headers-present + description: > + All source files (.res, .js, .ts, .zig, .adoc, .md, .a2ml, .scm, .ncl) + must carry a valid SPDX-License-Identifier header. + run: > + bash -uc 'git ls-files | grep -E "\.(res|js|ts|zig|adoc|a2ml|scm|ncl)$" | + xargs grep -rL "SPDX-License-Identifier" | grep -v node_modules | grep -v ".git" + | { read out; [ -z "$out" ] || (echo "Missing SPDX: $out" && exit 1); }' - - name: policy-compiles - description: "policy/policy.ncl must compile." - run: "nickel check policy/policy.ncl" + - name: grammar-canonical + description: > + The canonical EBNF grammar spec/grammar.ebnf must exist and must not be + empty. It is the single source of truth for Error-Lang syntax. + run: "bash -uc 'test -s spec/grammar.ebnf'" - - name: gateway-exposes-port - description: "Service must expose the configured port." - run: "bash -uc 'ss -lnt | rg \":${GATEWAY_PORT:-8080}\"'" + - name: spec-files-intact + description: > + spec/grammar.ebnf must exist. SPEC.core.scm will be checked when available. + run: "bash -uc 'test -f spec/grammar.ebnf'" - - name: logs-are-json - description: "Logs must be JSON." - run: "bash -uc 'rg --files -g \"*.json\" logs | xargs -r jq -e .'" + - name: echo-type-system-spec-present + description: > + spec/type-system.md must contain Echo type definitions (§7). This verifies + that the Echo decomposition contract has been documented. + run: > + bash -uc 'grep -q "Echo" spec/type-system.md && grep -q "EchoR" spec/type-system.md + && grep -q "Stab-Erase" spec/type-system.md' - - name: schema-version-matches - description: "Schema must match version spec." - run: "bash -uc 'rg -n \"${SCHEMA_VERSION:-v0.0.1}\" schema'" + - name: echo-decomposition-doc-present + description: > + docs/Echo-Decomposition.adoc must exist and contain the governing invariant. + run: > + bash -uc 'test -f docs/Echo-Decomposition.adoc && + grep -q "decomposition must be visible" docs/Echo-Decomposition.adoc' + + - name: echo-erase-cost-defined + description: > + The VM must define echoEraseCost matching the contractual value (15.0). + This is the [Stab-Erase] stability debit for echo_to_residue. + run: > + bash -uc 'grep -q "echoEraseCost = 15.0" compiler/src/VM.res' + + - name: echo-residue-not-unified-spec + description: > + The type-system spec must document that TyEcho and TyEchoR never unify. + run: > + bash -uc 'grep -q "never unif" spec/type-system.md || + grep -q "does not unify" spec/type-system.md' + + - name: no-banned-languages-at-runtime + description: > + The cli/ runtime must not import TypeScript, Python, Go, or Node.js + modules at the process boundary. (The compiler/*.res reference frontend + is exempted — it is legacy pending AffineScript re-target.) + run: > + bash -uc '! grep -rn "require(\"typescript\")\|import.*from.*\"typescript\"" + cli/ 2>/dev/null | grep -v ".git"' + + - name: machine-readable-in-subdir + description: > + Machine-readable state files must live under .machine_readable/, never + directly at the repo root (root copies must be symlinks). + run: > + bash -uc 'for f in STATE.a2ml META.a2ml AGENTIC.a2ml ECOSYSTEM.a2ml + NEUROSYM.a2ml PLAYBOOK.a2ml; do + [ ! -e "$f" ] || [ -L "$f" ] || (echo "Root SCM file not a symlink: $f" && exit 1) + done' + + - name: ai-manifest-present + description: > + 0-AI-MANIFEST.a2ml must exist at the repo root. It is the AI agent gateway. + run: "bash -uc 'test -f 0-AI-MANIFEST.a2ml'" + + - name: explainme-present + description: > + EXPLAINME.adoc must exist at the repo root. It is the human/agent + orientation document. + run: "bash -uc 'test -f EXPLAINME.adoc'" diff --git a/contractiles/trust/Trustfile.hs b/contractiles/trust/Trustfile.hs new file mode 100644 index 0000000..7e97893 --- /dev/null +++ b/contractiles/trust/Trustfile.hs @@ -0,0 +1,105 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Trustfile.hs — Error-Lang trust and verification semantics +-- +-- This file describes the trust model for the project: what we verify, +-- what we trust transitively, and how to confirm integrity. +-- It is written in Haskell syntax as a specification document. + +module ErrorLang.Trust where + +-- | The trust model for Error-Lang sources. +data TrustSource + = RepoOwner -- hyperpolymath — unconditional trust + | SignedCommit -- GPG-signed commit from a listed key + | CI -- Any check from .github/workflows/ passing + | ExternalDep -- Third-party code (Deno std, etc.) + deriving (Show, Eq) + +-- | Verification steps, in order of execution. +-- Run these to confirm project integrity before a release. +data VerificationStep = VerificationStep + { stepName :: String + , stepCommand :: String + , stepReason :: String + } deriving (Show) + +verificationSteps :: [VerificationStep] +verificationSteps = + [ VerificationStep + { stepName = "licence-consistency" + , stepCommand = "git ls-files | xargs grep -L 'SPDX-License-Identifier' \ + \| grep -E '\\.(res|js|zig|a2ml)$' | grep -v node_modules" + , stepReason = "All source must carry MPL-2.0 header. Never AGPL." + } + , VerificationStep + { stepName = "echo-decomposition-invariant" + , stepCommand = "grep -q 'echoEraseCost = 15.0' compiler/src/VM.res \ + \&& grep -q 'TyEchoR' compiler/src/TypeChecker.res" + , stepReason = "decomposition must be visible: erasure costs stability, \ + \EchoR does not unify with Echo." + } + , VerificationStep + { stepName = "grammar-canonical" + , stepCommand = "test -s spec/grammar.ebnf" + , stepReason = "spec/grammar.ebnf is the canonical source of truth for \ + \Error-Lang syntax. Must never be empty or deleted." + } + , VerificationStep + { stepName = "spec-type-system" + , stepCommand = "grep -q 'Echo' spec/type-system.md \ + \&& grep -q 'Stab-Erase' spec/type-system.md" + , stepReason = "The type-system spec must document Echo types (§7) \ + \and the [Stab-Erase] stability rule." + } + , VerificationStep + { stepName = "no-banned-runtime-languages" + , stepCommand = "! grep -rn 'require(\"typescript\")' cli/ 2>/dev/null" + , stepReason = "TypeScript, Python, Go, Node.js are banned at runtime \ + \boundaries. The compiler/*.res reference frontend is \ + \exempt (legacy, pending AffineScript re-target)." + } + , VerificationStep + { stepName = "ci-checks-passing" + , stepCommand = "gh pr view --json statusCheckRollup 2>/dev/null \ + \| jq '.statusCheckRollup[] | select(.state != \"SUCCESS\")'" + , stepReason = "All CI checks except governance/Language/package-anti-pattern \ + \must pass. That check fails pre-existingly on main (ReScript \ + \ban; resolves with AffineScript re-target)." + } + , VerificationStep + { stepName = "machine-readable-not-at-root" + , stepCommand = "for f in STATE.a2ml META.a2ml AGENTIC.a2ml; do \ + \ [ ! -e \"$f\" ] || [ -L \"$f\" ] || exit 1; done" + , stepReason = "SCM files must live in .machine_readable/. Root copies \ + \must be symlinks, never plain files." + } + ] + +-- | The external dependencies we transitively trust. +-- These should be reviewed on major version bumps. +trustedDependencies :: [(String, String, String)] +trustedDependencies = + [ ( "deno.land/std" + , "Deno standard library" + , "Used in cli/ runtime tools; trust the Deno project." + ) + , ( "hyperpolymath/standards" + , "Estate-wide governance reusable workflow" + , "Called by .github/workflows/governance.yml via @main; \ + \trust the estate owner (same as repo owner)." + ) + , ( "hyperpolymath/echo-types" + , "Agda mechanization of Echo fiber types" + , "Source of mechanized truth for Echo := Σ(x:A), (f x ≡ y). \ + \Error-Lang's Echo is a single-witness runtime model; Agda is the proof." + ) + ] + +-- | Release gate: all verificationSteps must pass, +-- and no dependency in trustedDependencies has a pending security advisory. +releaseGate :: String +releaseGate = + "Run all verificationSteps. Check Dependabot for advisories. \ + \Tag only after `just validate-rsr` passes." diff --git a/docs/Curriculum.adoc b/docs/Curriculum.adoc index f84041d..c4603f7 100644 --- a/docs/Curriculum.adoc +++ b/docs/Curriculum.adoc @@ -296,6 +296,40 @@ end * Error cascades * Panic mode recovery +=== Lesson 11: Structured Loss (Echo) + +**Concept**: Decomposition made visible — loss can be structured, but it is never free or hidden + +**The Problem**: +Most languages discard information silently. Error-Lang makes the *moment of loss* +observable: an `Echo` holds a witness and its output; `echo_to_residue` +erases the witness into an `EchoR`, debiting the Stability Score. + +**Example**: +[source,err] +---- +main + let e = echo(42, "answer") # Echo + println(echo_input(e)) # 42 — witness still here + println(echo_output(e)) # "answer" + + let r = echo_to_residue(e) # erasure — stability drops here + println(echo_output(r)) # "answer" survives + println(residue_strictly_loses(r)) # true — loss is observable + + gutter + println(echo_input(r)) # ERROR: the witness is gone + end +end +---- + +**Learning Objectives**: + +* Structured loss vs. silent discard +* Irreversibility: `EchoR` never coerces back to `Echo` +* Consequence amplification: the erasure stability debit is visible, charged once +* The invariant *decomposition must be visible* + == Assessment Ideas === Quiz Format diff --git a/docs/Design-Philosophy.adoc b/docs/Design-Philosophy.adoc index 99a23f7..71f6b70 100644 --- a/docs/Design-Philosophy.adoc +++ b/docs/Design-Philosophy.adoc @@ -115,6 +115,36 @@ end **Learning outcome:** State persists. Programs have history. +== Structured Loss: Decomposition Made Visible (Echo) + +The contradictions above show *meaning* decaying. Echo types show *information* +decaying — but **deliberately, observably, and irreversibly**. + +Error-Lang is a dissembling, decompositional language: programs, syntax, +semantics, and types can decay or destabilise, and the language exposes that +decomposition rather than hiding it. Echo gives that idea a first-class shape: + +[cols="1,3",options="header"] +|=== +| Form | Meaning +| `Echo` | a retained witness `x : A` plus the visible output `y : B` it reached +| `EchoR` | the residue after irreversible erasure — the witness is gone, only the output survives +| `echo_to_residue(e)` | the explicit decomposition step that destroys the witness and **debits stability** +|=== + +The governing invariant is **decomposition must be visible**: `echo_to_residue` +is never a silent cast, `EchoR` is not an `Echo` with a missing field, and the +stability debit (consequence amplification, applied via the `[Stab-Erase]` rule) +is never hidden. A learner should be able to see the exact moment structured loss +becomes non-recoverable residue. + +**Learning outcome:** Loss can be structured — but structure is not free, and the +type system refuses to let you pretend the residue is still recoverable. + +See `docs/Echo-Decomposition.adoc` for the full narrative and the three +decomposition planes (syntactic, semantic/runtime, type-checking), and +`spec/type-system.md` §7 for the formal rules. + == The Paradigm Shift After Error-Lang, students will think differently: diff --git a/docs/Echo-Decomposition.adoc b/docs/Echo-Decomposition.adoc new file mode 100644 index 0000000..f57cc8c --- /dev/null +++ b/docs/Echo-Decomposition.adoc @@ -0,0 +1,151 @@ +// SPDX-License-Identifier: MPL-2.0 += Echo Types: Decomposition Made Visible +:toc: +:sectnums: +:source-highlighter: rouge + +== Why Echo belongs in Error-Lang + +Error-Lang is not merely "a language with errors." It is a *dissembling*, +*decompositional* educational language. Its distinctive claim is that programs — +their syntax, their semantics, and their types — can **decay, decompose, and +destabilise over time**, sometimes gracefully and sometimes catastrophically, +and that this decomposition is itself something the language can *expose* and +*reason about*. + +Most languages treat loss as something to be hidden: a discarded value, an +erased witness, a collapsed abstraction — gone silently. Error-Lang takes the +opposite stance, consistent with its core principle of **consequence +amplification** (see `Design-Philosophy.adoc`): when structure is lost, the loss +must be *seen*. + +**Echo types are how Error-Lang gives structured loss a first-class shape** — in +the runtime *and* in the type checker — adapted from the constructive Agda +library https://github.com/hyperpolymath/echo-types[echo-types] and its +executable companion https://github.com/hyperpolymath/EchoTypes.jl[EchoTypes.jl]. +Where those upstream repos model echoes conservatively (ghost/static, proof +relevant), Error-Lang makes the *decomposition step itself* observable: + +[cols="1,3",options="header"] +|=== +| Form | Meaning + +| `Echo` +| A **retained witness** `x : A` together with the **visible output** `y : B` + it reached — one element of the fibre of a function `A → B`. + +| `EchoR` +| The **residue** after an *irreversible erasure*: the `A`-witness is gone + (non-recoverable); only reachability of the output `B` survives. + +| `echo_to_residue` +| The **explicit decomposition step** — `Echo → EchoR` — that destroys + the witness and incurs a stability cost. It is never a silent cast. +|=== + +== The educational invariant: decomposition must be visible + +The single invariant that governs every design and test decision for Echo: + +[IMPORTANT] +==== +**Decomposition must be visible.** + +A learner must be able to *see the exact moment* structured loss becomes +non-recoverable residue. + +* `echo_to_residue` must **not** become a silent cast. +* `EchoR` must **not** behave like an `Echo` with a missing field. +* The stability debit must **not** be hidden inside incidental runtime behaviour. +==== + +This is why Echo is valuable *here* specifically: it turns an abstract +type-theoretic idea (the fibre / structured loss) into a concrete, observable +decomposition event that a student can trigger, watch, and reason about. + +== The three decomposition planes + +The proof/test obligation for Echo is **not** the shallow "Echo typechecks." It +is: _the code's decomposition behaviour is represented syntactically, +semantically, and in type checking._ Echo is therefore specified and tested +across three planes. + +=== Plane 1 — Syntactic decomposition + +How the loss is *written and rendered*. + +* Parsing and pretty-printing **preserve** `Echo` and `EchoR` forms (round-trip). +* Malformed Echo syntax **fails clearly**, not silently. +* Sugar lowers **predictably**: ++ +[cols="1,2",options="header"] +|=== +| Surface | Lowering +| `Echo` | `TyEcho(Some(A), Some(B))` +| `Echo` | `TyEcho(Some(A), None)` — codomain inferred (treated as `Any`) +| `Echo` | `TyEcho(None, None)` — opaque fallback / unresolved +|=== +* Nested forms — e.g. `Echo>` — do **not** confuse the + greedy `>>` lexing of type annotations (the parser splits a fused `>>` token). + +=== Plane 2 — Semantic / runtime decomposition + +How the loss *behaves when it runs* (single-witness core; whole-fibre awaits +first-class functions). + +* `echo(x, y)` produces `VEcho{input: x, output: y}`. +* `echo_input` works on `VEcho`, and **fails on a residue**. +* `echo_output` works on **both** `VEcho` and `VResidue` (the output survives). +* `echo_to_residue(VEcho{x, y})` produces `VResidue{output: y}`. +* After residue conversion the input witness is **actually unavailable** — not + merely hidden. +* `residue_strictly_loses` reports the non-recoverability property. +* Stability is debited **exactly once**, by `echo_to_residue` — and **not** by + mere projection (`echo_input` / `echo_output` never touch stability). + +=== Plane 3 — Type-checking decomposition + +How the loss is *enforced in the types*. + +* `Echo` unifies **only** structurally with `Echo`. +* `Echo` does **not** unify with `EchoR`. +* `EchoR` does **not** unify back into `Echo`. +* `echo_input : Echo -> A` — and is **illegal** on `EchoR`. +* `echo_output : Echo | EchoR -> B`. +* `echo_to_residue : Echo -> EchoR`. +* There is **no implicit coercion** `Echo -> EchoR` or `Echo -> B`. + +== The contract, in one place + +[source] +---- +echo(x, y) : (A, B) -> Echo +echo_to_residue(e) : Echo -> EchoR (+ stability debit) +residue_strictly_loses(r) : EchoR -> Bool +echo_input(e) : Echo -> A (illegal on residue) +echo_output(e) : Echo|EchoR -> B +---- + +Canonical names mirror EchoTypes.jl so the concept maps 1:1 across the three +codebases; shorter aliases (`residue`, `residue_loses`) may be added later but +the canonical names preserve the conceptual mapping. + +== Relationship to the wider Echo lineage + +* https://github.com/hyperpolymath/echo-types[echo-types] (Agda) — the **source + of mechanized truth**: `Echo f y := Σ (x : A), (f x ≡ y)`. +* https://github.com/hyperpolymath/EchoTypes.jl[EchoTypes.jl] (Julia) — the + **finite-domain executable model** (a model, not a proof). +* **Error-Lang** — the **operational, stability-aware, decomposition-visible** + embedding: not a proof assistant, so `f x ≡ y` is carried as a runtime pairing + rather than a HoTT path; the value of Echo here is the *visible decomposition + story*, not the importing of cross-estate vocabulary. + +== See also + +* `spec/type-system.md` §7 — formal typing rules, unification, and the + `[Stab-Erase]` stability rule. +* `docs/Design-Philosophy.adoc` — consequence amplification and the stability + score that the erasure debit feeds into. +* `compiler/test/TypeCheckerTest.res`, `ParserTest.res`, `EchoRuntimeTest.res` — + the proof/test pass across the three planes above. diff --git a/docs/Educational-Framework.adoc b/docs/Educational-Framework.adoc index 4ad9e41..2b3e2c6 100644 --- a/docs/Educational-Framework.adoc +++ b/docs/Educational-Framework.adoc @@ -437,6 +437,7 @@ Students can see and modify aspects interactively! - AST visualization - How code becomes data structures - Tree traversal and transformation +- Structured loss with Echo: `echo_to_residue` as a visible, irreversible decomposition step (`Echo` → `EchoR`), and why the witness cannot be recovered — see `docs/Echo-Decomposition.adoc` - **Layer focus:** AST (Layer 3) === Week 7-8: Parsing and Grammars diff --git a/docs/Error-Categories.adoc b/docs/Error-Categories.adoc index 3a80e22..fded553 100644 --- a/docs/Error-Categories.adoc +++ b/docs/Error-Categories.adoc @@ -256,8 +256,13 @@ The `gutter` (ошибка) block is where errors are injected: | Arithmetic | -10 | Numeric edge cases | Interface | -15 | Design concepts | Security | -20 | Critical importance +| Echo erasure | -15 | Structured loss is not free: `echo_to_residue` debits stability ([Stab-Erase]), charged once and never on projection |=== +NOTE: The Echo-erasure debit is not an *error* category — it is a deliberate, +visible decomposition cost. It appears here because it feeds the same Stability +Score. See `docs/Echo-Decomposition.adoc` and `spec/type-system.md` §7. + == Implementation Notes === Compiler Phases diff --git a/docs/Error-Lang.adoc b/docs/Error-Lang.adoc index 5c82371..09f133a 100644 --- a/docs/Error-Lang.adoc +++ b/docs/Error-Lang.adoc @@ -43,6 +43,22 @@ error reduces the score. At S=0, execution still works but output becomes This creates the "it's working, but it's falling apart" aesthetic. +=== Structured Loss Is Visible (Echo) + +Where Jenga Semantics decay the *whole program*, Echo types decay a *single +value* — deliberately, observably, and irreversibly. Error-Lang is a +decompositional language: when structure is lost, the loss must be **seen**. + +* `Echo` — a retained witness `x : A` plus the visible output `y : B` it reached. +* `EchoR` — the non-recoverable residue after erasure (the witness is gone). +* `echo_to_residue(e)` — the explicit decomposition step, `Echo → EchoR`, + which **debits the Stability Score**. + +The governing rule is **decomposition must be visible**: `echo_to_residue` is +never a silent cast, `EchoR` is never an `Echo` with a missing field, and the +stability debit is never hidden. See `docs/Echo-Decomposition.adoc` and +`spec/type-system.md` §7. + === Always Recoverable The parser is error-tolerant. Every injected error is: @@ -88,6 +104,8 @@ end | `gutter` | Error injection zone (safe to break) | `if` / `else` | Conditionals (Stage 2+) | `function` | Function definition (Stage 2+) +| `Echo` | Fibre type: retained witness + visible output (`Echo`) +| `EchoR` | Residue type: non-recoverable remains after erasure (`EchoR`) |=== ==== Literals @@ -124,6 +142,21 @@ end let x = 42 let message = "Hello" let result = x + 10 +let e: Echo = echo(42, "answer") # type annotation: a fibre witness +---- + +==== Echo: Structured Loss + +[source,err] +---- +let e = echo(42, "answer") # Echo: witness 42 reached "answer" +let i = echo_input(e) # 42 — recover the witness +let o = echo_output(e) # "answer" — the visible output + +let r = echo_to_residue(e) # EchoR — witness erased; stability drops +let still = echo_output(r) # "answer" — output survives erasure +let lost = residue_strictly_loses(r) # true — non-recoverability is observable +# echo_input(r) # ERROR: the witness is gone (decomposition is real) ---- ==== Output diff --git a/examples/11-echo-decomposition.err b/examples/11-echo-decomposition.err new file mode 100644 index 0000000..bcca14d --- /dev/null +++ b/examples/11-echo-decomposition.err @@ -0,0 +1,43 @@ +# SPDX-License-Identifier: MPL-2.0 +# Example: Structured Loss with Echo +# Learning: decomposition must be VISIBLE — loss can be structured, but never free or hidden + +main + # An Echo is a retained witness plus the visible output it reached. + # echo(42, "answer") : Echo — "input 42 reached output answer" + let e = echo(42, "answer") + + # While we hold the Echo, both halves are recoverable: + println("witness:", echo_input(e)) # 42 + println("output: ", echo_output(e)) # "answer" + + # THE DECOMPOSITION STEP. + # echo_to_residue erases the witness, leaving a non-recoverable residue. + # This is not a silent cast — it debits the Stability Score ([Stab-Erase]). + let r = echo_to_residue(e) # EchoR ; stability 100 -> 85 + + # The output survives erasure... + println("output still:", echo_output(r)) # "answer" + # ...and the loss itself is observable: + println("strictly loses:", residue_strictly_loses(r)) # true + + gutter + # The witness is genuinely gone. This is a type error AND a runtime error: + # a residue is non-recoverable — EchoR never behaves like an Echo. + println(echo_input(r)) + end + + println("Still running — but the witness is not coming back.") +end + +# 🎓 LEARNING OUTCOME: +# Echo = retained witness + visible output +# EchoR = non-recoverable residue after erasure +# echo_to_residue = the explicit, stability-costed decomposition step +# +# The invariant: DECOMPOSITION MUST BE VISIBLE. +# - echo_to_residue is never a silent cast (watch the stability score drop) +# - EchoR is never an Echo with a missing field (echo_input on it is rejected) +# - the stability debit is charged exactly once, never on mere projection +# +# See docs/Echo-Decomposition.adoc and spec/type-system.md §7. diff --git a/spec/type-system.md b/spec/type-system.md index a940e46..cc82de1 100644 --- a/spec/type-system.md +++ b/spec/type-system.md @@ -272,7 +272,33 @@ Named to mirror EchoTypes.jl, so concepts map 1:1 across the three codebases: `echo_input` on an `EchoR` is a **type error** (and a runtime error): the witness is gone. This is the type system enforcing that loss, once structured, is real. -### 7.5 Fidelity note +### 7.5 Decomposition obligations (decomposition must be visible) + +Error-Lang is a *decompositional* language: Echo's correctness is not "Echo +typechecks" but "the code's decomposition behaviour is represented syntactically, +semantically, and in type checking." The governing invariant is: + +> **Decomposition must be visible.** `echo_to_residue` is never a silent cast; +> `EchoR` never behaves as an `Echo` with a missing field; the stability debit is +> never hidden in incidental runtime behaviour. + +Echo is therefore specified and tested across three planes: + +1. **Syntactic** — parse/pretty-print round-trip for `Echo`/`EchoR`; malformed + Echo fails clearly; sugar lowers predictably (§7.1); nested forms + (`Echo>`) survive the greedy `>>` lexing. +2. **Semantic / runtime** — `echo` builds `VEcho{input,output}`; `echo_input` + works on `VEcho` and fails on `VResidue`; `echo_output` works on both; + `echo_to_residue` yields `VResidue` and the witness becomes genuinely + unavailable; `residue_strictly_loses` reports non-recoverability; stability is + debited **exactly once** by `echo_to_residue` and **never** by projection. +3. **Type-checking** — the unification and builtin rules of §7.3–§7.4, including + `EchoR` not unifying back into `Echo` and no implicit `Echo → EchoR` or + `Echo → B` coercion. + +See `docs/Echo-Decomposition.adoc` for the narrative form of these obligations. + +### 7.6 Fidelity note Error-Lang is a runnable scripting language, not a proof assistant: the equality proof `f x ≡ y` is carried as a runtime-checkable pairing, not a HoTT path. The