From 57e404ef4b9d8f79e42c310614ad87b276e00736 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 07:53:03 +0100 Subject: [PATCH] =?UTF-8?q?fix(typecheck):=20implement=20[T-Twist-Strand]?= =?UTF-8?q?=20=E2=80=94=20(~a)=20on=20a=20named=20strand=20(#96)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- compiler/lib/eval.ml | 12 ++++++++++++ compiler/lib/typecheck.ml | 31 ++++++++++++++++++++++++++----- compiler/test/test_typecheck.ml | 25 +++++++++++++++++++++++++ scripts/check-corpus.sh | 10 +++------- 4 files changed, 66 insertions(+), 12 deletions(-) diff --git a/compiler/lib/eval.ml b/compiler/lib/eval.ml index cd909cc..99cd309 100644 --- a/compiler/lib/eval.ml +++ b/compiler/lib/eval.ml @@ -428,6 +428,18 @@ let rec eval_expr (env : env) (e : expr) : value = cup/cap pair. Represented as an empty closed tangle. *) VTangle { tv_word = []; tv_closed = true } + (* [T-Twist-Strand]: `(~a)` on a NAMED STRAND inside a weave. Treated as + structural, exactly as `Crossing` is below — weave bodies describe a + morphism, and the interpreter carries no strand context at runtime. + A single-strand twist is in any case invisible to the braid WORD: it is a + framing change (Reidemeister I), which the braid group does not see. + + Safe to detect by "a Var the environment does not bind": the typechecker + runs first and accepts `Twist (Var a)` ONLY when `a` is in the strand + context, so a genuinely unbound variable never reaches here. *) + | Twist (Var a) when env_lookup env a = None -> + ignore a; VBraid [] + | Twist e1 -> let v = eval_expr env e1 in begin match v with diff --git a/compiler/lib/typecheck.ml b/compiler/lib/typecheck.ml index f40d8d1..99b42d7 100644 --- a/compiler/lib/typecheck.ml +++ b/compiler/lib/typecheck.ml @@ -373,11 +373,32 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty = (* [T-Twist-Word], [T-Twist-Tangle] (D1.18) *) | Twist e1 -> - let t = infer_expr gamma sigma e1 in - begin match t with - | TWord n -> TWord n - | TTangle (a, b) -> TTangle (a, b) - | _ -> type_error "twist requires Word[n] or Tangle[A,B], got %s" (pp_ty t) + (* [T-Twist-Strand] (D1.18, spec section 3.10) must be tried FIRST: + * + * Sigma(a) = (i, T) + * --------------------------------- + * Gamma; Sigma |- (~a) : Tangle[[T], [T]] + * + * `(~a)` on a NAMED STRAND inside a weave twists that strand. Falling + * through to the general case would infer `a` as an ordinary expression, + * and the Var rule rejects strand names outright ("cannot be used as a + * standalone expression") — which is why conformance/valid/v09_twist.tangle + * never typechecked despite the spec licensing it. + * + * Exactly parallel to [T-Self-Cross] below, which types `(a > a)` the same + * way; the spec presents them as a pair. *) + begin match e1 with + | Var a when strand_lookup sigma a <> None -> + let ea = Option.get (strand_lookup sigma a) in + TTangle ([strand_to_type ea.strand_ty], [strand_to_type ea.strand_ty]) + | _ -> + (* [T-Twist-Word] / [T-Twist-Tangle]: the standalone forms. *) + let t = infer_expr gamma sigma e1 in + begin match t with + | TWord n -> TWord n + | TTangle (a, b) -> TTangle (a, b) + | _ -> type_error "twist requires Word[n] or Tangle[A,B], got %s" (pp_ty t) + end end (* ---- Crossings in weave context [T-Cross-Over], [T-Cross-Under] ---- *) diff --git a/compiler/test/test_typecheck.ml b/compiler/test/test_typecheck.ml index c7fc4cc..d448e8f 100644 --- a/compiler/test/test_typecheck.ml +++ b/compiler/test/test_typecheck.ml @@ -357,6 +357,31 @@ let test_isotopy () = infer gamma (BinOp (Isotopy, Var "t1", Var "t2")) = TBool); (* Isotopy: non-topological types -> error *) + (* #96 [T-Twist-Strand] (D1.18): `(~a)` on a NAMED STRAND inside a weave. + Specified in FORMAL-SEMANTICS section 3.10 and in spec/grammar.ebnf, but + infer_expr rejected any strand name used as an expression, so the + construct was licensed by the spec and unimplemented. Parallel to + [T-Self-Cross], which the spec presents alongside it. *) + test "#96 T-Twist-Strand: (~a) on a strand is Tangle[[T],[T]]" (fun () -> + let sigma = [("a", { strand_pos = 1; strand_ty = StrandNamed "Q" })] in + infer_expr [] sigma (Twist (Var "a")) + = TTangle ([StrandNamed "Q"], [StrandNamed "Q"])); + + test "#96 twist agrees with the self-crossing rule it parallels" (fun () -> + (* [T-Self-Cross] types (a > a) the same way; the two must not diverge. *) + let sigma = [("a", { strand_pos = 1; strand_ty = StrandNamed "Q" })] in + infer_expr [] sigma (Twist (Var "a")) + = infer_expr [] sigma (Crossing ("a", Over, "a"))); + + test "#96 standalone twist on a Word is unchanged" (fun () -> + (* Regression guard: [T-Twist-Word] must still apply outside a weave. *) + infer [] (Twist (BraidLit [sigma 1])) = TWord 2); + + test "#96 twist of a non-strand, non-word is still rejected" (fun () -> + (* `raises` is defined in a later group; inline it here. *) + try let _ = infer [] (Twist (StringLit "x")) in false + with Type_error _ -> true); + test "T-Isotopy (type error)" (fun () -> try let _ = infer [] (BinOp (Isotopy, IntLit 1, IntLit 2)) in diff --git a/scripts/check-corpus.sh b/scripts/check-corpus.sh index 9e71d40..d190ca8 100755 --- a/scripts/check-corpus.sh +++ b/scripts/check-corpus.sh @@ -75,14 +75,10 @@ CONFORMANCE_KNOWN_UNPARSED=( ) # conformance/valid programs that PARSE but do not yet TYPECHECK+EVALUATE. -# v09_twist : `(~a)` — twisting a named strand inside a weave. spec/grammar.ebnf -# says "In weave context: (~a) twists named strand a", but -# infer_expr rejects any strand name used as an expression, so the -# construct is specified and unimplemented. Tracked in #96. -# v11 : does not parse at all (see above); listed here too so the eval -# loop does not double-report it. +# v11 : does not parse at all (see above); listed here too so the eval loop +# does not double-report it. +# (v09_twist was listed here for [T-Twist-Strand] until #96 implemented it.) CONFORMANCE_KNOWN_UNRUNNABLE=( - v09_twist.tangle v11_add_block.tangle )