Skip to content

Commit ddd4322

Browse files
claudeclaude
committed
docs(echo): design note for echo-types integration (slice 1)
Records the accepted design decisions for the Echo type former: - non-dependent approximation Echo<A => B> (erased map-shaped retained-loss residue), NOT the value-indexed fiber Echo f y; Echo<T> only as later sugar - Echo = proof-relevant content of affine weakening; quantity controls use, Echo records structured loss (born from quantities, not identical) - mode/subtyping laws mirroring EchoLinear weaken + no-section - bridge scope: linear/affine now; provenance/audit next; rest later - surface syntax Echo<A => B> (solo first), ~> reserved, witnesses erased; staging 1-4 - claim boundary held to "loss-graded reindexing modality over a thin poset" (echo-types retraction R-2026-05-18); forbidden-terms list - EchoTypes.jl as a phase-2 differential oracle, not a slice-1 blocker Docs only — no parser/codegen/runtime/proof-layer changes. https://claude.ai/code/session_01VHjceAPA5ZARUe7ESWNQPF
1 parent fff5dfc commit ddd4322

1 file changed

Lines changed: 155 additions & 0 deletions

File tree

‎docs/design/echo-types-integration.md‎

Lines changed: 155 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,155 @@
1+
<!-- SPDX-License-Identifier: MPL-2.0 -->
2+
<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
3+
4+
# Design note: integrating `echo-types` into the my-lang type checker
5+
6+
**Status:** accepted (slice 1) · **Date:** 2026-06-02 · **PR:** #86
7+
**Upstream:** [`hyperpolymath/echo-types`](https://github.com/hyperpolymath/echo-types)
8+
(Agda library) · executable companion
9+
[`hyperpolymath/EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl)
10+
11+
This note records the design decisions for bringing *echo types* — a
12+
formal account of **"loss that is not total erasure"** — into the my-lang
13+
type system. It documents what slice 1 (PR #86) deliberately is and is
14+
not, so later slices stay on the agreed line.
15+
16+
## What an echo type is (upstream)
17+
18+
In `echo-types`, given `f : A → B`, the **echo** at `y : B` is the fiber
19+
20+
```
21+
Echo f y = Σ (x : A), (f x ≡ y)
22+
```
23+
24+
— a *proof-relevant* witness of which inputs collapsed to `y`. It captures
25+
the third case between reversible (no loss) and irreversible (total
26+
erasure): **irreversible-but-with-a-retained, typed constraint on what was
27+
lost**.
28+
29+
## 1. Index shape — non-dependent approximation
30+
31+
my-lang is **not** dependently typed, so we do not index echoes by a
32+
specific function `f` and output `y`. Forcing value-indexing now would drag
33+
the checker into refinement/dependent territory before the language is
34+
ready.
35+
36+
**Canonical form:**
37+
38+
```
39+
Echo<A => B> // internal: Ty::Echo { mode, domain: A, codomain: B }
40+
```
41+
42+
read as *"a retained residue/witness of some admissible collapse from `A`
43+
to `B`"* — **not** the complete fiber of a specific `f` at `y`.
44+
45+
- **Keep** the map-shaped form `Echo<A => B>` as the semantic core; the
46+
source/target asymmetry is essential.
47+
- **Possible sugar later (only if needed):** `Echo<T> := Echo<T => T>` (or
48+
`Echo<Unknown => T>`). `Echo<T>` is *not* the primary form — it is too
49+
modal and discards the asymmetry.
50+
- **Avoid for now:** the value-indexed/dependent `Echo<f, y>` form.
51+
52+
The Agda `Echo f y` remains the *semantic ideal*; `Echo<A => B>` is its
53+
deliberate erased approximation.
54+
55+
## 2. Relationship to the quantity (affine/QTT) system
56+
57+
Echo is **born from** the quantity system but is **not identical** to it:
58+
59+
```
60+
Quantity controls USE.
61+
Echo records the structured LOSS caused by weakening / use-erasure.
62+
```
63+
64+
Design invariant:
65+
66+
> A linear value weakened to affine may **produce** an `Echo` residue. The
67+
> weakening is one-way. The residue is proof-relevant evidence that
68+
> something was lost but **not annihilated**.
69+
70+
The first (and, for now, only) bridge is therefore **linear → affine**.
71+
Echo is **not** made fully orthogonal to quantities yet; orthogonal
72+
modalities (epistemic/security/provenance) can come later.
73+
74+
## 3. Mode and subtyping (slice 1, implemented)
75+
76+
`EchoMode { Linear, Affine }` mirrors `EchoLinear.agda`'s two-point thin
77+
poset `linear ⊑ affine`. Assignability (`Ty::is_assignable_from`) encodes:
78+
79+
```
80+
Echo Linear <: Echo Affine (EchoLinear.weaken)
81+
Echo Affine </: Echo Linear (EchoLinear.no-section-weaken)
82+
domain / codomain invariant
83+
```
84+
85+
The five unit tests in `crates/my-lang/src/types.rs` mirror the Agda
86+
theorems directly: mode ordering (`_≤m_`), `weaken`, `no-section`, and
87+
domain/codomain invariance.
88+
89+
## 4. Bridges — scope
90+
91+
| Bridge | Status |
92+
|--------|--------|
93+
| linear / affine | **in scope now** (slice 1) |
94+
| provenance / audit | next candidate (design-noted, not implemented) |
95+
| epistemic | later |
96+
| security | later |
97+
| graded / tropical | research layer |
98+
| choreographic | separate bridge |
99+
| ordinal | definitely later |
100+
101+
Rationale: provenance/audit/security are tempting because they fit
102+
my-lang's AI/audit features, but introducing them early would contaminate
103+
the core. Slice 1 answers exactly one question — *what proof-relevant
104+
residue remains when linear information is weakened?* — and the audit
105+
bridge later reuses that answer.
106+
107+
## 5. Surface syntax & runtime — staging
108+
109+
First dialect: **solo** (the affine one). Canonical syntax `Echo<A => B>`.
110+
The lossy-arrow `~>` is **reserved** for possible later sugar (lossy
111+
function / operation), not introduced now to avoid overloading. Witnesses
112+
are **erased** initially.
113+
114+
```
115+
Stage 1 (this PR): checker-only Echo type former ← done
116+
Stage 2: parser syntax for Echo<A => B> (solo)
117+
Stage 3: proof-layer residue object (EchoResidue, Coq/Idris)
118+
Stage 4: optional runtime witness — only if audit/provenance needs
119+
observable evidence; modelled as a single residue record,
120+
not a whole fiber
121+
```
122+
123+
## 6. Claim boundary
124+
125+
Hold the narrowed line from `echo-types` retraction **R-2026-05-18**:
126+
127+
> Echo is a **loss-graded reindexing modality over a thin poset**.
128+
129+
Permitted, modest, strong claim:
130+
131+
> Echo models irreversible weakening as a one-way, proof-relevant residue
132+
> transformation. Linear Echo can weaken to Affine Echo. Affine Echo cannot
133+
> reconstruct Linear Echo.
134+
135+
**Do not** use (unless a future proof actually justifies it): "graded
136+
comonad", "universal property", "adjunction", "final/initial semantics",
137+
"free construction".
138+
139+
## 7. EchoTypes.jl as differential oracle
140+
141+
Phase-2, not a blocker for slice 1. The current Rust tests already mirror
142+
the `EchoLinear.agda` weakening/no-section theorems at the type-algebra
143+
level. Once parser syntax or proof-layer residue terms exist, add
144+
finite-domain differential tests against EchoTypes.jl's `LEcho` / `EchoMode`
145+
— for semantic examples, **not** core checker soundness.
146+
147+
## Slice 1 scope (PR #86) — exactly
148+
149+
- `EchoMode { Linear, Affine }`
150+
- `Ty::Echo { mode, domain, codomain }`
151+
- assignability: `Linear → Affine` only; domain/codomain invariant
152+
- `Display`
153+
- five Agda-mirroring tests
154+
155+
No parser, codegen, runtime, or proof-layer changes in this PR.

0 commit comments

Comments
 (0)