Section 08: Algebra Law Adoption

Status: Not Started Goal: Install algebra blocks on stdlib operator traits (Add, Mul, Sub, Neg, etc.) and laws on stdlib impls (int, float, str, bool, list) so the normalization pass (Section 09) has concrete laws to consume. This is where Tang’s Monoid/Group/Ring models are expressed — not as a rigid hierarchy, but as opt-in law declarations on individual impls.

Critical soundness decisions (from consensus rounds 3-4):

float: Add does NOT declare associative — float reassociation changes results
float: Mul does NOT declare associative — same reason
str: Add declares associative and identity but NOT commutative — string concat is not commutative
[T]: Add declares associative and identity but NOT commutative — list concat is ordered
bool: && and || are hardcoded language operators, not overloadable traits. Section 09 may still normalize them for builtin bool, but Sections 07-08 do NOT model them as trait laws.

Depends on: Section 06 (runtime identity fixes — must land first so identity laws are sound) and Section 07 (algebra schema must exist).

08.1 Operator Trait Algebra Blocks

File(s): library/std/prelude.ori

Add algebra { } blocks to operator traits declaring which laws are available for impls to opt into.

Add to Add trait:

pub trait Add<Rhs = Self> {
    type Output
    @add (self, rhs: Rhs) -> Self.Output

    algebra {
        supports [associative, commutative]
        identity: Zero::zero
        inverse: Neg::negate
    }
}

Add to Mul trait:

pub trait Mul<Rhs = Self> {
    type Output
    @multiply (self, rhs: Rhs) -> Self.Output

    algebra {
        supports [associative, commutative]
        identity: One::one
        distributes_over [{ inner: Add::add, side: both }]
    }
}

Add to Neg trait:

pub trait Neg {
    type Output
    @negate (self) -> Self.Output

    algebra {
        supports [involutive]
    }
}

Add to Not trait:

pub trait Not {
    type Output
    @not (self) -> Self.Output

    algebra {
        supports [involutive]
    }
}

Sub, Div, Rem, FloorDiv — no algebra blocks (subtraction is not associative, division is not commutative)
BitAnd, BitOr, BitXor — algebra blocks for associative + commutative + identity (all/zero/zero respectively)
Do NOT add algebra blocks for logical && / ||: BinaryOp::And / Or do not map through BinaryOp::trait_name() and are validated as hardcoded boolean operators in ori_types
Verify: all modified trait definitions parse correctly
Verify: timeout 150 ./test-all.sh passes (algebra blocks with no law consumers are inert)
/tpr-review passed — independent review found no critical or major issues (or all findings triaged)
/impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.
Subsection close-out (08.1) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-08.1 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 08.1: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.
/sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.
Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

08.2 Stdlib Impl Laws

File(s): library/std/prelude.ori (or wherever stdlib impls live)

Add laws [ ] declarations to stdlib operator impls. Each law declaration is the programmer’s assertion that the algebraic property holds for this type+operation combination. The compiler trusts this.

IMPORTANT: Builtin operator impls do NOT exist as .ori impl blocks. Currently, prelude.ori defines operator traits (e.g., trait Add<Rhs = Self>) but NOT the impls for builtin types (int, float, str, etc.). Builtin operator dispatch is handled entirely by the type checker (via well-known trait bitfield and infer_binary_op) and the evaluator/codegen (via hardcoded dispatch). This means we have TWO options for installing laws:

Option A (.ori impl blocks): Add explicit impl Add for int { @add (self, rhs: int) -> int = self + rhs; laws [associative, commutative, identity, inverse] } to prelude.ori. This creates circular dispatch (the + in the body would resolve to the same Add::add). The type checker would need to handle this without infinite recursion. This is the cleaner long-term approach but requires careful compiler work.

Option B (Rust-side registration): Install laws during trait registration in compiler/ori_types/src/check/registration/traits.rs by populating ImplEntry.declared_laws for builtin type operator impls. This avoids .ori syntax issues but means laws are hardcoded in Rust rather than declared in the language.

Recommendation: Option B for this plan (pragmatic, matches how builtin operator impls already work). Option A is a future improvement when the language supports intrinsic impl bodies.

NOTE: All impl syntax in .ori below uses the CURRENT parser syntax (impl Trait for Type), not the planned impl Type: Trait syntax (roadmap Section 3.23, not yet implemented). For Option B (Rust-side registration), syntax is irrelevant.

08.3 Soundness Validation

File(s): Tests in tests/spec/algebra/ (NEW directory)

Write tests that verify the algebraic properties actually hold for each declared law. These are NOT compiler tests — they’re mathematical property tests executed by the Ori runtime.

Create tests/spec/algebra/ directory
For each impl with laws, write property tests. NOTE: every .ori test file MUST include use std.testing { assert_eq } (or { assert, assert_eq }) — assert_eq is NOT in the prelude.
- int_add_assoc.ori: assert_eq(actual: (a + b) + c, expected: a + (b + c)) for various a, b, c
- int_add_commutative.ori: assert_eq(actual: a + b, expected: b + a)
- int_add_identity.ori: assert_eq(actual: a + 0, expected: a) and assert_eq(actual: 0 + a, expected: a)
- str_add_identity.ori: assert_eq(actual: s + "", expected: s) and assert_eq(actual: "" + s, expected: s)
- str_add_assoc.ori: assert_eq(actual: (a + b) + c, expected: a + (b + c))
- list_add_identity.ori: list + [] and [] + list
- bool_and_identity.ori: b && true == b (runtime semantics validation — NOT an ARC IR optimization target since && is short-circuit control flow, not PrimOp)
- bool_or_identity.ori: b || false == b (runtime semantics validation — NOT an ARC IR optimization target since || is short-circuit control flow, not PrimOp)
- int_neg_involutive.ori: -(-x) == x for various x
- bool_not_involutive.ori: !!b == b
Negative tests verifying we correctly EXCLUDED:
- float_add_not_assoc.ori: demonstrate (1e15 + 1.0) + (-1e15) != 1e15 + (1.0 + (-1e15)) — proves associativity doesn’t hold for float
- str_add_not_commutative.ori: "ab" + "cd" != "cd" + "ab" — proves commutativity doesn’t hold for str
Verify: timeout 150 cargo st tests/spec/algebra/ passes
Trust model note: User-declared laws [] are trusted without runtime verification (same model as GHC RULES, C++ copy elision). An incorrect laws [associative] declaration on a user type will produce silently wrong optimized code. This is by design — runtime verification would eliminate the optimization benefit. Future work (not this plan): a --verify-algebra mode that inserts runtime property tests for declared laws during development builds.

Matrix dimensions:

Types: int, float, str, [int], bool
Laws: associative, commutative, identity, inverse, involutive
Coverage: positive (law holds) + negative (law correctly excluded)
Semantic pin: int_add_assoc.ori only meaningful with associative law declared
Negative pin: float_add_not_assoc.ori proves exclusion is correct
/tpr-review passed — independent review found no critical or major issues (or all findings triaged)
/impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.
Subsection close-out (08.3) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-08.3 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 08.3: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.
/sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.
Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

08.R Third Party Review Findings

None.

08.N Completion Checklist

Exit Criteria: Every overloadable stdlib operator impl has explicit algebraic law declarations. Soundness tests verify all declared properties hold. Float is correctly excluded from associativity and identity. Builtin bool logic (&& / ||) is explicitly kept outside the trait-law schema (they are control-flow IR, not PrimOps, and not optimizable at ARC IR level). All tests pass in debug and release.