feat(check): make Echo types operational — typing rules for echo operations by hyperpolymath · Pull Request #56 · hyperpolymath/betlang

hyperpolymath · 2026-06-03T17:56:00Z

Summary

Echo types were inert type formers: bet-check's unifier handled Echo T / EchoR T (distinct from T, structural recursion, distinct from each other), but no expression could introduce or eliminate one. The design doc listed all the operations as "deferred".

This integrates the structured-loss operations into the type system as genuinely polymorphic builtins, each instantiated with a fresh carrier variable per use site:

Operation	Typing rule	Role
`echo`	`'a -> Echo 'a`	introduction (`echo-intro`, unary collapse of the fibre core)
`echo_output`	`Echo 'a -> 'a`	explicit projection to the base value (never an implicit coercion)
`echo_to_residue`	`Echo 'a -> EchoR 'a`	lower a full echo to its strict, non-recoverable residue
`sample_echo`	`Dist 'a -> Echo 'a`	probabilistic-support bridge: retains the residue `sample` discards

Wired through Expr::Var so lexical bindings shadow the builtins. Surface syntax is ordinary application (echo(x)), so no grammar change was needed.

Design fidelity

Types-only / ghost. Echo T / EchoR T still erase to T at runtime — no residue payload is materialised, matching docs/echo-types.adoc §"Runtime representation strategy". No runtime/effect commitment.
Distinctness preserved. Enforced through the operations as well as the formers — echo_output on a bare carrier is rejected. No implicit Echo T -> T.
Canonical names mirror hyperpolymath/echo-types (source of truth) and EchoTypes.jl.
Deliberately not added: echo_input (coincides with echo_output for the unary former), residue_strictly_loses (a propositional witness, not a term), bet_echo (needs ternary surface form).

Verification

34/34 bet-check tests pass (27 baseline + 7 new: intro, explicit projection, residue lowering, sample_echo bridge + composition, polymorphic reuse, bare-carrier rejection, shadowing).
tools/proof-scan.sh clean — no banned soundness escape hatches.
New library code is clippy-clean.

Formal-proof follow-up

Lean keeps echo/echoR as type formers only, so Progress/Preservation remain intact. Mirroring the operation typing rules in Lean (and re-establishing the metatheory) is registered as obligation TP-5 in PROOF-NEEDS.md / PROOF-STATUS.md, deferred until the runtime residue representation is settled.

Files

compiler/bet-check/src/lib.rs — echo_builtin_type + Expr::Var wiring + tests
docs/echo-types.adoc — new "Operations (typing rules)" section; narrowed deferral list
README.adoc — Echo Types section updated
PROOF-NEEDS.md / PROOF-STATUS.md — TP-5 registered
proofs/BetLang.lean — comment-only pointer to the landed rules + TP-5

https://claude.ai/code/session_01QGi8GND5yNWgDyfReVEPYs

Generated by Claude Code

…ations Echo/EchoR were inert type formers: the unifier already handled them (distinct from T, structural recursion, distinct from each other) but no expression could introduce or eliminate one. This integrates the structured-loss operations into the type system as genuinely polymorphic builtins in bet-check, each instantiated with a fresh carrier variable per use site: echo : 'a -> Echo 'a (introduction; echo-intro) echo_output : Echo 'a -> 'a (explicit projection; no implicit coercion) echo_to_residue : Echo 'a -> EchoR 'a (strict residue lowering) sample_echo : Dist 'a -> Echo 'a (probabilistic-support bridge) Wired through Expr::Var so lexical bindings shadow the builtins; surface syntax is ordinary application, so no grammar change is needed. Stays types-only / ghost — Echo/EchoR still erase to T at runtime, matching the existing design in docs/echo-types.adoc. 7 new tests (intro, explicit projection, residue lowering, sample_echo bridge + composition, polymorphic reuse at Int and String, bare-carrier rejection, shadowing); 34/34 bet-check tests pass; proof-scan clean. Docs: echo-types.adoc gains an "Operations (typing rules)" section and the deferred list is narrowed; README Echo Types section updated. Lean keeps echo/echoR as type formers only (Progress/Preservation intact) — the mechanised mirror for the echo operations is registered as obligation TP-5 in PROOF-NEEDS.md / PROOF-STATUS.md. https://claude.ai/code/session_01QGi8GND5yNWgDyfReVEPYs

github-actions · 2026-06-03T17:57:01Z

🔍 Hypatia Security Scan

Findings: 64 issues detected

Severity	Count
🔴 Critical	8
🟠 High	15
🟡 Medium	41

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "missing_timeout_minutes",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "missing_timeout_minutes",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "missing_timeout_minutes",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "missing_timeout_minutes",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_timeout_minutes",
    "file": "secret-scanner.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in spark-theatre-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "spark-theatre-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "scorecard_publish_with_run_step",
    "file": "scorecard-enforcer.yml",
    "action": "split_scorecard_publish_job",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "codeql_missing_actions_language",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/ternary.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Widens the echo-type integration from the four base operations to the full functor + comonad surface that echo-types proves upstream: echo_map : ('a -> 'b) -> Echo 'a -> Echo 'b (functor / map-over) echo_duplicate : Echo 'a -> Echo (Echo 'a) (comultiplication) echo_output : Echo 'a -> 'a (now documented as counit) This is the ungraded, ghost shadow of EchoGradedComonad.agda (gextract / gduplicate / coassoc): bet-check carries the typing; the laws live in the Agda (mirrored for Lean as obligation TP-5). Also pins the type-level bridge from the core primitive — echo(bet a b c) : Echo T already type-checks, so the type story needs no new primitive (runtime bet_echo branch-tag retention stays deferred). +4 tests (functor, duplicate, extract-after-duplicate typing, bet bridge); 38/38 bet-check tests pass; proof-scan clean. Docs (echo-types.adoc, README), the Lean pointer comment, and TP-5 updated to cover the comonad surface. https://claude.ai/code/session_01QGi8GND5yNWgDyfReVEPYs

github-actions · 2026-06-03T18:22:55Z

🔍 Hypatia Security Scan

Findings: 64 issues detected

Severity	Count
🔴 Critical	8
🟠 High	15
🟡 Medium	41

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "missing_timeout_minutes",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "missing_timeout_minutes",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "missing_timeout_minutes",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "missing_timeout_minutes",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_timeout_minutes",
    "file": "secret-scanner.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in spark-theatre-gate.yml",
    "type": "missing_timeout_minutes",
    "file": "spark-theatre-gate.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "scorecard_publish_with_run_step",
    "file": "scorecard-enforcer.yml",
    "action": "split_scorecard_publish_job",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "codeql_missing_actions_language",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/ternary.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…ng (#60) ## betlang reference-pass (estate reconciliation + hygiene) — increment 1 Part of the estate-wide reconciliation/hygiene checkpoint, with **betlang as the reference repo**. ### Branch reconciliation → one clean `main` - `estate-standardization-20260607` is **fully merged into `main`** (`main..branch` is empty; the branch tip is the merge-base). Nothing unmerged to lose. - Deleting it is **blocked in this environment** (git proxy returns `HTTP 403` on `push --delete`; no MCP delete-branch tool). → recorded as an **owner UI action**. After it's gone, `main` is the sole branch. ### Metadata currency (`.machine_readable/6a2/`) - **STATE.a2ml**: reflects PR #56 — echo operations are now *typed* (the functor/comonad surface: `echo`, `echo_output`, `echo_map`, `echo_duplicate`, `echo_to_residue`, `sample_echo`). M5/M6 marked done (type-level); stale "echo operations deferred" blocker removed; next-actions refreshed (harden checker, TP-5, `bet_echo` runtime); maintenance notes 38 bet-check tests. - **META.a2ml / ECOSYSTEM.a2ml**: drop the standards-**banned** `PMPL-1.0` token in descriptive metadata → `Palimpsest License (SPDX: MPL-2.0)`. (betlang's actual SPDX headers + root `LICENSE` were already correct MPL-2.0.) ### ⚠️ Flagged for the owner (cannot verify from here — out of MCP scope) `Causals.jl` and `BowtieRisk.jl` both ship `LICENSES/PMPL-1.0-or-later.txt` (the *banned* identifier) while declaring MPL-2.0 canonical. Two freshly-templated repos with the identical artifact strongly implies **`rsr-template-repo` still ships the banned license file** — please check the template + `standards`. ### Still to come on this branch (betlang reference pass) CI-health-at-root verification, issues for tracked proof/tech-debt, `bot_directives/` (greenfield format — needs a schema decision), and the repo wiki (currently none). https://claude.ai/code/session_01QGi8GND5yNWgDyfReVEPYs --- _Generated by [Claude Code](https://claude.ai/code/session_01QGi8GND5yNWgDyfReVEPYs)_ --------- Co-authored-by: Claude <noreply@anthropic.com>

hyperpolymath marked this pull request as ready for review June 3, 2026 19:57

hyperpolymath merged commit 3ac22ca into main Jun 3, 2026
33 checks passed

hyperpolymath deleted the claude/sharp-heisenberg-2ZsZv branch June 3, 2026 19:58

hyperpolymath mentioned this pull request Jun 13, 2026

chore(estate): betlang reconciliation + 6a2 currency + license branding #60

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(check): make Echo types operational — typing rules for echo operations#56

feat(check): make Echo types operational — typing rules for echo operations#56
hyperpolymath merged 2 commits into
mainfrom
claude/sharp-heisenberg-2ZsZv

hyperpolymath commented Jun 3, 2026

Uh oh!

github-actions Bot commented Jun 3, 2026

Uh oh!

github-actions Bot commented Jun 3, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

hyperpolymath commented Jun 3, 2026

Summary

Design fidelity

Verification

Formal-proof follow-up

Files

Uh oh!

github-actions Bot commented Jun 3, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 3, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants