feat(echo): integrate echo + product types into the OCaml typechecker

Mirrors the Lean spec (proofs/Tangle.lean) into the OCaml checker so echo
types are a feature of the actual typechecker, not only the metatheory.

- typecheck.ml: `ty` gains `TProd of ty*ty` and `TEcho of ty*ty`; `pp_ty` is
  now `let rec` and prints them; `infer_expr` gains the eight typing rules
  [T-Echo-Close]/[T-Lower]/[T-Residue]/[T-Pair]/[T-Fst]/[T-Snd]/[T-Echo-Add]/
  [T-Echo-Eq], matching the HasType rules.
- ast.ml: `expr` gains EchoClose/Lower/Residue/Pair/Fst/Snd/EchoAdd/EchoEq.
- pretty.ml: pp_expr prints the new forms (kept exhaustive).
- eval.ml: eval_expr gets an explicit "not yet implemented" arm for the echo
  forms (runtime evaluation is a scoped follow-on; the typechecker is the
  deliverable). Stays exhaustive.

Scope: the typechecker. Surface parser syntax + runtime eval are follow-ons.

NOTE: no OCaml toolchain or OCaml CI exists in this environment, so this was
NOT compiled here — it is a careful by-hand integration (exhaustiveness audited
via the Ast-only `Twist` probe: pretty/eval/typecheck are the only exhaustive
Ast.expr matchers; compositional's of_ast_expr has a catch-all; repl matches no
expr). Verify with `dune build` in compiler/.

https://claude.ai/code/session_01PgHpCFzwYB7Qy9L6kmR8CE

Author: claude

compiler/lib/ast.ml

@@ -80,6 +80,18 @@ and expr =
   | Cup       of expr * expr
   | Twist     of expr
 
+  (* ---- Echo types (structured loss) — mirror the Lean spec in
+   *      proofs/Tangle.lean (Ty.echo / Ty.prod and the echo operations).
+   *      Typed by typecheck.ml; surface parser syntax is a follow-on. ---- *)
+  | EchoClose of expr                 (* echo-preserving closure (residue-retaining close) *)
+  | Lower     of expr                 (* project an echo to its result *)
+  | Residue   of expr                 (* project an echo to its residue (recover witness) *)
+  | Pair      of expr * expr          (* product introduction *)
+  | Fst       of expr                 (* first projection *)
+  | Snd       of expr                 (* second projection *)
+  | EchoAdd   of expr * expr          (* echo-preserving addition (residue = summand pair) *)
+  | EchoEq    of expr * expr          (* echo-preserving equality (residue = operand pair) *)
+
   (* ---- Literals ---- *)
   | BraidLit  of generator list
   | Identity

compiler/lib/eval.ml

@@ -429,6 +429,14 @@ let rec eval_expr (env : env) (e : expr) : value =
     in
     try_arms arms
 
+  (* ---- Echo types (structured loss) ----
+   * These are typed by typecheck.ml (mirroring proofs/Tangle.lean).  Runtime
+   * evaluation needs echo/product value forms and is a deliberate follow-on;
+   * the typechecker is the scoped deliverable. *)
+  | EchoClose _ | Lower _ | Residue _ | Pair _ | Fst _ | Snd _ | EchoAdd _ | EchoEq _ ->
+    eval_error "echo-type evaluation is not yet implemented (typecheck-only); \
+                see proofs/Tangle.lean for the intended small-step semantics"
+
 (** Evaluate a binary operation on two values. *)
 and eval_binop (op : binop) (v1 : value) (v2 : value) : value =
   match op with

compiler/lib/pretty.ml

@@ -171,6 +171,52 @@ let rec pp_expr ctx = function
     pp_expr ctx e;
     emit ctx ")"
 
+  | EchoClose e ->
+    emit ctx "echoClose(";
+    pp_expr ctx e;
+    emit ctx ")"
+
+  | Lower e ->
+    emit ctx "lower(";
+    pp_expr ctx e;
+    emit ctx ")"
+
+  | Residue e ->
+    emit ctx "residue(";
+    pp_expr ctx e;
+    emit ctx ")"
+
+  | Pair (e1, e2) ->
+    emit ctx "pair(";
+    pp_expr ctx e1;
+    emit ctx ", ";
+    pp_expr ctx e2;
+    emit ctx ")"
+
+  | Fst e ->
+    emit ctx "fst(";
+    pp_expr ctx e;
+    emit ctx ")"
+
+  | Snd e ->
+    emit ctx "snd(";
+    pp_expr ctx e;
+    emit ctx ")"
+
+  | EchoAdd (e1, e2) ->
+    emit ctx "echoAdd(";
+    pp_expr ctx e1;
+    emit ctx ", ";
+    pp_expr ctx e2;
+    emit ctx ")"
+
+  | EchoEq (e1, e2) ->
+    emit ctx "echoEq(";
+    pp_expr ctx e1;
+    emit ctx ", ";
+    pp_expr ctx e2;
+    emit ctx ")"
+
   | BraidLit gens ->
     emit ctx "braid[";
     List.iteri (fun i g ->

compiler/lib/typecheck.ml

@@ -41,6 +41,9 @@ type ty =
   | TNum                            (** Num — integers and floats *)
   | TBool                           (** Bool — booleans *)
   | TStr                            (** Str — strings *)
+  | TProd   of ty * ty              (** ρ × σ — product / residue carrier for lossy ops *)
+  | TEcho   of ty * ty              (** Echo[ρ, τ] — structured loss: residue ρ, result τ.
+                                        Mirrors Ty.echo in proofs/Tangle.lean. *)
 
 (** Function signature: (param_types) -> return_type. *)
 type fun_sig = {
@@ -89,12 +92,14 @@ let pp_boundary (b : boundary) : string =
     "[" ^ String.concat ", " (List.map pp_strand_type b) ^ "]"
 
 (** Pretty-print a type. *)
-let pp_ty = function
+let rec pp_ty = function
   | TWord n        -> Printf.sprintf "Word[%d]" n
   | TTangle (a, b) -> Printf.sprintf "Tangle[%s, %s]" (pp_boundary a) (pp_boundary b)
   | TNum           -> "Num"
   | TBool          -> "Bool"
   | TStr           -> "Str"
+  | TProd (a, b)   -> Printf.sprintf "(%s * %s)" (pp_ty a) (pp_ty b)
+  | TEcho (r, t)   -> Printf.sprintf "Echo[%s, %s]" (pp_ty r) (pp_ty t)
 
 (* ================================================================== *)
 (*  Environment operations                                             *)
@@ -373,6 +378,66 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty =
     ) arm_types;
     result_ty
 
+  (* ---- Echo types (structured loss) ----
+   * Mirror the HasType rules in proofs/Tangle.lean:
+   *   [T-Echo-Close] echoClose e : Echo[Word[n], Word[0]]   when e : Word[n]
+   *   [T-Lower]      lower e      : τ                        when e : Echo[ρ, τ]
+   *   [T-Residue]    residue e    : ρ                        when e : Echo[ρ, τ]
+   *   [T-Pair]/[T-Fst]/[T-Snd]    product intro + projections
+   *   [T-Echo-Add]   echoAdd a b  : Echo[Num × Num, Num]
+   *   [T-Echo-Eq]    echoEq a b   : Echo[ρ × ρ, Bool]        for ρ ∈ {Num, Str, Word[n]}
+   *)
+  | EchoClose e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TWord n -> TEcho (TWord n, TWord 0)
+    | t -> type_error "echoClose requires Word[n], got %s" (pp_ty t)
+    end
+
+  | Lower e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TEcho (_, t) -> t
+    | t -> type_error "lower requires Echo[_, _], got %s" (pp_ty t)
+    end
+
+  | Residue e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TEcho (r, _) -> r
+    | t -> type_error "residue requires Echo[_, _], got %s" (pp_ty t)
+    end
+
+  | Pair (e1, e2) ->
+    let t1 = infer_expr gamma sigma e1 in
+    let t2 = infer_expr gamma sigma e2 in
+    TProd (t1, t2)
+
+  | Fst e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TProd (a, _) -> a
+    | t -> type_error "fst requires a product, got %s" (pp_ty t)
+    end
+
+  | Snd e1 ->
+    begin match infer_expr gamma sigma e1 with
+    | TProd (_, b) -> b
+    | t -> type_error "snd requires a product, got %s" (pp_ty t)
+    end
+
+  | EchoAdd (e1, e2) ->
+    begin match infer_expr gamma sigma e1, infer_expr gamma sigma e2 with
+    | TNum, TNum -> TEcho (TProd (TNum, TNum), TNum)
+    | t1, t2 -> type_error "echoAdd requires Num, Num, got %s, %s" (pp_ty t1) (pp_ty t2)
+    end
+
+  | EchoEq (e1, e2) ->
+    begin match infer_expr gamma sigma e1, infer_expr gamma sigma e2 with
+    | TNum, TNum -> TEcho (TProd (TNum, TNum), TBool)
+    | TStr, TStr -> TEcho (TProd (TStr, TStr), TBool)
+    | TWord n, TWord m when n = m -> TEcho (TProd (TWord n, TWord n), TBool)
+    | t1, t2 ->
+      type_error "echoEq requires matching Num/Str/Word[n] operands, got %s, %s"
+        (pp_ty t1) (pp_ty t2)
+    end
+
 (** Infer the type of a binary operation given operand types.
  *  Implements rules from sections 3.4, 3.5, 3.6.
  *)