fix(typecheck): implement [T-Twist-Strand] — (~a) on a named strand (#96) - #101
Conversation
) conformance/valid/v09_twist.tangle: def twisted = weave strands a:Q into (~a) yield strands a:Q parsed but failed to typecheck with Strand name 'a' cannot be used as a standalone expression The spec licenses it explicitly. FORMAL-SEMANTICS section 3.10: Sigma(a) = (i, T) ----------------------------------- Gamma; Sigma |- (~a) : Tangle[[T], [T]] [T-Twist-Strand] and spec/grammar.ebnf: "In weave context: (~a) twists named strand a". The `Twist` case inferred its operand as an ordinary expression, and the `Var` rule rejects strand names outright — so the strand-name guard fired before the twist rule could apply. [T-Twist-Strand] is now tried FIRST, leaving [T-Twist-Word] / [T-Twist-Tangle] to the standalone forms. The spec presents this rule alongside [T-Self-Cross], which types `(a > a)` identically and was already implemented. One of a matched pair was missing; a test now pins that the two agree, so they cannot drift. Evaluation mirrors `Crossing`: structural, yielding the empty word. Weave bodies only became evaluable in #93, so this construct had never run. A single-strand twist is in any case invisible to the braid WORD — it is a framing change (Reidemeister I) that the braid group does not see. Detecting it as "a Var the environment does not bind" is safe because typechecking runs first and admits `Twist (Var a)` only when `a` is a strand. conformance: 16/19 -> 17/19 evaluating (18/19 parse). The corpus ratchet demanded the manifest update, which is what it is for. v11_add_block (#94, the Harvard sub-language) is now the only remaining gap. Tests: the rule itself, agreement with [T-Self-Cross], a regression guard that standalone twist on a Word is unchanged, and that a nonsense twist still fails. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
| | Twist (Var a) when env_lookup env a = None -> | ||
| ignore a; VBraid [] |
There was a problem hiding this comment.
💡 Edge Case: Twist eval guard diverges from typecheck under name shadowing
In eval.ml the [T-Twist-Strand] case is detected by Twist (Var a) when env_lookup env a = None, whereas the typechecker prioritizes the strand context (strand_lookup sigma a) over gamma. If a weave strand a shares a name with a top-level def a, typecheck classifies (~a) as a strand twist (Tangle[[T],[T]]) but eval finds a bound in env and falls through to the general Twist e1 branch, twisting the def's braid/tangle value instead of producing the structural empty word. The two phases then disagree on the meaning of the same expression. The neighboring Crossing case avoids this by ignoring env entirely; consider mirroring that (or checking the strand context) so eval and typecheck agree regardless of shadowing.
Was this helpful? React with 👍 / 👎
|
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 with suggestions 0 resolved / 1 findingsImplements the [T-Twist-Strand] typechecking and evaluation rule for named strands in weave contexts, advancing the conformance suite to 17/19. Consider aligning the twist evaluation guard with typechecking to prevent divergence under name shadowing.
💡 Edge Case: Twist eval guard diverges from typecheck under name shadowing📄 compiler/lib/eval.ml:440-441 📄 compiler/lib/typecheck.ml:390-393 In eval.ml the [T-Twist-Strand] case is detected by 🤖 Prompt for agentsOptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
|
|
1 participant
conformance/valid/v09_twist.tangleparsed but failed to typecheck:The spec licenses it explicitly
FORMAL-SEMANTICS.md§3.10:and
spec/grammar.ebnf: "In weave context:(~a)twists named strand a."The
Twistcase inferred its operand as an ordinary expression, and theVarrule rejects strand names outright — so the strand-name guard fired before the twist rule could apply.[T-Twist-Strand]is now tried first, leaving[T-Twist-Word]/[T-Twist-Tangle]to the standalone forms.One of a matched pair was missing
The spec presents this rule immediately alongside
[T-Self-Cross]:[T-Self-Cross]was already implemented; its twin was not. A test now pins that the two agree, so they can't drift apart again.Evaluation
Mirrors
Crossing: structural, yielding the empty word. Weave bodies only became evaluable in #93, so this construct had never run.That's also defensible mathematically — a single-strand twist is invisible to the braid word: it's a framing change (Reidemeister I) that the braid group doesn't see.
Detecting it as "a
Varthe environment doesn't bind" is safe because typechecking runs first and admitsTwist (Var a)only whenais a strand.Result
conformance 16/19 → 17/19 evaluating (18/19 parse). The corpus ratchet demanded the manifest update — exactly what it's for.
v11_add_block(#94, the Harvard sub-language) is now the only remaining gap.Tests: the rule itself; agreement with
[T-Self-Cross]; a regression guard that standalone twist on aWordis unchanged; and that a nonsense twist still fails.All suites green; corpus and RSR gates pass.
🤖 Generated with Claude Code