feat(types): echo-types integration — Echo type former (slice 1) (#86)

Adds EchoMode { Linear, Affine }, Ty::Echo { mode, domain, codomain }, and
affine-weakening assignability implementing EchoLinear.weaken / no-section-weaken.
5 unit tests mirror the Agda theorems. Claim boundary held to the narrowed
loss-graded reindexing modality over a thin poset (retraction R-2026-05-18).
Design note in docs/design/echo-types-integration.md.

Author: hyperpolymath

crates/my-lang/src/types.rs

@@ -4,6 +4,46 @@
 
 use std::fmt;
 
+/// Linearity mode of an echo residue.
+///
+/// Mirrors `Mode` in the `echo-types` Agda library (`EchoLinear.agda`):
+/// the thin two-point poset `linear ⊑ affine`. `Linear` keeps the full,
+/// proof-relevant fiber witness; `Affine` keeps only the collapsed
+/// residue (all affine echoes over a point are equal — `affine-all-equal`).
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum EchoMode {
+    /// Full fiber retained; distinctions preserved.
+    Linear,
+    /// Collapsed residue; distinctions weakened away.
+    Affine,
+}
+
+impl EchoMode {
+    /// The mode ordering `_≤m_` from `EchoLinear.agda`
+    /// (`linear ≤m linear`, `linear ≤m affine`, `affine ≤m affine`).
+    ///
+    /// `self.weakens_to(other)` is true when an echo at mode `self` may be
+    /// *weakened* to mode `other`. Crucially `Affine` does **not** weaken to
+    /// `Linear`: weakening is lossy and has no section (`no-section-weaken`).
+    pub fn weakens_to(self, other: EchoMode) -> bool {
+        matches!(
+            (self, other),
+            (EchoMode::Linear, EchoMode::Linear)
+                | (EchoMode::Linear, EchoMode::Affine)
+                | (EchoMode::Affine, EchoMode::Affine)
+        )
+    }
+}
+
+impl fmt::Display for EchoMode {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        match self {
+            EchoMode::Linear => write!(f, "linear"),
+            EchoMode::Affine => write!(f, "affine"),
+        }
+    }
+}
+
 /// Internal type representation used during type checking
 #[derive(Debug, Clone, PartialEq)]
 pub enum Ty {
@@ -46,6 +86,20 @@ pub enum Ty {
     /// Effect type
     Effect(Box<Ty>),
 
+    /// Echo type — the proof-relevant residue of a lossy map, after the
+    /// `echo-types` library: `Echo f y = Σ (x : domain) (f x ≡ y)`. We track
+    /// the collapsing map's `domain` and `codomain` plus the linearity
+    /// `mode`. It models "loss that is not total erasure": a typed witness of
+    /// what a `domain` value retained after collapsing into `codomain`.
+    /// `mode` records whether the full fiber (`Linear`) or only the collapsed
+    /// residue (`Affine`) is observable. See the affine bridge in
+    /// `proofs/verification/{coq,idris}/solo-core/EchoResidue.*`.
+    Echo {
+        mode: EchoMode,
+        domain: Box<Ty>,
+        codomain: Box<Ty>,
+    },
+
     /// Type variable (for inference)
     Var(usize),
 
@@ -103,6 +157,17 @@ impl Ty {
                     && p1.iter().zip(p2.iter()).all(|(x, y)| y.is_assignable_from(x)) // contravariant
                     && r1.is_assignable_from(r2) // covariant
             }
+            (
+                Ty::Echo { mode: m_t, domain: d_t, codomain: c_t },
+                Ty::Echo { mode: m_s, domain: d_s, codomain: c_s },
+            ) => {
+                // Echo weakening (EchoLinear `weaken` / `_≤m_`): a more-
+                // informative source echo may be supplied where a less-
+                // informative target is expected — `Linear` weakens to
+                // `Affine`, never the reverse (the weakening has no section,
+                // `no-section-weaken`). Domain and codomain are invariant.
+                m_s.weakens_to(*m_t) && d_t == d_s && c_t == c_s
+            }
             _ => false,
         }
     }
@@ -143,6 +208,9 @@ impl fmt::Display for Ty {
             }
             Ty::AI(inner) => write!(f, "AI<{}>", inner),
             Ty::Effect(inner) => write!(f, "Effect<{}>", inner),
+            Ty::Echo { mode, domain, codomain } => {
+                write!(f, "{} Echo<{} => {}>", mode, domain, codomain)
+            }
             Ty::Var(id) => write!(f, "?{}", id),
             Ty::Error => write!(f, "<error>"),
             Ty::Unknown => write!(f, "<unknown>"),
@@ -182,3 +250,63 @@ pub fn ast_type_to_ty(ty: &crate::ast::Type) -> Ty {
         Type::Constrained { base, .. } => ast_type_to_ty(base),
     }
 }
+
+#[cfg(test)]
+mod echo_tests {
+    use super::*;
+
+    fn echo(mode: EchoMode) -> Ty {
+        Ty::Echo {
+            mode,
+            domain: Box::new(Ty::Bool),
+            codomain: Box::new(Ty::Unit),
+        }
+    }
+
+    // EchoLinear `_≤m_`: linear ⊑ linear, linear ⊑ affine, affine ⊑ affine,
+    // and crucially affine ⋢ linear.
+    #[test]
+    fn mode_ordering_is_thin_poset() {
+        assert!(EchoMode::Linear.weakens_to(EchoMode::Linear));
+        assert!(EchoMode::Linear.weakens_to(EchoMode::Affine));
+        assert!(EchoMode::Affine.weakens_to(EchoMode::Affine));
+        assert!(!EchoMode::Affine.weakens_to(EchoMode::Linear));
+    }
+
+    // EchoLinear `weaken`: a linear echo may be supplied where an affine
+    // echo is expected (target.is_assignable_from(source)).
+    #[test]
+    fn linear_weakens_to_affine() {
+        let affine = echo(EchoMode::Affine);
+        let linear = echo(EchoMode::Linear);
+        assert!(affine.is_assignable_from(&linear));
+    }
+
+    // EchoLinear `no-section-weaken`: weakening is irreversible — an affine
+    // echo is NOT acceptable where a linear echo is required.
+    #[test]
+    fn affine_has_no_section_back_to_linear() {
+        let linear = echo(EchoMode::Linear);
+        let affine = echo(EchoMode::Affine);
+        assert!(!linear.is_assignable_from(&affine));
+    }
+
+    // Same mode is reflexively assignable; mismatched domain/codomain is not.
+    #[test]
+    fn echo_invariant_in_domain_and_codomain() {
+        let a = echo(EchoMode::Linear);
+        assert!(a.is_assignable_from(&a));
+        let other_codomain = Ty::Echo {
+            mode: EchoMode::Linear,
+            domain: Box::new(Ty::Bool),
+            codomain: Box::new(Ty::Int),
+        };
+        assert!(!a.is_assignable_from(&other_codomain));
+    }
+
+    #[test]
+    fn echo_display_renders_mode_and_arrow() {
+        assert_eq!(echo(EchoMode::Linear).to_string(), "linear Echo<Bool => ()>");
+        assert_eq!(echo(EchoMode::Affine).to_string(), "affine Echo<Bool => ()>");
+    }
+}

docs/design/echo-types-integration.md

@@ -0,0 +1,155 @@
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
+
+# Design note: integrating `echo-types` into the my-lang type checker
+
+**Status:** accepted (slice 1) · **Date:** 2026-06-02 · **PR:** #86
+**Upstream:** [`hyperpolymath/echo-types`](https://github.com/hyperpolymath/echo-types)
+(Agda library) · executable companion
+[`hyperpolymath/EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl)
+
+This note records the design decisions for bringing *echo types* — a
+formal account of **"loss that is not total erasure"** — into the my-lang
+type system. It documents what slice 1 (PR #86) deliberately is and is
+not, so later slices stay on the agreed line.
+
+## What an echo type is (upstream)
+
+In `echo-types`, given `f : A → B`, the **echo** at `y : B` is the fiber
+
+```
+Echo f y = Σ (x : A), (f x ≡ y)
+```
+
+— a *proof-relevant* witness of which inputs collapsed to `y`. It captures
+the third case between reversible (no loss) and irreversible (total
+erasure): **irreversible-but-with-a-retained, typed constraint on what was
+lost**.
+
+## 1. Index shape — non-dependent approximation
+
+my-lang is **not** dependently typed, so we do not index echoes by a
+specific function `f` and output `y`. Forcing value-indexing now would drag
+the checker into refinement/dependent territory before the language is
+ready.
+
+**Canonical form:**
+
+```
+Echo<A => B>          // internal: Ty::Echo { mode, domain: A, codomain: B }
+```
+
+read as *"a retained residue/witness of some admissible collapse from `A`
+to `B`"* — **not** the complete fiber of a specific `f` at `y`.
+
+- **Keep** the map-shaped form `Echo<A => B>` as the semantic core; the
+  source/target asymmetry is essential.
+- **Possible sugar later (only if needed):** `Echo<T> := Echo<T => T>` (or
+  `Echo<Unknown => T>`). `Echo<T>` is *not* the primary form — it is too
+  modal and discards the asymmetry.
+- **Avoid for now:** the value-indexed/dependent `Echo<f, y>` form.
+
+The Agda `Echo f y` remains the *semantic ideal*; `Echo<A => B>` is its
+deliberate erased approximation.
+
+## 2. Relationship to the quantity (affine/QTT) system
+
+Echo is **born from** the quantity system but is **not identical** to it:
+
+```
+Quantity controls USE.
+Echo records the structured LOSS caused by weakening / use-erasure.
+```
+
+Design invariant:
+
+> A linear value weakened to affine may **produce** an `Echo` residue. The
+> weakening is one-way. The residue is proof-relevant evidence that
+> something was lost but **not annihilated**.
+
+The first (and, for now, only) bridge is therefore **linear → affine**.
+Echo is **not** made fully orthogonal to quantities yet; orthogonal
+modalities (epistemic/security/provenance) can come later.
+
+## 3. Mode and subtyping (slice 1, implemented)
+
+`EchoMode { Linear, Affine }` mirrors `EchoLinear.agda`'s two-point thin
+poset `linear ⊑ affine`. Assignability (`Ty::is_assignable_from`) encodes:
+
+```
+Echo Linear  <:  Echo Affine          (EchoLinear.weaken)
+Echo Affine  </: Echo Linear          (EchoLinear.no-section-weaken)
+domain / codomain invariant
+```
+
+The five unit tests in `crates/my-lang/src/types.rs` mirror the Agda
+theorems directly: mode ordering (`_≤m_`), `weaken`, `no-section`, and
+domain/codomain invariance.
+
+## 4. Bridges — scope
+
+| Bridge | Status |
+|--------|--------|
+| linear / affine | **in scope now** (slice 1) |
+| provenance / audit | next candidate (design-noted, not implemented) |
+| epistemic | later |
+| security | later |
+| graded / tropical | research layer |
+| choreographic | separate bridge |
+| ordinal | definitely later |
+
+Rationale: provenance/audit/security are tempting because they fit
+my-lang's AI/audit features, but introducing them early would contaminate
+the core. Slice 1 answers exactly one question — *what proof-relevant
+residue remains when linear information is weakened?* — and the audit
+bridge later reuses that answer.
+
+## 5. Surface syntax & runtime — staging
+
+First dialect: **solo** (the affine one). Canonical syntax `Echo<A => B>`.
+The lossy-arrow `~>` is **reserved** for possible later sugar (lossy
+function / operation), not introduced now to avoid overloading. Witnesses
+are **erased** initially.
+
+```
+Stage 1 (this PR): checker-only Echo type former        ← done
+Stage 2: parser syntax for Echo<A => B> (solo)
+Stage 3: proof-layer residue object (EchoResidue, Coq/Idris)
+Stage 4: optional runtime witness — only if audit/provenance needs
+         observable evidence; modelled as a single residue record,
+         not a whole fiber
+```
+
+## 6. Claim boundary
+
+Hold the narrowed line from `echo-types` retraction **R-2026-05-18**:
+
+> Echo is a **loss-graded reindexing modality over a thin poset**.
+
+Permitted, modest, strong claim:
+
+> Echo models irreversible weakening as a one-way, proof-relevant residue
+> transformation. Linear Echo can weaken to Affine Echo. Affine Echo cannot
+> reconstruct Linear Echo.
+
+**Do not** use (unless a future proof actually justifies it): "graded
+comonad", "universal property", "adjunction", "final/initial semantics",
+"free construction".
+
+## 7. EchoTypes.jl as differential oracle
+
+Phase-2, not a blocker for slice 1. The current Rust tests already mirror
+the `EchoLinear.agda` weakening/no-section theorems at the type-algebra
+level. Once parser syntax or proof-layer residue terms exist, add
+finite-domain differential tests against EchoTypes.jl's `LEcho` / `EchoMode`
+— for semantic examples, **not** core checker soundness.
+
+## Slice 1 scope (PR #86) — exactly
+
+- `EchoMode { Linear, Affine }`
+- `Ty::Echo { mode, domain, codomain }`
+- assignability: `Linear → Affine` only; domain/codomain invariant
+- `Display`
+- five Agda-mirroring tests
+
+No parser, codegen, runtime, or proof-layer changes in this PR.