feat(typecheck): QTT quantity semiring — strands are linear in weave - #103
Conversation
`weave` performed no usage checking at all. It built the strand context,
checked the body, computed `Tangle[A,B]` — and discarded it, returning gamma
unchanged. Three unsound programs were accepted in silence:
weave strands a, b into (a > a) yield strands a, b # contraction
weave strands a, b into (a > b) yield strands a, b, a # contraction
weave strands a, b into (a > b) yield strands a # weakening
The spec already forbade the first (`i != j` on [T-Cross-Over]) and the third
("yield declarations match B"). Both side conditions were written down and
never enforced.
## Why a semiring and not "make the language linear"
The requirement is genuinely mixed, so a single discipline is the wrong answer
in both directions:
* braid WORDS are unrestricted (omega) — `x . x` is sigma_1^2, a legitimate
braid. Blanket linearity would reject valid programs.
* STRANDS are linear (1) — a strand is a physical thread. A braid on n
strands is a permutation of those n strands, so strand count is a
conservation law. AFFINE is specifically wrong here: affine permits
discarding, and a strand cannot vanish. That case is what decides it.
* the CLAIM in `Epi[k, rho, tau]` is erased (0) — A-TG-11.1's recorded gap.
`compiler/lib/quantity.ml` provides {0, 1, omega} with add/mul/permits.
Independent uses combine with semiring addition, so two uses of one strand give
1 + 1 = omega, which is not permitted where 1 was declared.
## Applied in BOTH weave forms
Wiring the check into the weave STATEMENT rule alone left `def x = weave ...`
— the idiomatic spelling — entirely unchecked, because it reaches the weave
EXPRESSION rule and never touches the statement rule. The new conformance tier
caught this on its first run.
## Gating
New `conformance/ill-typed/` tier with a DOUBLE assertion: the file must PARSE
and then FAIL to typecheck. Asserting only "the compiler rejects it" is the
failure this suite already had once, when three invalid/ cases scored points
because the command was wrong and failed on every input. Requiring the parse
first proves the rejection came from the typechecker, not from a typo in the
fixture.
Wired into `scripts/check-corpus.sh` (what CI runs) as well as
`run_conformance.sh`, and verified with a negative control: making one
ill-typed fixture well-typed turns the gate red, restoring it turns it green.
`valid/` is now also required to TYPECHECK, not merely parse. All 16 already do.
## Verification
* semiring laws checked EXHAUSTIVELY over all 27 triples — a "semiring"
whose operations don't satisfy the laws is two arbitrary tables, and every
soundness claim resting on it is worth nothing
* 677 compiler tests pass (`dune runtest --force`)
* conformance 23/23; 8/8 examples evaluate; stdlib typechecks
* corpus + RSR gates green
Spec: new section 3.10.1 with the [T-Weave-Linear] rule and the quantity table.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ Approved 2 resolved / 2 findingsAdds QTT quantity semiring enforcing linear strands in weave expressions and statements, accompanied by a new conformance tier. Consider addressing the dead [T-Self-Cross] rule and adding an empty-glob guard to run_conformance.sh.
✅ 2 resolved✅ Quality: Self-crossing rule [T-Self-Cross] is now dead / contradicts spec
✅ Quality: run_conformance.sh ill-typed loop lacks empty-glob guard
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
|
|
…#104) ## The problem Seventeen rules matched a `-> ()` arm in `check`. That is not a partial check — **it is an accept**. A forged node naming `T-Close`, `T-App` or `T-Weave` could conclude *any type at all* and the graph still checked green. The JEG's entire claim is *"evidence, not a log"* — that a derivation can be validated without trusting whoever produced it. Those seventeen arms were the part that made the claim false. ## Why three of them were genuinely underivable `T-App`, `T-Crossing` and `T-Weave` could not be re-derived from the recorded data, because the judgement didn't carry what the rule reads. So the judgement was widened: - **`j_ctx` now holds `env_entry`, not `ty`** — a `T-App` node cannot be checked without the callee's *signature*. - **`j_sigma` (new) holds the strand context** — `T-Crossing`/`T-Weave` read Σ rather than premise types. They were previously bare **leaves**: nodes asserting a type with *nothing* licensing it. The other fourteen were derivable all along and simply hadn't been written. ## Shared rule functions — the JEG now *cannot* drift `infer_binop` was already type-in/type-out. The remaining rules were inline in `infer_expr`, so the JEG would have had to **re-implement** them — and a JEG that re-implements the rules can drift from the typechecker, at which point it certifies a rule the compiler doesn't apply and the evidence is worthless. Extracted 16 (`infer_close`, `infer_mirror`, `infer_echo_eq`, `join_arm_ty`, …) into one definition each, called by **both**. Drift is impossible by construction rather than by discipline. The extraction is behaviour-preserving — every pre-existing test passes unchanged. ## Two rules with real substance - **`T-Let`** checks the conclusion is the *body's* type **and** that the body was checked under the binding the let actually makes. Type-only checking would accept a derivation whose body silently assumed `x` had a more convenient type — there's a test for exactly that forgery. - **`T-Weave`** re-runs the strand **linearity** check from #103, so a graph cannot launder a weave that duplicates or drops a strand. ## The remaining hole is reported, not hidden `T-Add-Block`'s island has its own judgement (⊢_hd). Rather than a silent accept it's **recorded** — new `unchecked : derivation -> (string * judgement) list`. So *"check succeeded"* and *"check succeeded **and re-derived every node**"* are now distinguishable results, and `--derive` says which: ``` == c == (3 nodes, depth 3, every node re-derived) [T-Close] |- close(mirror(w)) : Tangle[I, I] [T-Mirror] |- mirror(w) : Word[3] [T-Var] w:Word[3] |- w : Word[3] ``` ## Verification - JEG suite **19 → 51 tests**, structured as an honest/forged **pair** per rule closed — so each test's forged half is a case that **would have passed before** - **709 compiler tests** pass (`dune runtest --force`) - conformance 23/23; corpus + RSR gates green Follows #103 (merged). `feat/jeg-complete` on origin is a superseded pre-rebase copy of this branch — safe to delete. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
1 participant
The gap
weavedid no usage checking at all. It built the strand context, checked the body, computedTangle[A,B]— and discarded it, returninggammaunchanged. Three unsound programs were accepted in silence:The spec already forbade the first (
i ≠ jon[T-Cross-Over]) and the third ("yield declarations match B"). Both side conditions were written down and never enforced.Why a semiring, not "make the language linear"
The requirement is genuinely mixed, so a single discipline is wrong in both directions:
ωx . xis σ₁² — a legitimate braid. Blanket linearity would reject valid programs.1Epi[κ,ρ,τ]0Linear, not affine — and the vanishing-strand case is what decides it. Affine permits discarding; a strand cannot vanish. That is the distinguishing test, and
test_quantity.mlasserts it by name.compiler/lib/quantity.mlgives {0, 1, ω} withadd/mul/permits. Independent uses combine with semiring addition, so two uses of one strand give1 + 1 = ω, which is not permitted where1was declared.Applied in BOTH weave forms
Wiring the check into the weave statement rule alone left
def x = weave …— the idiomatic spelling — entirely unchecked, because it reaches the weave expression rule and never touches the statement rule. The new conformance tier caught this on its first run, which is the argument for the tier existing.Gating
New
conformance/ill-typed/tier carrying a double assertion: the file must parse, and must then fail to typecheck.Asserting only "the compiler rejects it" is precisely the failure this suite already had once — three
invalid/cases scored points because the runner command was wrong and failed on every input. Requiring the parse first proves the rejection came from the typechecker and not from a typo in the fixture.Wired into
scripts/check-corpus.sh(what CI actually runs) as well asrun_conformance.sh.valid/is now also required to typecheck, not merely parse — all 16 already do.Negative control run: making one ill-typed fixture well-typed turns the gate red with the right error; restoring it turns it green. The gate is not decorative.
Verification
dune runtest --force)lib/stdlib.tangletypechecksSpec
New §3.10.1 with the
[T-Weave-Linear]rule, the quantity table, the rejected-programs table, and an explicit scope note: this is the semiring applied to strands. The core judgement is stillΓ ⊢ e : τ— a fullΓ ⊢ e :^q τchanges the judgement shape and needs the metatheory re-proved, tracked separately.🤖 Generated with Claude Code