Commit 0f0fb90
Claude/ci workflow hardening (#33)
* 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 0d55f86 commit 0f0fb90
0 file changed
0 commit comments