feat(types): accommodate Echo types (structured loss) in the type checker

Add the `Echo T` / `EchoR T` type formers from hyperpolymath/echo-types
across betlang's type-system surfaces. `Echo T` is a distinct,
proof-relevant structured-loss residue over `T`; `EchoR T` is its strict,
non-recoverable weakening (reserved — operations deferred).

Design (per maintainer direction):
- Distinct from the carrier: unify(Echo T, T) and unify(Echo T, EchoR T)
  both fail; no implicit forgetting Echo T -> T.
- Domain-agnostic in core; the canonical betlang introduction site is
  probabilistic-support retention (a future `sample_echo : Dist T -> Echo T`
  keeps the draw/branch residue that `sample` marginalises away).
- Ghost/proof-relevant residue: erases to T's representation at runtime;
  no runtime payload yet.

Surfaces:
- compiler/bet-core/src/types.rs: Type::Echo / Type::EchoR variants.
- compiler/bet-check/src/lib.rs: lower `Echo T`/`EchoR T` (type
  applications) in ast_type_to_core; structural resolve/unify; distinctness
  via the mismatch fallthrough. Adds 5 unit tests (lowering, distinctness,
  structural unification, Echo != EchoR, inference recursion) and fixes the
  test module's missing `Symbol` import (tests never compiled under
  `cargo check`). `cargo test -p bet-check`: 27 passed.
- proofs/BetLang.lean: Ty.echo / Ty.echoR formers (no Expr/HasType use, so
  Progress/Preservation are unaffected).
- spec/SPEC.core.scm + spec/grammar.ebnf: echo-types semantics entry and
  grammar note.
- docs/echo-types.adoc: design + deferred-work writeup.

https://claude.ai/code/session_01NGKc4681nuptfQADqreAfc

Author: claude

compiler/bet-check/src/lib.rs

@@ -107,6 +107,8 @@ impl CheckEnv {
             Type::Tuple(elems) => {
                 Type::Tuple(elems.iter().map(|e| self.resolve(e)).collect())
             }
+            Type::Echo(inner) => Type::Echo(Box::new(self.resolve(inner))),
+            Type::EchoR(inner) => Type::EchoR(Box::new(self.resolve(inner))),
             _ => ty.clone(),
         }
     }
@@ -161,6 +163,15 @@ impl CheckEnv {
                 }
                 Ok(())
             }
+            // Echo/EchoR unify only structurally with their own former — never
+            // with the bare carrier `T`, nor with each other. This keeps the
+            // "retained loss" distinction: `Echo T` is not `T` with decoration.
+            (Type::Echo(a_inner), Type::Echo(b_inner)) => {
+                self.unify(a_inner, b_inner, span)
+            }
+            (Type::EchoR(a_inner), Type::EchoR(b_inner)) => {
+                self.unify(a_inner, b_inner, span)
+            }
 
             _ => Err(CompileError::TypeMismatch {
                 expected: format!("{:?}", a),
@@ -887,6 +898,12 @@ fn ast_type_to_core(ty: &bet_syntax::ast::Type) -> Type {
                 "Dist" if args.len() == 1 => {
                     Type::Dist(Box::new(ast_type_to_core(&args[0].node)))
                 }
+                "Echo" if args.len() == 1 => {
+                    Type::Echo(Box::new(ast_type_to_core(&args[0].node)))
+                }
+                "EchoR" if args.len() == 1 => {
+                    Type::EchoR(Box::new(ast_type_to_core(&args[0].node)))
+                }
                 _ => Type::Named(base_name),
             }
         }
@@ -907,6 +924,9 @@ fn ast_type_to_core(ty: &bet_syntax::ast::Type) -> Type {
 #[cfg(test)]
 mod tests {
     use super::*;
+    // `Symbol` is re-exported at the bet_syntax crate root (not via
+    // `bet_syntax::ast::*`), so import it explicitly for the tests.
+    use bet_syntax::Symbol;
 
     /// Helper: create a dummy-spanned expression.
     fn dummy(expr: Expr) -> Spanned<Expr> {
@@ -1152,4 +1172,81 @@ mod tests {
         let result = check_expr(&dummy(par), &mut env).expect("TODO: handle error");
         assert_eq!(result, Type::List(Box::new(Type::Float)));
     }
+
+    // ---- Echo types (structured loss; see hyperpolymath/echo-types) ----
+
+    /// `Echo T` / `EchoR T` surface syntax (parsed as a type application)
+    /// lowers to the dedicated semantic formers.
+    #[test]
+    fn test_echo_lowering() {
+        use bet_syntax::ast::Type as AstType;
+        let app = |name: &str, arg: AstType| {
+            AstType::App(
+                Box::new(Spanned::dummy(AstType::Named(Symbol::intern(name)))),
+                vec![Spanned::dummy(arg)],
+            )
+        };
+        assert_eq!(
+            ast_type_to_core(&app("Echo", AstType::Named(Symbol::intern("Int")))),
+            Type::Echo(Box::new(Type::Int))
+        );
+        assert_eq!(
+            ast_type_to_core(&app("EchoR", AstType::Named(Symbol::intern("Float")))),
+            Type::EchoR(Box::new(Type::Float))
+        );
+    }
+
+    /// `Echo T` is distinct from `T`: no implicit forgetting in either
+    /// direction. This is the load-bearing invariant — if it unified with the
+    /// carrier the checker would lose the entire point of retained loss.
+    #[test]
+    fn test_echo_distinct_from_carrier() {
+        let mut env = CheckEnv::new();
+        assert!(env.unify(&Type::Echo(Box::new(Type::Int)), &Type::Int, None).is_err());
+        assert!(env.unify(&Type::Int, &Type::Echo(Box::new(Type::Int)), None).is_err());
+    }
+
+    /// `Echo T` unifies structurally with `Echo T'` iff `T` unifies with `T'`.
+    #[test]
+    fn test_echo_unifies_structurally() {
+        let mut env = CheckEnv::new();
+        env.unify(
+            &Type::Echo(Box::new(Type::Int)),
+            &Type::Echo(Box::new(Type::Int)),
+            None,
+        )
+        .expect("Echo Int should unify with Echo Int");
+        assert!(env
+            .unify(
+                &Type::Echo(Box::new(Type::Int)),
+                &Type::Echo(Box::new(Type::String)),
+                None
+            )
+            .is_err());
+    }
+
+    /// `Echo T` and `EchoR T` are distinct formers (the residue is a strict
+    /// weakening, not interchangeable with the full echo).
+    #[test]
+    fn test_echo_vs_residue_distinct() {
+        let mut env = CheckEnv::new();
+        assert!(env
+            .unify(
+                &Type::Echo(Box::new(Type::Int)),
+                &Type::EchoR(Box::new(Type::Int)),
+                None
+            )
+            .is_err());
+    }
+
+    /// Unification recurses through the Echo former, so an inference variable
+    /// inside an `Echo` is solved.
+    #[test]
+    fn test_echo_inference_var_recurses() {
+        let mut env = CheckEnv::new();
+        let a = env.fresh_var();
+        env.unify(&Type::Echo(Box::new(a.clone())), &Type::Echo(Box::new(Type::Int)), None)
+            .expect("Echo 'a should unify with Echo Int");
+        assert_eq!(env.resolve(&Type::Echo(Box::new(a))), Type::Echo(Box::new(Type::Int)));
+    }
 }

compiler/bet-core/src/types.rs

@@ -34,6 +34,18 @@ pub enum Type {
     Option(Box<Type>),
     /// Result type
     Result(Box<Type>, Box<Type>),
+    /// Echo type: `Echo T` — a proof-relevant *structured-loss* residue over
+    /// values of type `T` (after `hyperpolymath/echo-types`). Distinct from
+    /// `T`: no implicit forgetting `Echo T -> T`. Domain-agnostic in core; its
+    /// canonical betlang introduction site is probabilistic support retention
+    /// (a draw/branch is marginalised into `T`, while the echo keeps that
+    /// residue statically). The residue is ghost/proof-relevant — erased at
+    /// runtime for now.
+    Echo(Box<Type>),
+    /// Echo residue: `EchoR T` — the strict, non-recoverable weakening of
+    /// `Echo T` (no recovery operation is promised). Reserved former; rich
+    /// operations are deferred until the residue semantics are settled.
+    EchoR(Box<Type>),
     /// Type variable (for inference)
     Var(u32),
     /// Named type

docs/echo-types.adoc

@@ -0,0 +1,100 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+// @taxonomy: docs/echo-types
+= Echo Types in BetLang
+:toc:
+
+Integration of *Echo Types* — a first-class notion of **structured loss**
+(loss that is not total erasure) — into BetLang's type system. Upstream:
+https://github.com/hyperpolymath/echo-types[`echo-types`] (Agda, source of
+truth) and https://github.com/hyperpolymath/EchoTypes.jl[`EchoTypes.jl`]
+(executable finite-domain companion).
+
+== Concept
+
+Given `f : A → B`, the echo at `y : B` is the fibre
+`Echo f y := Σ (x : A), (f x ≡ y)` — a *proof-relevant residue* recording
+what was lost when `f` collapsed `x` to `y`. The honest post-retraction
+core is the Echo functor (`echo-intro`, `map-over`) plus the **residue**
+weakening `EchoR` (a strict, non-recoverable lowering).
+
+BetLang is non-dependent, so it does not represent the literal fibre.
+Instead it adds two **unary type formers**:
+
+[cols="1,4"]
+|===
+| Former | Meaning
+
+| `Echo T`
+| A `T`-value carrying a proof-relevant residue of retained loss
+  (potentially recoverability-bearing). *Distinct from `T`.*
+
+| `EchoR T`
+| The strict, non-recoverable residue/retraction of `Echo T`. Reserved
+  former; rich operations deferred.
+|===
+
+== Design decisions (this pass)
+
+. **Distinctness.** `Echo T` is *not* `T`. `unify(Echo T, T)` fails, as
+  does `unify(Echo T, EchoR T)`. There is no implicit forgetting
+  `Echo T → T`; introduction and projection are explicit. If `Echo T`
+  unified with `T`, the checker would lose the entire point of retained
+  loss.
+. **Domain-agnostic core, probabilistic-support bridge.** `Echo` is the
+  general structured-loss former. Its *canonical betlang introduction
+  site* is probabilistic support retention — but that is the bridge, not
+  the definition (so future structured-loss uses are not foreclosed).
++
+[source]
+----
+sample      : Dist T -> T        // marginalises away which draw/branch fired
+sample_echo : Dist T -> Echo T   // retains that residue   (DEFERRED)
+----
+. **Ghost / erased residue.** The residue is proof-relevant; at runtime
+  `Echo T` (and `EchoR T`) erase to `T`'s representation. No runtime
+  payload is added until operations demand it — avoiding premature
+  commitment to a representation of branch histories, support traces,
+  seeds, or likelihood paths.
+
+== Where it lives
+
+[cols="1,3"]
+|===
+| Surface | Change
+
+| `compiler/bet-core/src/types.rs`
+| `Type::Echo(Box<Type>)`, `Type::EchoR(Box<Type>)`.
+
+| `compiler/bet-check/src/lib.rs`
+| Lowering `Echo T` / `EchoR T` (parsed as type applications) in
+  `ast_type_to_core`; structural `resolve`/`unify`; distinctness enforced
+  by the existing mismatch fallthrough. Unit tests cover lowering,
+  distinctness, structural unification, `Echo`≠`EchoR`, and inference
+  recursion.
+
+| `proofs/BetLang.lean`
+| `Ty.echo`, `Ty.echoR` constructors. Type *formers* only — no `Expr`
+  introduces/eliminates them and `HasType` assigns no expression an echo
+  type, so Progress/Preservation are unaffected.
+
+| `spec/SPEC.core.scm`, `spec/grammar.ebnf`
+| `echo-types` semantics entry (incl. the canonical statement) and a
+  grammar note. `Echo T` already parses as an application type.
+|===
+
+== Deferred (next passes)
+
+* Introduction/elimination forms: `echo_intro : T -> Echo T`,
+  `proj₁ : Echo T -> T`, `echo_to_residue : Echo T -> EchoR T`.
+* The residue-retaining `sample_echo` / `bet_echo` operations and their
+  typing rules.
+* Lean typing rules + metatheory for the echo operations once the runtime
+  residue representation is settled.
+* Runtime residue payload (only when an operation requires it).
+
+== References
+
+* `proofs/agda/Echo.agda`, `EchoResidue.agda`,
+  `EchoProbabilisticSupport.agda` (upstream echo-types).
+* `EchoTypes.jl` — the finite-domain executable shadow.

proofs/BetLang.lean

@@ -31,6 +31,16 @@ inductive Ty : Type where
   | unit   : Ty
   | arrow  : Ty → Ty → Ty
   | dist   : Ty → Ty
+  -- Echo types (structured loss; see `hyperpolymath/echo-types`). `echo T` is
+  -- a proof-relevant retained-loss residue over `T`, distinct from `T`;
+  -- `echoR T` is its strict, non-recoverable weakening. These are type
+  -- *formers* only at this stage: no `Expr` constructor introduces or
+  -- eliminates them and `HasType` assigns no expression an echo type, so the
+  -- carrier's metatheory (Progress/Preservation below) is unaffected. The
+  -- canonical betlang introduction site (probabilistic-support retention,
+  -- `Dist T → echo T`) and its typing rules are deferred to a later pass.
+  | echo   : Ty → Ty
+  | echoR  : Ty → Ty
   deriving DecidableEq, Repr
 
 /-- BetLang core expressions using de Bruijn indices. -/

spec/SPEC.core.scm

@@ -131,6 +131,35 @@
             "Debugging stochastic behavior"
             "Conformance testing"))))
 
+    ;;=========================================================================
+    ;; TYPE SYSTEM EXTENSION: echo types (structured loss)
+    ;;=========================================================================
+    (echo-types
+     . ((origin . "hyperpolymath/echo-types (Agda, source of truth); EchoTypes.jl (executable companion)")
+        (canonical-statement
+         . "Echo T is a distinct proof-relevant structured-loss type whose first canonical betlang introduction form is probabilistic support retention: sampling or betting may erase branch/draw information into T, while the echo form retains that residue statically.")
+
+        (formers
+         . ((Echo  . ((arity . 1)
+                      (meaning . "Echo T : a T-value carrying a proof-relevant residue of retained loss; potentially recoverability-bearing")
+                      (surface-syntax . "Echo T  (parsed as a type application, like `Dist T`)")))
+            (EchoR . ((arity . 1)
+                      (meaning . "EchoR T : the strict, non-recoverable residue/retraction of Echo T; no recovery operation is promised")
+                      (status . "reserved former; rich operations deferred")))))
+
+        (typing-rules
+         . ((distinctness . "Echo T is NOT T: unify(Echo T, T) fails and unify(Echo T, EchoR T) fails. No implicit forgetting Echo T -> T.")
+            (structural . "Echo T ~ Echo T' iff T ~ T'; likewise EchoR T ~ EchoR T'.")
+            (domain-agnostic . "Echo is the general structured-loss former in core; the probabilistic-support bridge is its canonical betlang integration, not its definition.")))
+
+        (canonical-bridge
+         . ((sample . "sample : Dist T -> T   (marginalises away which draw/branch produced the value)")
+            (echo-companion . "sample_echo / bet_echo : Dist T -> Echo T   (retains that residue) -- DEFERRED")))
+
+        (runtime . "Residue is ghost / proof-relevant: Echo T and EchoR T erase to T's representation in codegen for now (no runtime payload until operations demand it).")
+
+        (mechanisation . "Type formers Ty.echo / Ty.echoR in proofs/BetLang.lean; Type::Echo / Type::EchoR in compiler/bet-core/src/types.rs; lowered + unified (distinctly) in compiler/bet-check.")))
+
     ;;=========================================================================
     ;; TESTING REQUIREMENTS
     ;;=========================================================================

spec/grammar.ebnf

@@ -210,6 +210,10 @@ type = arrow_type;
 arrow_type = application_type, [ "->", arrow_type ];
 
 application_type = atom_type, { atom_type };
+(* Recognised built-in type constructors are written as applications, e.g.
+   `Dist T`, `List T`, `Echo T`, `EchoR T`. `Echo T` / `EchoR T` are the
+   structured-loss formers (see SPEC.core.scm > echo-types); `Echo T` is a
+   distinct type from `T`. *)
 
 atom_type = named_type
           | type_variable