Skip to content

Commit 52f57e0

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs: design Error-Lang as a Trope IR front end (trope-particularity integration)
Adds docs/Trope-Particularity-Integration.adoc — a design (not yet implemented) for lowering Error-Lang's Echo operations and stability factors to the language-neutral Trope IR (hyperpolymath/trope-checker, v0.1 prevent profile) and consuming the verified verdict + witness. - Object/effect/grade correspondence: Echo<A,B> <-> Trope[Phi], EchoR <-> FloatingQuality, echo/echo_to_residue/echo_input/echo_output <-> preserve/ detach/project. echo_to_residue IS detach (bond=Severed, irrecoverable), matching the [Stab-Erase] debit and "decomposition must be visible". - stabilityFactor -> grade mapping; the silent instabilities (GlobalState, RaceCondition) land on the deceptive Conflated bottom -> a lowering fault under the prevent profile. - Verdict mapping: scalar calculateStability -> use-model floor + p-sufficient/ p-insufficient + witness edge (the invariant-path argmin Stability.idr already reasons about). - Architecture (reference, never vendor; schema is the trust boundary), the per-front-end O2 lowering-correctness obligations (L-Echo/L-Grade/L-Silent/ L-Floor), and a 4-phase plan. Builds on docs/Echo-Decomposition.adoc; references echo-types, trope-checker and trope-particularity-workbench by URL only. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
1 parent 450c32a commit 52f57e0

1 file changed

Lines changed: 246 additions & 0 deletions

File tree

‎docs/Trope-Particularity-Integration.adoc‎

Lines changed: 246 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,246 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= Trope-Particularity Integration: Error-Lang as a Trope IR Front End
4+
:toc:
5+
:sectnums:
6+
:source-highlighter: rouge
7+
8+
[abstract]
9+
This is a *design* (not yet implemented). It proposes that Error-Lang become a
10+
second *front end* to the portable trope-checker
11+
(https://github.com/hyperpolymath/trope-checker[`hyperpolymath/trope-checker`]),
12+
lowering its Echo operations and its stability factors to the language-neutral
13+
*Trope IR* (v0.1, `prevent` profile) and consuming the checker's verified verdict
14+
and witness. It defines the object/effect/grade correspondence, the verdict
15+
mapping, the architecture (reference, never vendor), and — most importantly — the
16+
per-front-end *lowering-correctness obligations* the trope-checker does **not**
17+
discharge for us.
18+
19+
Both systems already sit on the same substrate: the
20+
https://github.com/hyperpolymath/echo-types[echo-types] graded-loss line, cited
21+
verbatim by `docs/Echo-Decomposition.adoc` and by the trope calculus
22+
(`trope-checker/spec/calculus.adoc`, "Provenance of the ideas"). This document
23+
makes that shared lineage *operational*.
24+
25+
== Motivation: a stability score is a scalar; loss is not
26+
27+
Error-Lang grades instability with `calculateStability` (`compiler/src/Types.res`
28+
lines 270–274):
29+
30+
[source]
31+
----
32+
calculateStability(factors) = max(0, 100 + Σ stabilityImpact(factor))
33+
----
34+
35+
Every `stabilityFactor` is mapped to a single negative integer and the integers
36+
are summed. That is a *scalar collapse* of structured loss. The trope-particularity
37+
calculus exists to reject exactly this move — its load-bearing thesis
38+
(`calculus.adoc` §3) is:
39+
40+
[quote]
41+
A grade is *not a scalar*: two operations can lose the same _amount_ yet differ
42+
in _kind_ and in _honesty_.
43+
44+
So the calculus's three-coordinate grade is a principled *upgrade* of Error-Lang's
45+
stability model. It lets us keep _which_ particularity degraded, whether the loss
46+
is _recoverable_, and whether it is _honest_ — and it yields a use-relative
47+
*verdict* with a *witness edge* ("the operation to repair") in place of an opaque
48+
`0–100` number. For a language whose entire identity is the *visible decomposition*
49+
of structure (`Echo-Decomposition.adoc`, "Decomposition must be visible"), this is
50+
a capability upgrade, not ornament.
51+
52+
Two further alignments make the fit unusually tight:
53+
54+
* **The Echo operations already _are_ trope effects.** `echo`, `echo_to_residue`,
55+
`echo_input`, `echo_output` implement witness-retention and irreversible erasure
56+
— which the calculus names `preserve`, `detach`, and field `project` (§5).
57+
* **The verification toolchains already overlap.** The trope-checker's core is an
58+
Agda reference plus an Idris2 implementation (`trope-checker/src/idris2/Main.idr`);
59+
Error-Lang already carries an Idris2 proof of the *scalar* bound
60+
(`src/abi/Stability.idr`). The integration generalises that proof's target from
61+
a clamped integer to a checked grade.
62+
63+
== The correspondence
64+
65+
=== Objects: Echo ↔ trope, EchoR ↔ FloatingQuality
66+
67+
A trope is a property-instance over the field set
68+
`Φ = {quality, bearer, context, record}` (`calculus.adoc` §2). Error-Lang's
69+
`Echo<A,B>` — a retained witness `x : A` with the visible output `y : B` it
70+
reached — populates Φ as:
71+
72+
[cols="1,2,3",options="header"]
73+
|===
74+
| Φ field | Echo content | Justification
75+
76+
| `bearer` | the witness `x : A` | the *particular* entity the result is a result _of_
77+
| `quality` | the reached output `y : B` (and `f x ≡ y`) | the situated property borne by `x`
78+
| `context` | the function `f` / evaluation site | what individuates this fibre element
79+
| `record` | the runtime pairing `VEcho{input,output}` | honest provenance of how `y` arose
80+
|===
81+
82+
[cols="1,2",options="header"]
83+
|===
84+
| Echo form | Trope IR node
85+
86+
| `Echo<A,B>` | `type: "Trope"`, `present: ["quality","bearer","context","record"]`
87+
| `EchoR<A,B>` | `type: "FloatingQuality"`, `present: ["quality"]` (no `bearer` — the severance is structurally visible)
88+
|===
89+
90+
The type change `Echo → EchoR` is exactly the type change `Trope → FloatingQuality`,
91+
and the reason `echo_input` is *illegal on a residue* (`Echo-Decomposition.adoc`
92+
Plane 3) is, in IR terms, that a `FloatingQuality` node has *no bearer field to
93+
project*. The same fact, two vocabularies.
94+
95+
=== Echo operations → writable effects
96+
97+
[cols="2,2,3",options="header"]
98+
|===
99+
| Echo op | Effect | Grade (per `calculus.adoc` §5)
100+
101+
| `echo(x,y)` | `preserve` | `ε` — all fields `Present`, `bond=Intact`, `merge=Single`
102+
| `echo_output(e)` | `project[quality]` | drop `bearer,context,record`; quality survives; `bond=Withheld`
103+
| `echo_input(e)` | `project[bearer]` | legal only while `bearer ∈ S`; *undefined on `FloatingQuality`*
104+
| `echo_to_residue(e)`| `detach` | `sever`: `fate(quality)=Present`, others `Dropped`, `bond=Severed`, `merge=Single`
105+
|===
106+
107+
The `[Stab-Erase]` rule (`spec/type-system.md` §7) debits stability *exactly once*,
108+
on `echo_to_residue`, and never on projection. That is precisely the calculus's
109+
accounting: `detach` carries the `Severed` (irrecoverable) loss; `project` carries
110+
only a recoverable `Withheld`. The educational invariant "`echo_to_residue` must
111+
**not** become a silent cast" is the calculus's refusal of untagged/deceptive
112+
collapse.
113+
114+
.Worked Trope IR — `echo_to_residue` as a `detach` (illustrative, schema-shaped)
115+
[source,json]
116+
----
117+
{
118+
"version": "0.1", "profile": "prevent",
119+
"nodes": [
120+
{ "id": "e", "type": "Trope", "present": ["quality","bearer","context","record"] },
121+
{ "id": "res", "type": "FloatingQuality", "present": ["quality"] }
122+
],
123+
"edges": [
124+
{ "id": "erase", "effect": "detach", "inputs": ["e"], "output": "res",
125+
"grade": {
126+
"fate": { "quality": {"k":"Present"}, "bearer": {"k":"Dropped"},
127+
"context": {"k":"Dropped"}, "record": {"k":"Dropped"} },
128+
"bond": { "k": "Severed" }, "merge": { "k": "Single" } },
129+
"note": "echo_to_residue: witness erased, output reachable" }
130+
],
131+
"use_model": { "output": "res", "floor": { "bond": { "k": "Withheld" } } }
132+
}
133+
----
134+
135+
Here the floor demands `bond ⊒ Withheld` (the use needs a _recoverable_ bearer);
136+
since `detach` delivered `Severed`, the verdict is `p-insufficient`, witness =
137+
`erase`. A use that only reads `echo_output` would declare a quality-only floor and
138+
pass. The score becomes a *reason*.
139+
140+
=== stabilityFactor → grade
141+
142+
Each `stabilityFactor` becomes a grade, with its `stabilityImpact` magnitude
143+
feeding the fidelity element `δ`. Crucially, the two *silent* instabilities land
144+
on the deceptive `Conflated` bottom — an untagged merge of particulars — which,
145+
under the `prevent` profile, is a *lowering fault* the validator rejects by name.
146+
Error-Lang's worst bugs are the calculus's moral-core violation.
147+
148+
[cols="2,3,2",options="header"]
149+
|===
150+
| Factor | Grade (faithful lowering) | Honesty
151+
152+
| `TypeInstability{reassignments}` | `fate(quality)=Attenuated(15·r)` | faithful
153+
| `NullPropagation{depth}` | `fate(quality)=Attenuated(20·d)`, `Dropped` at the leaf | faithful
154+
| `UnhandledError{paths}` | `fate=Dropped` on the unguarded error fields | faithful (visible gap)
155+
| `AlgorithmComplexity{time_ms}` | `fate=Attenuated(δ)`, `δ=⊤` when unbounded (matches `fix`→`⊤`, §7) | faithful
156+
| `MutableState{mutations,readers}` | `fate(quality)=Attenuated(10·m+5·r)`; `Fused(τ=write-site)` if writes blend | faithful if tracked
157+
| `MemoryLeak{bytes}` | `detach`: `bond=Severed` (owner unreachable, irrecoverable) | faithful
158+
| `GlobalState{mutations,deps}` | `Fused(τ=global@site)` if threaded; **`Conflated` (fault)** if silent | *deceptive when silent*
159+
| `RaceCondition{conflicts}` | `Fused(τ=lock)` if serialised; **`Conflated` (fault)** if unsynchronised | *deceptive when silent*
160+
|===
161+
162+
=== Verdict and witness
163+
164+
[cols="1,2",options="header"]
165+
|===
166+
| Error-Lang today | Trope-checker
167+
168+
| `score = max(0,100+Σ)` | `p-sufficient ⟺ floor(U) ⊑ acc(output)`
169+
| (no locus) | `p-insufficient` + *witness edge* = first edge whose accumulated grade drops below the floor
170+
| `breakdown : dict<string,int>` | per-coordinate retention at each node
171+
| `recommendStabilization(factor)` | human advice *attached to the witnessed edge* (now principled, not heuristic)
172+
| `Stability.idr`: `score ∈ [0,100]` | grade soundness (`calculus.adoc` §8): declared grade never over-claims retention
173+
|===
174+
175+
The witness is, by the calculus's own statement (§6.2), "the trope-particularity
176+
analogue of the invariant-path argmin" — the same argmin shape `Stability.idr`
177+
already reasons about. The verdict thus _subsumes_ the current score: the score is
178+
recoverable as a projection, but the verdict additionally names the edge to repair.
179+
180+
== Architecture: reference, never vendor
181+
182+
[cols="1,3",options="header"]
183+
|===
184+
| Concern | Decision
185+
186+
| Trust boundary | Pin `trope-checker/schemas/trope-ir.schema.json` at `version 0.1`, `profile prevent`. The schema is the contract (mirrors the IR spec's "schema is the trust boundary").
187+
| Dependency | Depend on the `trope-checker` *binary* (a pure `IR → verdict` function) and the *IR schema* by URL. Do **not** vendor the calculus, the checker, or `haec`.
188+
| New backend | Add a `trope` lowering target beside the existing codegen backends: Error-Lang AST/VM ops → Trope IR DAG (schema-validated) → `trope-checker` → verdict object → surfaced as Error-Lang diagnostics.
189+
| Precedent | The same trust-tagged "fold external prover output back into our report" pattern panic-attack uses in `src/aggregate/`.
190+
| Multi-producer | Sanctioned by `trope-ir.adoc`: "a static analyser for an existing language MAY emit Trope IR for code it did not author." Error-Lang's analyzer is exactly such a producer.
191+
|===
192+
193+
== O2 — lowering-correctness obligations (ours to discharge)
194+
195+
The trope-checker proves the *composition* of grades is sound. It explicitly does
196+
**not** prove that an Error-Lang construct lowered to effect `X` _is_ an `X`
197+
(`calculus.adoc` §8, firewall 2; §10-O2). Those are our proof obligations:
198+
199+
[cols="1,4",options="header"]
200+
|===
201+
| ID | Obligation
202+
203+
| *L-Echo* | `OpEchoToResidue` (`VM.res`) semantically _is_ `detach`: the witness becomes unreachable ⇒ `bond=Severed`; output reachability survives ⇒ `fate(quality)=Present`. **Open decision:** is residue's quality `Present`, or `Attenuated(δ)` (only "reachability", not full `y`)? This must be fixed before Phase 1 freezes the lowering.
204+
| *L-Grade* | Each `stabilityFactor`'s grade is a *faithful over-approximation* of the real loss (grade-soundness direction: never claim more retention than occurs). The current `stabilityImpact` magnitudes are heuristic; for soundness `δ` must be a conservative loss bound.
205+
| *L-Silent* | The `Conflated` lowering of `GlobalState`/`RaceCondition` is correct only when the merge is genuinely untagged. If a provenance tag is recoverable, we MUST emit `Fused(τ)` instead; emitting `Conflated` for a tractable merge is a false positive.
206+
| *L-Floor* | The `use_model` floor Error-Lang emits faithfully encodes the program's declared stability requirement (per-function loss signatures, §7 "Declared signatures at the boundaries").
207+
|===
208+
209+
These mirror, in Error-Lang's setting, the open obligations the calculus states for
210+
itself (O1–O4) — and they are checkable with the *same* Idris2 discipline already
211+
used in `src/abi/`.
212+
213+
== Phasing
214+
215+
[cols="1,3",options="header"]
216+
|===
217+
| Phase | Work
218+
219+
| *0 (now)* | Shape the AffineScript Echo types (during the ReScript→AffineScript port) so `Echo`/`EchoR`/`echo_to_residue` lower cleanly to `Trope`/`FloatingQuality`/`detach`. This document + cross-references. *No new runtime coupling.*
220+
| *1* | Implement the `trope` lowering backend for the Echo operations only (the tightest correspondence). Emit schema-valid IR; conformance-test against `trope-checker/tests/conformance/fixtures/`.
221+
| *2* | Lower `stabilityFactor` → grade and emit a `use_model`; surface the verdict + witness as diagnostics alongside (then in place of) the scalar score.
222+
| *3* | Discharge L-Echo / L-Grade / L-Silent / L-Floor as Idris2/Agda proofs; CI-gate the lowering.
223+
|===
224+
225+
== Open questions
226+
227+
* *Profile.* Adopt `prevent` (silent merges rejected at validation — strongest, and
228+
on-message for "decomposition must be visible") or `detect` (representable, caught
229+
at the verdict)? This design assumes `prevent`.
230+
* *Residue fidelity* (L-Echo): `Present` vs `Attenuated(δ)` for `echo_to_residue`.
231+
* *Floor authorship.* Where do use-models come from — a whole-program default, or
232+
per-function loss-signature annotations the learner writes?
233+
* *Coverage* (calculus O1): are all eight `stabilityFactor`s expressible with the
234+
six writable effects? The table above is a well-chosen mapping, not yet a theorem.
235+
236+
== See also
237+
238+
* `docs/Echo-Decomposition.adoc` — the three decomposition planes this builds on.
239+
* `docs/Design-Philosophy.adoc` — consequence amplification and the stability score.
240+
* `spec/type-system.md` §7 — typing rules and the `[Stab-Erase]` stability debit.
241+
* `src/abi/Stability.idr` — the existing Idris2 bound proof (verdict-soundness anchor).
242+
* External (referenced, not vendored):
243+
https://github.com/hyperpolymath/trope-checker[trope-checker] (`spec/calculus.adoc`,
244+
`spec/trope-ir.adoc`, `schemas/trope-ir.schema.json`),
245+
https://github.com/hyperpolymath/trope-particularity-workbench[trope-particularity-workbench]
246+
(the nine effects), https://github.com/hyperpolymath/echo-types[echo-types] (shared substrate).

0 commit comments

Comments
 (0)