Skip to content

Commit f728315

Browse files
Claude/ci workflow hardening (#37)
* feat(types): add Echo types (structured loss) across the pipeline Introduce `Echo<A, B>` — the fibre of a function A → B (a retained witness `x : A` with `f x ≡ y : B`) — and its residue `EchoR<A, B>`, porting the echo-types (Agda) / EchoTypes.jl lineage into Error-Lang as a runnable, stability-aware model of non-total erasure. Pipeline: - Types/Lexer: `Echo`/`EchoR` keywords; `TyEcho`/`TyEchoResidue` typeExpr with sugar (`Echo<A,B>`, `Echo<A>`, bare `Echo`). - Parser: real `parseTypeExpr` (primitives, `Array<T>`, Echo/EchoR, nested `>>` splitting) wired into let annotations, struct fields and function params/return — annotations were previously dropped. - TypeChecker: internal `TyEcho`/`TyEchoR` with conversion, display and unification. Echo and EchoR unify only with their own kind and never with each other, so erasure is irreversible at the type level. Builtins mirror EchoTypes.jl: echo, echo_to_residue, residue_strictly_loses, echo_input (illegal on a residue), echo_output. - Runtime (Bytecode/VM/Codegen): `VEcho{input,output}` single-witness value and `VResidue{output}`; dedicated opcodes. Erasing an Echo to its residue debits stability (a Landauer-style cost; cf. fiber_erasure_bound). - Pretty/LayerNavigator: render the new type forms. - spec/type-system.md: new §7 (Echo Types) plus the [Stab-Erase] rule. - Tests: type-checker, parser and lexer coverage for Echo/EchoR. The core conversion/display/unification logic was compile-verified and behaviourally checked in isolation (the wider compiler/ tree does not build against mainstream ReScript for reasons predating this change). * ci: add timeout-minutes to standalone workflow jobs Addresses the Hypatia workflow-audit `missing_timeout_minutes` findings on the jobs that can carry a job-level timeout: - casket-pages.yml: build (15m), deploy (10m) - codeql.yml: analyze (30m) - hypatia-scan.yml: scan (20m) The reusable-workflow callers (governance.yml, mirror.yml, scorecard.yml) are intentionally left untouched: GitHub does not permit `timeout-minutes` on a job that uses `uses:`. governance.yml's `@main` reference is also left as-is — mirror/scorecard are SHA-pinned but governance is deliberately kept on main by the maintainer. --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 0e44905 commit f728315

0 file changed

File tree

    0 commit comments

    Comments
     (0)