A cross-engine language-design decision, in the same shape as #50. It cannot be made in OCaml alone: Lean's tEqWord is normative and TG-3's 496 kernel-checked obligations tie OCaml's infer_expr to it, so changing one engine silently breaks the differential.
The rule today
| tEqWord (Γ : Ctx) (e₁ e₂ : Expr) (n : Nat) : -- [T-Eq-Word]
HasType Γ e₁ (.word n) →
HasType Γ e₂ (.word n) → -- SAME n, both sides
HasType Γ (.eq e₁ e₂) .boolBoth engines agree with each other. The problem is that the language disagrees with itself, in four separate ways.
Evidence 1 — compose already widens; equality does not
Same file, same type language:
| tComposeWord … : HasType Γ e₁ (.word n) → HasType Γ e₂ (.word m) →
HasType Γ (.compose e₁ e₂) (.word (max n m)) -- WIDENS
| tEqWord … : HasType Γ e₁ (.word n) → HasType Γ e₂ (.word n) →
HasType Γ (.eq e₁ e₂) .bool -- same width onlySo braid[s1] . braid[s2] is fine (Word[2] . Word[3] → Word[3]), but braid[s1] == braid[s2] is a type error. You can build a thing you are not allowed to test. Auto-widening is documented as a language feature at the top of typecheck.ml; equality is the exception.
Evidence 2 — ~ already accepts differing widths, and since TG-7 calls the same function
In adjacent match cases of infer_binop:
| Eq -> …
| TWord n, TWord m when n = m -> TBool
| TWord n, TWord m -> type_error "Cannot compare words of differing width: …"
| Isotopy -> …
| TWord _, TWord _ -> TBool (* no width check at all *)
Since #87 both operators evaluate through Braid_equiv.equiv — the identical decision procedure. Demonstrated on main:
== : In definition 'a': Cannot compare words of differing width: Word[2] == Word[3]
~ : typechecks fine, evaluates
Identical operands, identical runtime function, identical answer — one is rejected by the typechecker and the other is not. That is not a design choice anyone made; it is drift.
Evidence 3 — two Lean step rules are all but unreachable
| eqIdBraid : Step (.eq .identity (.braidLit gs)) (.boolLit (isTrivialBraid gs))
| eqBraidId : Step (.eq (.braidLit gs) .identity) (.boolLit (isTrivialBraid gs))
identity : word 0 (tIdentity), so under tEqWord these only ever type when generatorWidth gs = 0 — i.e. when gs = []. The semantics has dedicated rules for "is this braid trivial?", and the typing rule forbids asking. The rules were clearly written expecting cross-width comparison.
Evidence 4 — the decision procedure never cared
braid_equiv.equiv takes two generator lists and reduces u · v⁻¹. It has no width parameter and no width check. Only the typing rule forbids what the implementation already computes correctly.
What it blocks
|
|
lib/stdlib.tangle |
the standard library does not typecheck — Cannot compare words of differing width: Word[2] == Word[0] |
examples/trefoil.tangle |
Word[0] == Word[2] |
examples/compositional_pd.tangle |
Word[0] == Word[3] |
examples/tensor_product.tangle |
Word[0] == Word[5] |
examples/braids_as_data.tangle |
Word[3] == Word[2] |
examples/turing_complete.tangle |
the match-arm variant: arms at Word[2] vs Word[0] |
Four of the five remaining #88 failures are this one rule. (The fifth, recursive scalar functions, is fixed in #91.)
The mathematics
Braid groups embed: Bₙ ↪ Bₙ₊₁ by adding a strand that does nothing. A word on 2 strands is a word on 3 strands that never touches the third. So "are these equal?" across widths is not ill-formed — it is asked in the larger group, which is exactly what equiv already does.
identity == braid[s1, s1^-1] is the most natural phrasing of "is this trivial?", and it is currently a type error.
Options
(a) Widen — Word[n] == Word[m] is well-typed, decided in B_max(n,m).
Matches tComposeWord, matches ~, matches the implementation, un-blocks the stdlib and four examples, and makes eqIdBraid/eqBraidId reachable. Cost: change tEqWord in Lean and Eq in OCaml, re-check Progress/Preservation/Determinism (likely cheap — as with TG-7 the theorems need the rule's shape, not its side condition), and regenerate TG3Differential.lean via tg3_emit.
(b) Keep the restriction; fix the corpus.
Rewrite the stdlib and four examples to avoid cross-width comparison. Cheap and local, but it leaves == stricter than ~ for the same computation, leaves two step rules unreachable, and makes "is this braid trivial?" unsayable via ==. It also means the language's own stdlib is shaped around a rule the implementation doesn't need.
(c) Narrow ~ to match ==.
Consistent, but the wrong direction: it would break examples/isotopy.tangle, which is currently the only example demonstrating the central claim, and it contradicts TG-7 — where the whole point was that equivalence is not syntactic.
Recommendation
(a), with the match-arm width join decided at the same time (the turing_complete case) so the two don't drift apart the way == and ~ just did.
I would take it in one change across both engines, exactly as #87 did — OCaml, Lean, regenerate the TG-3 differential, and tests that distinguish the semantics. Not before a ruling, though: this changes what type-checks, and #50 established that is an owner call.
A cross-engine language-design decision, in the same shape as #50. It cannot be made in OCaml alone: Lean's
tEqWordis normative and TG-3's 496 kernel-checked obligations tie OCaml'sinfer_exprto it, so changing one engine silently breaks the differential.The rule today
Both engines agree with each other. The problem is that the language disagrees with itself, in four separate ways.
Evidence 1 — compose already widens; equality does not
Same file, same type language:
| tComposeWord … : HasType Γ e₁ (.word n) → HasType Γ e₂ (.word m) → HasType Γ (.compose e₁ e₂) (.word (max n m)) -- WIDENS | tEqWord … : HasType Γ e₁ (.word n) → HasType Γ e₂ (.word n) → HasType Γ (.eq e₁ e₂) .bool -- same width onlySo
braid[s1] . braid[s2]is fine (Word[2] . Word[3] → Word[3]), butbraid[s1] == braid[s2]is a type error. You can build a thing you are not allowed to test. Auto-widening is documented as a language feature at the top oftypecheck.ml; equality is the exception.Evidence 2 —
~already accepts differing widths, and since TG-7 calls the same functionIn adjacent match cases of
infer_binop:Since #87 both operators evaluate through
Braid_equiv.equiv— the identical decision procedure. Demonstrated onmain:Identical operands, identical runtime function, identical answer — one is rejected by the typechecker and the other is not. That is not a design choice anyone made; it is drift.
Evidence 3 — two Lean step rules are all but unreachable
identity : word 0(tIdentity), so undertEqWordthese only ever type whengeneratorWidth gs = 0— i.e. whengs = []. The semantics has dedicated rules for "is this braid trivial?", and the typing rule forbids asking. The rules were clearly written expecting cross-width comparison.Evidence 4 — the decision procedure never cared
braid_equiv.equivtakes two generator lists and reducesu · v⁻¹. It has no width parameter and no width check. Only the typing rule forbids what the implementation already computes correctly.What it blocks
lib/stdlib.tangleCannot compare words of differing width: Word[2] == Word[0]examples/trefoil.tangleWord[0] == Word[2]examples/compositional_pd.tangleWord[0] == Word[3]examples/tensor_product.tangleWord[0] == Word[5]examples/braids_as_data.tangleWord[3] == Word[2]examples/turing_complete.tangleWord[2]vsWord[0]Four of the five remaining #88 failures are this one rule. (The fifth, recursive scalar functions, is fixed in #91.)
The mathematics
Braid groups embed: Bₙ ↪ Bₙ₊₁ by adding a strand that does nothing. A word on 2 strands is a word on 3 strands that never touches the third. So "are these equal?" across widths is not ill-formed — it is asked in the larger group, which is exactly what
equivalready does.identity == braid[s1, s1^-1]is the most natural phrasing of "is this trivial?", and it is currently a type error.Options
(a) Widen —
Word[n] == Word[m]is well-typed, decided in B_max(n,m).Matches
tComposeWord, matches~, matches the implementation, un-blocks the stdlib and four examples, and makeseqIdBraid/eqBraidIdreachable. Cost: changetEqWordin Lean andEqin OCaml, re-check Progress/Preservation/Determinism (likely cheap — as with TG-7 the theorems need the rule's shape, not its side condition), and regenerateTG3Differential.leanviatg3_emit.(b) Keep the restriction; fix the corpus.
Rewrite the stdlib and four examples to avoid cross-width comparison. Cheap and local, but it leaves
==stricter than~for the same computation, leaves two step rules unreachable, and makes "is this braid trivial?" unsayable via==. It also means the language's own stdlib is shaped around a rule the implementation doesn't need.(c) Narrow
~to match==.Consistent, but the wrong direction: it would break
examples/isotopy.tangle, which is currently the only example demonstrating the central claim, and it contradicts TG-7 — where the whole point was that equivalence is not syntactic.Recommendation
(a), with the match-arm width join decided at the same time (the
turing_completecase) so the two don't drift apart the way==and~just did.I would take it in one change across both engines, exactly as #87 did — OCaml, Lean, regenerate the TG-3 differential, and tests that distinguish the semantics. Not before a ruling, though: this changes what type-checks, and #50 established that is an owner call.