diff --git a/compiler/lib/quantity.ml b/compiler/lib/quantity.ml new file mode 100644 index 0000000..a186e5e --- /dev/null +++ b/compiler/lib/quantity.ml @@ -0,0 +1,102 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* quantity.ml — the QTT quantity semiring {0, 1, omega}. + * + * Quantitative Type Theory (Atkey 2018) annotates each binding with a quantity + * drawn from a semiring. With {0, 1, omega} that single mechanism subsumes + * three disciplines rather than forcing a choice between them: + * + * 0 erased present for typing, absent at runtime + * 1 linear used exactly once + * omega unrestricted used freely + * + * ── Why TANGLE needs the semiring and not one discipline ──────────────────── + * The requirement is genuinely mixed, which is why "make the language linear" + * or "make it affine" are both wrong answers: + * + * * BRAID WORDS are unrestricted (omega). `x . x` is sigma_1^2 — composing + * a braid with itself is a legitimate braid, not resource duplication. + * Linearity would forbid a valid program. + * + * * STRANDS inside a `weave` are LINEAR (1). A strand is a physical thread: + * it is used exactly once, and it must come out the other side. Braids are + * permutations of n strands and strand count is a conservation law, so + * AFFINE is specifically wrong here — affine permits discarding, and a + * strand cannot vanish. + * + * * The CLAIM in `Epi[k, rho, tau]` (TG-11) is erased (0): it fixes the type + * and is never observable. Assumption A-TG-11.1 records that the current + * encoding carries it instead, because erasing it without quantities would + * break uniqueness of typing. This module is the missing half. + * + * ── Scope ─────────────────────────────────────────────────────────────────── + * This provides the semiring and applies it to STRAND usage, which is where + * the discipline actually bites and where a real soundness gap exists. It is + * NOT a QTT conversion of the whole core: TANGLE's judgement is still + * `Gamma |- e : tau` without quantities on ordinary bindings. Doing that means + * changing the judgement shape and re-proving the metatheory, and is tracked + * separately. + *) + +(** A quantity from the {0, 1, omega} semiring. *) +type t = + | Zero (** erased: present for typing, absent at runtime *) + | One (** linear: used exactly once *) + | Omega (** unrestricted *) + +let to_string = function + | Zero -> "0" | One -> "1" | Omega -> "omega" + +(** Semiring addition. Combines the quantities of two INDEPENDENT uses — + e.g. the two operands of a crossing. Using something once in each of two + places is using it twice, which is unrestricted usage, so 1 + 1 = omega + rather than an error: the error is raised later by [check_linear], when the + binding's declared quantity is compared against its total use. *) +let add a b = + match a, b with + | Zero, x | x, Zero -> x + | One, One -> Omega + | Omega, _ | _, Omega -> Omega + +(** Semiring multiplication. Scales a usage by the context it sits in — a + binding used once inside something used twice is used twice. Zero + annihilates: nothing inside an erased position is used at all. *) +let mul a b = + match a, b with + | Zero, _ | _, Zero -> Zero + | One, x | x, One -> x + | Omega, Omega -> Omega + +(** Additive identity. *) +let zero = Zero + +(** Multiplicative identity. *) +let one = One + +(** Is [actual] usage permitted where [declared] was promised? + + * [Zero] demands NO use at runtime. + * [One] demands EXACTLY one — neither zero (the resource vanishes) nor + more (it is duplicated). This is what makes it linear rather + than affine: [Zero] actual is a violation. + * [Omega] permits anything. *) +let permits ~declared ~actual = + match declared, actual with + | Zero, Zero -> true + | Zero, _ -> false + | One, One -> true + | One, _ -> false + | Omega, _ -> true + +(** Why a usage was rejected, in words a programmer can act on. *) +let explain ~declared ~actual = + match declared, actual with + | One, Zero -> + "declared linear (used exactly once) but never used — a strand cannot \ + vanish; braids conserve strand count" + | One, Omega -> + "declared linear (used exactly once) but used more than once — a strand \ + cannot be duplicated" + | Zero, _ -> + "declared erased (quantity 0) but used at runtime" + | _ -> + Printf.sprintf "declared %s but used %s" (to_string declared) (to_string actual) diff --git a/compiler/lib/typecheck.ml b/compiler/lib/typecheck.ml index 846b053..c976ff0 100644 --- a/compiler/lib/typecheck.ml +++ b/compiler/lib/typecheck.ml @@ -164,6 +164,77 @@ let apply_perm (b : boundary) (gens : generator list) : boundary = (* Type inference for expressions *) (* ================================================================== *) +(* ================================================================== *) +(* Strand linearity (QTT quantities applied to weave) *) +(* ================================================================== *) + +(** Count how many times each STRAND is used in a weave body, in the {0,1,omega} + semiring. Independent uses combine with semiring ADDITION, so two uses of + the same strand give 1 + 1 = omega — which then fails the linear check. + + Strands appear in two places: as the operands of a crossing (`a > b`), and + under a twist (`(~a)`, [T-Twist-Strand]). *) +let rec strand_uses (sigma : strand_ctx) (e : expr) : (string * Quantity.t) list = + let merge xs ys = + List.fold_left (fun acc (n, q) -> + match List.assoc_opt n acc with + | Some q' -> (n, Quantity.add q q') :: List.remove_assoc n acc + | None -> (n, q) :: acc) xs ys + in + let go = strand_uses sigma in + let use n = if strand_lookup sigma n <> None then [(n, Quantity.one)] else [] in + match e with + | Crossing (a, _, b) -> merge (use a) (use b) + | Twist (Var a) -> use a + | Var a -> use a + | BinOp (_, x, y) | Pipeline (x, y) | Cap (x, y) | Cup (x, y) + | Pair (x, y) | EchoAdd (x, y) | EchoEq (x, y) -> merge (go x) (go y) + | UnaryOp (_, x) | Close x | Mirror x | Reverse x | Simplify x | Twist x + | EchoClose x | Lower x | Residue x | Fst x | Snd x | Evidence x -> go x + | Warrant (_, c, ev) | EpiVal (_, c, ev) -> merge (go c) (go ev) + | Let (_, a, b) -> merge (go a) (go b) + | Match (sc, arms) -> + List.fold_left (fun acc a -> merge acc (go a.arm_body)) (go sc) arms + | Call (_, args) -> List.fold_left (fun acc a -> merge acc (go a)) [] args + | Weave wb -> go wb.weave_body + | AddBlock _ | BraidLit _ | Identity | BoolLit _ | IntLit _ | FloatLit _ + | StringLit _ -> [] + +(** Enforce that every declared input strand is used EXACTLY ONCE, and that the + yielded strands are a permutation of the inputs. + + Both halves are conservation laws of braids, not stylistic rules. A braid + on n strands is a permutation of those n strands: none may be duplicated + (contraction) and none may vanish (weakening). That is why the discipline + is LINEAR and not affine — affine would permit the second. *) +let check_strand_linearity (sigma : strand_ctx) (wb : weave_block) : unit = + let uses = strand_uses sigma wb.weave_body in + (* 1. Each input is linear: exactly one use. *) + List.iter (fun (name, _) -> + let actual = match List.assoc_opt name uses with + | Some q -> q | None -> Quantity.zero in + if not (Quantity.permits ~declared:Quantity.one ~actual) then + type_error "strand '%s': %s" name + (Quantity.explain ~declared:Quantity.one ~actual) + ) sigma; + (* 2. The yield must be a permutation of the inputs: same multiset of names, + each exactly once. This is where `yield strands a, b, a` is caught. *) + let ins = List.map fst sigma in + let outs = List.map (fun ts -> ts.strand_name) wb.weave_outputs in + List.iter (fun n -> + let k = List.length (List.filter (( = ) n) outs) in + if k = 0 then + type_error "strand '%s' is declared but never yielded — a strand cannot \ + vanish; braids conserve strand count" n + else if k > 1 then + type_error "strand '%s' is yielded %d times — a strand cannot be \ + duplicated" n k + ) ins; + List.iter (fun n -> + if not (List.mem n ins) then + type_error "strand '%s' is yielded but was never declared as an input" n + ) outs + (* ================================================================== *) (* Harvard data types and the |-_hd judgement (spec sections 7.1, 9.3) *) (* ================================================================== *) @@ -300,6 +371,11 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty = (ts.strand_name, { strand_pos = i + 1; strand_ty = sty }) ) wb.weave_inputs in let input_boundary = List.map (fun (_, se) -> se.strand_ty) sigma' in + (* Strands are LINEAR — see [check_strand_linearity]. This must be applied + in BOTH weave forms: `def x = weave ...` reaches the expression rule and + never touches the statement rule, so checking only there would leave the + ordinary, idiomatic spelling of a weave completely unchecked. *) + check_strand_linearity sigma' wb; (* The body is checked in the strand context, exactly as the statement form does — strand names are only meaningful there. *) let body_ty = infer_expr gamma sigma' wb.weave_body in @@ -998,6 +1074,10 @@ let check_statement (gamma : env) (stmt : statement) : env = ) wb.weave_inputs in (* Build input boundary A *) let input_boundary = List.map (fun (_, se) -> se.strand_ty) sigma in + (* Strands are LINEAR (QTT quantity 1): used exactly once, and conserved + into the yield. Checked before the body's type, so the diagnostic names + the strand rather than some downstream type mismatch. *) + check_strand_linearity sigma wb; (* Type-check the body in the strand context *) let body_ty = infer_expr gamma sigma wb.weave_body in (* Validate the body produces a Tangle type *) diff --git a/compiler/test/dune b/compiler/test/dune index e2bf91a..3692c65 100644 --- a/compiler/test/dune +++ b/compiler/test/dune @@ -1,5 +1,5 @@ ; SPDX-License-Identifier: MPL-2.0 (tests - (names test_parser test_typecheck test_eval test_e2e test_property test_compositional test_roundtrip test_check test_jeg) - (libraries tangle)) + (names test_parser test_typecheck test_eval test_e2e test_property test_compositional test_roundtrip test_check test_jeg test_quantity) + (libraries tangle str)) diff --git a/compiler/test/test_quantity.ml b/compiler/test/test_quantity.ml new file mode 100644 index 0000000..32802fb --- /dev/null +++ b/compiler/test/test_quantity.ml @@ -0,0 +1,189 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* test_quantity.ml — the {0, 1, omega} quantity semiring, and the strand + * linearity rule built on it. + * + * Two halves, and the first is not decoration. A "semiring" whose operations + * do not actually satisfy the semiring laws is just two arbitrary tables, and + * every soundness claim resting on it is worth nothing. The carrier is three + * elements, so the laws are decidable by exhaustion: we check all 27 triples + * rather than asserting the laws in a comment. + * + * The second half checks the rule that consumes the semiring — that a strand + * is used exactly once, and that the yield is a permutation of the inputs. + *) + +open Tangle.Ast +open Tangle.Typecheck + +let passed = ref 0 +let failed = ref 0 + +let test name f = + (try + if f () then begin incr passed; Printf.printf " PASS %s\n" name end + else begin incr failed; Printf.printf " FAIL %s\n" name end + with e -> + incr failed; + Printf.printf " FAIL %s (%s)\n" name (Printexc.to_string e)) + +(* The whole carrier. Three elements, so "for all" is a fold, not a sample. *) +let all = Tangle.Quantity.[ Zero; One; Omega ] + +let for_all1 p = List.for_all p all +let for_all2 p = List.for_all (fun a -> List.for_all (p a) all) all +let for_all3 p = + List.for_all (fun a -> + List.for_all (fun b -> List.for_all (p a b) all) all) all + +(* ------------------------------------------------------------------ *) +(* Semiring laws — exhaustively, over every triple *) +(* ------------------------------------------------------------------ *) + +let () = print_endline "\n=== Semiring laws (exhaustive over all 3^3 triples) ===" + +let () = + let open Tangle.Quantity in + + test "(+) is associative" (fun () -> + for_all3 (fun a b c -> add (add a b) c = add a (add b c))); + + test "(+) is commutative" (fun () -> + for_all2 (fun a b -> add a b = add b a)); + + test "0 is the additive identity" (fun () -> + for_all1 (fun a -> add zero a = a && add a zero = a)); + + test "( * ) is associative" (fun () -> + for_all3 (fun a b c -> mul (mul a b) c = mul a (mul b c))); + + test "1 is the multiplicative identity" (fun () -> + for_all1 (fun a -> mul one a = a && mul a one = a)); + + test "0 annihilates under ( * )" (fun () -> + for_all1 (fun a -> mul zero a = zero && mul a zero = zero)); + + test "( * ) distributes over (+) on the left" (fun () -> + for_all3 (fun a b c -> mul a (add b c) = add (mul a b) (mul a c))); + + test "( * ) distributes over (+) on the right" (fun () -> + for_all3 (fun a b c -> mul (add a b) c = add (mul a c) (mul b c))) + +(* ------------------------------------------------------------------ *) +(* The intended readings of the two operations *) +(* ------------------------------------------------------------------ *) + +let () = print_endline "\n=== Intended readings ===" + +let () = + let open Tangle.Quantity in + + (* This single equation is the whole reason `a > a` is rejected: two + independent uses of a linear resource add to omega, and omega is not + permitted where 1 was declared. *) + test "1 + 1 = omega (two independent uses is unrestricted use)" (fun () -> + add one one = Omega); + + test "omega is absorbing under (+)" (fun () -> + for_all1 (fun a -> add Omega a = Omega)); + + (* permits is the linear, not the affine, check. The distinguishing case is + the FIRST one: an affine discipline would accept it. *) + test "declared 1, used 0 is REJECTED (linear, not affine)" (fun () -> + not (permits ~declared:one ~actual:zero)); + + test "declared 1, used 1 is accepted" (fun () -> + permits ~declared:one ~actual:one); + + test "declared 1, used omega is rejected" (fun () -> + not (permits ~declared:one ~actual:Omega)); + + test "declared omega permits every usage" (fun () -> + for_all1 (fun a -> permits ~declared:Omega ~actual:a)); + + test "declared 0 permits only 0" (fun () -> + for_all1 (fun a -> permits ~declared:zero ~actual:a = (a = Zero))); + + test "explain names the vanishing case" (fun () -> + let s = explain ~declared:one ~actual:zero in + (* substring search, so the wording can be improved without breaking this *) + let re = Str.regexp_string "never used" in + (try ignore (Str.search_forward re s 0); true with Not_found -> false)) + +(* ------------------------------------------------------------------ *) +(* Strand linearity, through the typechecker *) +(* ------------------------------------------------------------------ *) + +let () = print_endline "\n=== Strand linearity (weave) ===" + +let strand n = { strand_name = n; strand_type = Some "Q" } + +let weave ins body outs = + Weave { weave_inputs = List.map strand ins; + weave_body = body; + weave_outputs = List.map strand outs } + +let cross a b = Crossing (a, Over, b) + +let accepts e = + try ignore (infer_expr [] [] e); true with _ -> false + +let rejects e = not (accepts e) + +let () = + test "permutation weave is accepted" (fun () -> + accepts (weave ["a"; "b"] (cross "a" "b") ["b"; "a"])); + + test "identity-order yield is accepted" (fun () -> + accepts (weave ["a"; "b"] (cross "a" "b") ["a"; "b"])); + + test "single strand under a twist is accepted" (fun () -> + accepts (weave ["a"] (Twist (Var "a")) ["a"])); + + (* The three soundness gaps this work closes. *) + test "REJECTED: strand crossed with itself (a > a)" (fun () -> + rejects (weave ["a"; "b"] (cross "a" "a") ["a"; "b"])); + + test "REJECTED: strand yielded twice (contraction)" (fun () -> + rejects (weave ["a"; "b"] (cross "a" "b") ["a"; "b"; "a"])); + + test "REJECTED: strand dropped from the yield (weakening)" (fun () -> + rejects (weave ["a"; "b"] (cross "a" "b") ["a"])); + + test "REJECTED: yielding a strand that was never an input" (fun () -> + rejects (weave ["a"; "b"] (cross "a" "b") ["a"; "c"])); + + (* An input that the body never mentions is a violation too: it is declared + linear and used zero times. Distinct from the yield check — this one + fires even when the yield is a perfect permutation. *) + test "REJECTED: input strand never used in the body" (fun () -> + rejects (weave ["a"; "b"; "c"] (cross "a" "b") ["a"; "b"; "c"])) + +(* ------------------------------------------------------------------ *) +(* Braid WORDS are unrestricted — linearity must not leak into them *) +(* ------------------------------------------------------------------ *) + +let () = print_endline "\n=== Words stay unrestricted (omega) ===" + +let () = + (* `x . x` is sigma_1^2 — a legitimate braid. If the linear discipline + leaked out of `weave` and onto ordinary bindings, this would break, and + the language would reject valid programs. That is exactly why the answer + is a SEMIRING and not "make the language linear". *) + let gamma = [ ("x", EVal (TWord 2)) ] in + test "x . x typechecks (a word composed with itself)" (fun () -> + try ignore (infer_expr gamma [] (BinOp (Compose, Var "x", Var "x"))); true + with _ -> false); + + test "x . x . x typechecks (three uses)" (fun () -> + try + ignore (infer_expr gamma [] + (BinOp (Compose, Var "x", BinOp (Compose, Var "x", Var "x")))); + true + with _ -> false) + +(* ------------------------------------------------------------------ *) + +let () = + Printf.printf "\n=====================================\n"; + Printf.printf "Results: %d/%d passed\n" !passed (!passed + !failed); + if !failed > 0 then exit 1 diff --git a/conformance/ill-typed/t01_strand_duplicated_in_body.tangle b/conformance/ill-typed/t01_strand_duplicated_in_body.tangle new file mode 100644 index 0000000..dcf8ca9 --- /dev/null +++ b/conformance/ill-typed/t01_strand_duplicated_in_body.tangle @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: MPL-2.0 +# Conformance (ILL-TYPED): a strand crossed with itself. +# +# `a > a` uses the strand 'a' twice. Strands carry QTT quantity 1 (linear): +# a strand is a physical thread, not a value, and it cannot be duplicated. +# This PARSES — it is rejected by the typechecker, not the grammar. + +def self_cross = + weave strands a:Q, b:Q into + (a > a) + yield strands a:Q, b:Q diff --git a/conformance/ill-typed/t02_strand_duplicated_in_yield.tangle b/conformance/ill-typed/t02_strand_duplicated_in_yield.tangle new file mode 100644 index 0000000..37cfefb --- /dev/null +++ b/conformance/ill-typed/t02_strand_duplicated_in_yield.tangle @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: MPL-2.0 +# Conformance (ILL-TYPED): contraction — the yield names a strand twice. +# +# A braid on n strands is a PERMUTATION of those n strands, so the output +# boundary must be a permutation of the input boundary. Yielding 'a' twice +# manufactures a strand out of nothing. + +def duplicating = + weave strands a:Q, b:Q into + (a > b) + yield strands a:Q, b:Q, a:Q diff --git a/conformance/ill-typed/t03_strand_vanishes.tangle b/conformance/ill-typed/t03_strand_vanishes.tangle new file mode 100644 index 0000000..f63d594 --- /dev/null +++ b/conformance/ill-typed/t03_strand_vanishes.tangle @@ -0,0 +1,10 @@ +# SPDX-License-Identifier: MPL-2.0 +# Conformance (ILL-TYPED): weakening — a strand is dropped from the yield. +# +# This is the case that makes the discipline LINEAR rather than AFFINE. +# Affine would permit discarding; braids conserve strand count, so it cannot. + +def vanishing = + weave strands a:Q, b:Q into + (a > b) + yield strands a:Q diff --git a/conformance/ill-typed/t04_undeclared_strand_yielded.tangle b/conformance/ill-typed/t04_undeclared_strand_yielded.tangle new file mode 100644 index 0000000..4517f16 --- /dev/null +++ b/conformance/ill-typed/t04_undeclared_strand_yielded.tangle @@ -0,0 +1,7 @@ +# SPDX-License-Identifier: MPL-2.0 +# Conformance (ILL-TYPED): the yield names a strand that was never an input. + +def conjuring = + weave strands a:Q, b:Q into + (a > b) + yield strands a:Q, c:Q diff --git a/conformance/run_conformance.sh b/conformance/run_conformance.sh index c326014..7796cd3 100755 --- a/conformance/run_conformance.sh +++ b/conformance/run_conformance.sh @@ -2,8 +2,17 @@ # SPDX-License-Identifier: MPL-2.0 # Conformance test runner for Tangle # -# Invokes the Tangle compiler (OCaml/Menhir) on every file in valid/ -# and invalid/, asserting success for valid files and failure for invalid files. +# Three tiers, because "rejected" is not one property: +# +# valid/ MUST parse AND MUST typecheck +# invalid/ MUST FAIL TO PARSE (grammar-level rejection) +# ill-typed/ MUST PARSE but MUST FAIL to typecheck +# +# The third tier carries a DOUBLE assertion on purpose. Asserting only "the +# compiler rejects it" is the failure this suite already suffered once: an +# invalid case scores a point whenever the command fails, including when it +# fails for an unrelated reason. Requiring the file to parse FIRST proves the +# rejection came from the typechecker and not from a typo in the test. # # Usage: ./run_conformance.sh [path-to-tangle-binary] @@ -34,22 +43,30 @@ else fi fi -echo "parser: ${PARSER_CMD[*]}" +# The typechecker is the same binary with --check. Built as a separate array +# so a caller-supplied PARSER_CMD still gets the flag appended correctly. +CHECK_CMD=("${PARSER_CMD[@]}" --check) + +echo "parser: ${PARSER_CMD[*]}" +echo "typechecker: ${CHECK_CMD[*]}" PASS=0 FAIL=0 TOTAL=0 -# --- Valid programs: parser MUST succeed --- +# --- Valid programs: MUST parse AND MUST typecheck --- for f in "${SCRIPT_DIR}"/valid/*.tangle; do TOTAL=$((TOTAL + 1)) name="$(basename "$f")" - if "${PARSER_CMD[@]}" "$f" >/dev/null 2>&1; then + if ! "${PARSER_CMD[@]}" "$f" >/dev/null 2>&1; then + echo " FAIL valid/${name} (expected to parse, got a parse error)" + FAIL=$((FAIL + 1)) + elif ! "${CHECK_CMD[@]}" "$f" >/dev/null 2>&1; then + echo " FAIL valid/${name} (parses, but does not typecheck)" + FAIL=$((FAIL + 1)) + else echo " PASS valid/${name}" PASS=$((PASS + 1)) - else - echo " FAIL valid/${name} (expected success, got failure)" - FAIL=$((FAIL + 1)) fi done @@ -66,6 +83,24 @@ for f in "${SCRIPT_DIR}"/invalid/*.tangle; do fi done +# --- Ill-typed programs: MUST parse, MUST NOT typecheck --- +for f in "${SCRIPT_DIR}"/ill-typed/*.tangle; do + TOTAL=$((TOTAL + 1)) + name="$(basename "$f")" + if ! "${PARSER_CMD[@]}" "$f" >/dev/null 2>&1; then + # Not a pass. The file was supposed to reach the typechecker; if it + # cannot even parse, the test is broken and proves nothing. + echo " FAIL ill-typed/${name} (must PARSE first — got a parse error)" + FAIL=$((FAIL + 1)) + elif "${CHECK_CMD[@]}" "$f" >/dev/null 2>&1; then + echo " FAIL ill-typed/${name} (typechecker accepted an ill-typed program)" + FAIL=$((FAIL + 1)) + else + echo " PASS ill-typed/${name}" + PASS=$((PASS + 1)) + fi +done + echo "" echo "Results: ${PASS}/${TOTAL} passed, ${FAIL} failed" diff --git a/docs/spec/FORMAL-SEMANTICS.md b/docs/spec/FORMAL-SEMANTICS.md index b0061f6..5578281 100644 --- a/docs/spec/FORMAL-SEMANTICS.md +++ b/docs/spec/FORMAL-SEMANTICS.md @@ -477,6 +477,65 @@ yield declarations match B Weave blocks can reference all definitions in Γ (D2.8). +#### 3.10.1 Strand quantities — the linear discipline + +The rule above has two side conditions that were, until the quantity semiring +landed, written down and never enforced: the `i ≠ j` on `[T-Cross-Over]` / +`[T-Cross-Under]` below, and "yield declarations match B". Both are instances +of one law, so both are now discharged by one check. + +TANGLE annotates resources with a quantity from the QTT semiring +{0, 1, ω} (Atkey 2018), rather than committing the whole language to a single +substructural discipline: + +| quantity | reading | who carries it | +|---|---|---| +| `0` | erased — present for typing, absent at runtime | the claim in `Epi[κ, ρ, τ]` (see A-TG-11.1) | +| `1` | linear — used **exactly** once | **strands** inside a `weave` | +| `ω` | unrestricted — used freely | braid **words**, and every ordinary binding | + +Why a semiring and not a choice: + +- **Words are ω.** `x . x` is σ₁², a perfectly good braid. A blanket linear + discipline would reject a valid program. +- **Strands are 1, and linear rather than affine.** 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: a strand may be neither duplicated + (contraction) nor dropped (weakening). Affine permits the second, so affine + is specifically the wrong discipline here — this is the case that decides it. + +Independent uses combine with semiring addition, so two uses of one strand give +`1 + 1 = ω`, and `ω` is not permitted where `1` was declared. + +``` +Σ = {a₁ : (1, T₁), ..., aₙ : (n, Tₙ)} +uses(body, aᵢ) = 1 for every i (no contraction, no + unused strand) +⟦b₁, ..., bₘ⟧ is a permutation of ⟦a₁, ..., aₙ⟧ (m = n; conservation) +────────────────────────────────────────────────────────── [T-Weave-Linear] +Σ ⊢ weave strands a₁,...,aₙ into body yield strands b₁,...,bₘ linear +``` + +`uses` is defined by structural recursion over the body, mapping into the +semiring: a strand occurrence contributes `1`, the two operands of a crossing +and the two sides of any binary form combine with `+`, and non-strand leaves +contribute `0`. + +Four programs this rejects, each previously accepted in silence: + +| program | violated law | +|---|---| +| `weave strands a, b into (a > a) yield strands a, b` | contraction (also the spec's `i ≠ j`) | +| `weave strands a, b into (a > b) yield strands a, b, a` | contraction in the yield | +| `weave strands a, b into (a > b) yield strands a` | weakening — a strand vanished | +| `weave strands a, b into (a > b) yield strands a, c` | `c` is not in the input boundary | + +**Scope.** This is the semiring applied *to strands*, which is where the +discipline bites and where the soundness gap was. TANGLE's core judgement is +still `Γ ⊢ e : τ` without quantities on ordinary bindings; a full QTT judgement +`Γ ⊢ e :^q τ` would change the judgement shape and require re-proving the +metatheory, and is tracked separately. + **Crossing in weave context**: ``` diff --git a/scripts/check-corpus.sh b/scripts/check-corpus.sh index 00a30d3..2cc005f 100755 --- a/scripts/check-corpus.sh +++ b/scripts/check-corpus.sh @@ -187,10 +187,39 @@ for f in "${ROOT}"/conformance/invalid/*.tangle; do fi done +# ── 6. Conformance: ill-typed programs must PARSE and then be REJECTED. +# +# A third tier, separate from invalid/, because "the compiler rejects it" is +# two different properties and conflating them produces a gate that passes for +# the wrong reason. invalid/ is grammar-level: the file must not parse. +# ill-typed/ is type-level: the file MUST parse — reaching the typechecker is +# the whole point of the test — and the typechecker must then reject it. +# +# Asserting only the rejection is precisely the failure this suite already had +# once, when three invalid/ cases "passed" because the command was wrong and +# failed on every input. A typo in an ill-typed/ fixture would score the same +# false point here, so the parse step is asserted first. +echo +echo "== conformance: ill-typed programs must parse, then be rejected ==" +for f in "${ROOT}"/conformance/ill-typed/*.tangle; do + [[ -e "$f" ]] || continue + n="$(basename "$f")" + if ! "${BIN}" "$f" >/dev/null 2>&1; then + note "ill-typed/$n" "PARSE FAILED (must parse first)" + echo "::error::conformance/ill-typed/${n} does not parse — it must reach the typechecker to prove anything"; fail=1 + elif "${BIN}" --check "$f" >/dev/null 2>&1; then + note "ill-typed/$n" "TYPECHECKED (should not)" + echo "::error::conformance/ill-typed/${n} was accepted by the typechecker but is meant to be rejected"; fail=1 + else + note "ill-typed/$n" "parsed, then rejected ok" + fi +done + echo if [[ "$fail" -ne 0 ]]; then echo "::error::corpus drifted from the manifest — see the errors above." exit 1 fi echo "Corpus matches the manifest: examples parse, the must-run set evaluates," -echo "known gaps are unchanged, and invalid programs are still rejected." +echo "known gaps are unchanged, invalid programs are still rejected, and" +echo "ill-typed programs still parse but still fail to typecheck."