⏺ auto capture

[navicore]

Issue #395 — auto-capture for quotations passed to combinators — is implemented.
#395

What changed

File: crates/compiler/src/typechecker.rs
Change: analyze_captures: Extended to fire auto-capture when the body has more concrete inputs than the expected quotation type provides. Three sub-cases:

(a) expected is empty (strand.spawn, unchanged), (b) expected has concrete inputs and body has more (new — list.fold etc.), (c) expected has only
row-variable inputs (strand.weave — no capture, unify). infer_quotation: Closure pop loop now unifies each popped type against the expected capture

type
(soundness fix).
────────────────────────────────────────
File: tests/integration/src/test-auto-capture.seq
Change: New — 5 integration tests: fold+capture, map+capture, filter+capture, each+capture, Horner polynomial
────────────────────────────────────────
File: examples/projects/sss.seq
Change: Rewritten eval-poly: manual recursive loop → list.fold with auto-captured evaluation point. Removed eval-poly-loop. Updated header comments.
Secret
reconstruction still passes.

What works

• list.fold with one auto-captured value: fold body receives (acc, coeff, captured_x) with captured value on top
• list.map with captured offset: 100 [ i.+ ] list.map auto-captures 100
• list.filter with captured threshold: 4 [ >aux aux> i.< ] list.filter auto-captures 4
• list.each with captured value
• Auto-capture + aux-in-quotations compose: stash the captured value on quotation-level aux while doing fold work
• strand.spawn existing auto-capture: unchanged, still works
• strand.weave yield quotations: unchanged, still pass
• Shamir's Secret Sharing: eval-poly rewritten, "SUCCESS — secret recovered!" confirmed

Key convention

Captured values appear on top of the combinator-provided values at runtime. The body must be written accordingly: ( acc coeff captured_x ) with x on top
for a fold body that auto-captures one value.

[claude]

Code Review — Auto-Capture for Combinator Quotations (#395)

Overall this is solid work. The three-case logic (expected_is_empty / !expected_inputs.is_empty() / row-variable-only) is clear and well-commented, the sss.seq rewrite is a satisfying payoff for the feature, and the existing auto-capture paths (spawn, weave) are cleanly protected. A few things worth looking at:

---

Bug: misleading polynomial comment in test-horner-poly

: test-horner-poly ( -- )
  # p(x) = 2 + 1*x + 4*x^2 evaluated at x=3   ← this is wrong
  # Horner left-to-right: ((0*3+2)*3+1)*3+4 = 25
  list-of 2 lv 1 lv 4 lv
  ...

The Horner left-to-right trace ((0·3+2)·3+1)·3+4 = 25 is correct, and 25 is right. But the natural-language description is backwards. The list [2, 1, 4] is traversed high-to-low in coefficient order, so the actual polynomial is p(x) = 2x² + x + 4. At x=3: 18 + 3 + 4 = 25. ✓

The phrase "p(x) = 2 + 1·x + 4·x²" implies the constant term is 2, which would give p(3) = 2 + 3 + 36 = 41. The comment contradicts both the assertion and the Horner trace below it, so anyone reading it will be confused.

Suggested fix:

# p(x) = 2*x^2 + x + 4  (coefficients high-to-low: [2, 1, 4]) evaluated at x=3

Note this is different from eval-poly in sss.seq which reverses the list first (storing coefficients low-to-high). Worth making the convention explicit in one of the two places.

---

Unnecessary >aux aux> in test-filter-capture

[
  # Stack: ( elem threshold ) — threshold on top (captured)
  >aux aux> i.<     # elem < threshold
] list.filter

>aux stashes threshold and aux> immediately retrieves it — the pair is a no-op. The stack is already ( elem threshold ), so i.< alone computes elem < threshold directly. I suspect this was copied from the fold test where aux is genuinely needed, but it adds noise here.

---

Potential soundness gap: topmost body inputs not verified against expected

calculate_captures computes the number of captures as body_inputs.len() - expected_inputs.len() and slices the bottom N types. It does not verify that body_inputs[capture_count..] actually matches expected_inputs. So if someone writes a body whose remaining (non-captured) inputs are the wrong types for the combinator, the mismatch wouldn't be caught here.

For the spawn (empty-input) case this can't happen because all body inputs become captures. For the new non-empty case it could. Is that alignment checked downstream at the call site? If not, this is worth an issue or a // TODO: verify body[capture_count..] matches expected note in calculate_captures.

---

No negative tests for the new soundness fix

The closure-pop verification loop (type checking captures at the capture site) is the right thing to add, but there are no tests that verify it rejects a mismatch. Something like:

# should fail to compile:
# 42.0  # Float on stack
# [ ... ] list.fold  # body captures Float but expected Int

Even a comment in the test file noting "negative tests pending" would help signal intent.

---

Minor: use import inside function body

// typechecker.rs, analyze_captures
use crate::capture_analysis::extract_concrete_types;

Rust allows this, but the function already lives next to other code that presumably imports from capture_analysis. Moving this to the module-level imports would be tidier and avoid a reader wondering why the use is scoped to the match arm.

---

What's good

• The three sub-cases and their comments (including the stack diagram for the fold example) are excellent.
• The enumerate().rev() iteration with named position in the error message is a clear improvement over the silent loop.
• The eval-poly rewrite in sss.seq genuinely shows off the feature — replacing 18 lines of pick/roll juggling with a single fold is a meaningful demonstration.
• The updated sss.seq header is more honest about where the remaining non-idiomatic code lives and why.
• All five integration tests follow consistent structure and are self-documenting.

The polynomial comment bug and the possible gap in calculate_captures type alignment are the only things I'd want addressed before merging; the others are suggestions.

[claude]

Code Review — PR #400: auto capture

Overall this is a well-structured feature addition. The PR description is thorough, the code is well-commented, and the real-world validation via sss.seq is a good integration signal. Below are observations grouped by severity.

---

Potential Bugs / Soundness Gaps

1. should_capture branch coverage may have a latent gap (typechecker.rs ~line 2136)

The three-arm if/else if/else in analyze_captures works correctly for the three described cases, but it implicitly conflates two different conditions:

let expected_is_empty = matches!(expected_effect.inputs, StackType::Empty);
let should_capture = if expected_is_empty {
    !body_inputs.is_empty()
} else if !expected_inputs.is_empty() {   // concrete inputs exist
    body_inputs.len() > expected_inputs.len()
} else {
    false  // row-variable-only
};

The guard expected_is_empty tests the raw StackType, while !expected_inputs.is_empty() tests the concrete extracted types. These are complementary but not symmetric — if a new StackType variant were added (or if a Cons wrapping a RowVar occurs), the arms could produce unexpected results. Consider a unified predicate:

let expected_concrete_count = expected_inputs.len();
let body_concrete_count = body_inputs.len();
let should_capture = body_concrete_count > expected_concrete_count
    && !matches!(expected_effect.inputs, StackType::RowVar(_));

This is equivalent today but more robust to structural changes in StackType.

2. Topmost-type alignment not verified in calculate_captures (capture_analysis.rs lines 72–76)

The TODO you left is real and worth acting on before this merges — or at least promoting to a tracked issue. The current flow is:

1. calculate_captures counts the excess inputs → captures.
2. The topmost call_inputs.len() body types are assumed to align with the expected effect's inputs.
3. No structural comparison happens here; mismatch surfaces only during unification elsewhere or at runtime.

This means a user who writes a body like [ acc coeff x ] for a fold that provides (acc: String, elem: Bool) but captures an Int x, may not get a compile error at the capture site pointing at the actual stack layout mistake. Catching it here, as noted, would be a significant UX improvement.

3. Error message position index may be confusing (typechecker.rs ~line 1319–1326)

for (i, expected_type) in captures.iter().enumerate().rev() {
    let (new_stack, actual_type) = self.pop_type(...)?;
    unify_types(...).map_err(|e| {
        format!("closure capture type mismatch at position {}: ...", i, ...)
    })?;

captures is ordered bottom-to-top, and you iterate .rev() so you pop in top-down order (correct). But i is the bottom-to-top index, not the pop order. If there are 3 captures and the first pop (the topmost) fails, the error says "position 2" — which is accurate in the captures array sense, but may confuse users who think of position in terms of stack depth. A comment like "position in captures slice (0 = bottom-most)" would help.

---

Code Quality

4. Comment says "two sub-cases" but PR description says "three"

The inline comment at line ~2129 says "Two sub-cases: (a)…(b)…" but the PR description lists three. The code actually handles three distinct paths ((a) empty, (b) concrete, (c) row-var). Update the inline comment to say "Three sub-cases" to match the PR description and the actual logic.

5. eval-poly aux-level comment could use more explanation (sss.seq lines 106–112)

>aux                          # stash x in word-level aux: ( reversed_coeffs )
0                             # initial accumulator
aux>                          # retrieve x: ( reversed_coeffs 0 x )
[
  >aux                        # stash x in quotation-level aux

The pattern of stashing x at word level, pushing 0, then immediately retrieving x to put it back on the stack (just so it can be auto-captured) is non-obvious. A brief comment explaining why this dance is needed — e.g., "aux is used to interleave the fold acc before x so the auto-capture sees x on top" — would help future readers.

---

Test Coverage

6. test-each-capture has no assertion

: test-each-capture ( -- )
  # Just verify it compiles and runs without crashing.

This only catches crashes, not correctness regressions. Since list.each discards results, even a side-effectful accumulation (e.g., summing into an aux or global) could be asserted on. If the language has no mechanism for this yet, the comment is fine, but worth a follow-up issue.

7. No negative tests for the new should_capture path

There is no test for the case where a body has fewer inputs than the combinator expects (should fall through to the unification/error path). A test verifying that a type-mismatched quotation produces a compile error would give confidence that the unification error path still fires correctly.

8. No test for multiple simultaneous captures

All five integration tests capture exactly one value. A test capturing two values (e.g., a fold that captures both a multiplier and an offset) would exercise the multi-capture path in calculate_captures end-to-end.

9. No regression test for strand.weave (row-variable path)

The PR description notes strand.weave tests still pass, but there is no new test explicitly verifying that the false // row-variable-only branch does not accidentally trigger auto-capture. A targeted test here would guard against future regressions if the branch conditions change.

---

Minor

10. lagrange-basis-step packed-accumulator comment (sss.seq lines 186–194)

The comment accurately describes the workaround and flags it as future work for Issue #395. Since this PR is the Issue #395 implementation, update the comment to refer to "a future multi-capture fold" or a new tracking issue so it does not confuse readers who just landed this PR.

---

Summary

Category	Items
Potential bugs / soundness	3
Code quality	2
Test gaps	4
Minor	1

The core logic in analyze_captures and the closure pop loop is correct, and the real-world sss.seq validation is strong evidence it works end-to-end. The main things to address before merging are: promoting the topmost-type alignment gap to a tracked issue (item 2), and fixing the comment inconsistency (item 4). Items 6–9 are test improvements that would meaningfully increase confidence in the new paths.

[claude]

Code Review — Auto-capture for combinator quotations (Issue #395)

Overall this is a solid, well-scoped feature. The approach is sound, the sss.seq rewrite is noticeably cleaner, and the test spread across fold/map/filter/each is a good baseline. A few things worth looking at before merge:

---

Potential Bug — test-horner-poly doesn't exercise eval-poly

The new test at the bottom of test-auto-capture.seq inlines the Horner fold directly and passes coefficients high-to-low ([2, 1, 4]):

list-of 2 lv 1 lv 4 lv   # high-to-low
0  3  [...] list.fold
25 test.assert-eq

But eval-poly in sss.seq reverses the list before folding, so it expects low-to-high input. Calling eval-poly [2, 1, 4] 3 would produce 41, not 25.

Because the test never calls eval-poly, the actual rewritten word in sss.seq has no integration test. A test like:

: test-eval-poly ( -- )
  list-of 4 lv 1 lv 2 lv   # low-to-high: 4 + x + 2x^2
  3 eval-poly
  25 test.assert-eq          # 4 + 3 + 18 = 25
;

…would catch any regression in the new implementation. As written, the inlined fold test only validates the auto-capture mechanism itself (which is valuable), not the higher-level word that the PR is primarily showcasing.

---

Comment inconsistency — "Two sub-cases" vs. three branches

typechecker.rs (line ~2131):

// Auto-capture triggers when the body needs more concrete inputs
// than the expected provides. Two sub-cases:
// (a) Expected is empty (strand.spawn): body needs any inputs → capture all.
// (b) Expected has concrete inputs (list.fold): body has MORE → capture excess.
// We skip auto-capture when expected has ONLY a row variable ...

The prose says "Two sub-cases" but the code immediately below has three branches. The third branch (row-variable-only → false) is load-bearing and should be listed explicitly, or the label should read "Two capture sub-cases" to make clear the third branch opts out.

---

Error message position index — direction ambiguous

In typechecker.rs:

for (i, expected_type) in captures.iter().enumerate().rev() {
    ...
    format!("closure capture type mismatch at position {}: ...", i, ...)

enumerate() numbers from 0 at the bottom of the captures vector, and .rev() processes them top-down. So when a mismatch fires, the printed index is the bottom-up position — which is the opposite of the order the user sees on the stack. The calculate_captures error in capture_analysis.rs says "position {} (from top)", so the two error messages use opposite conventions. Consider standardising to one direction and labelling it explicitly (e.g. "position {i} (0 = bottommost capture)").

---

test-each-capture has no assertion

: test-each-capture ( -- )
  # Just verify it compiles and runs without crashing.
  ...
  ] list.each
;

A pure smoke test is fine, but a brief comment like # No value to assert — this test only checks that auto-capture compiles and executes makes the intent explicit and prevents a future reader from thinking the assertion was accidentally omitted. Alternatively, if list.each consumes the list, asserting the stack is empty afterward would add at least minimal runtime coverage.

---

Missing negative test for the new soundness check

calculate_captures now returns Err when the topmost body inputs don't align with what the combinator provides. There's no test that passes a deliberately mismatched quotation and verifies the compiler rejects it. Without this, a regression that silently drops the check would go unnoticed. A single negative test (expected compile error) would close this gap.

---

Minor: eval-poly comment in sss.seq

The new comment says "Coefficients are stored low-to-high [c0, c1, ...]" but the existing call sites in sss.seq (e.g. around the polynomial construction for Shamir shares) should be audited to confirm they actually pass low-to-high. If the previous eval-poly-loop had a different convention, callers may need updating. Worth a quick grep.

---

What's working well

• The should_capture guard (row-variable-only → don't capture) is the right call for the strand.weave case and the comment explains the reasoning clearly.
• Adding type unification in the Type::Closure branch (typechecker.rs) instead of just silently popping is a genuine soundness improvement.
• Splitting extract_concrete_types out for reuse is clean.
• The sss.seq rewrite reads much better — the aux/>aux pattern for stashing the captured value is the idiomatic approach and the comments track the stack at each step.

The main ask before merging would be a test-eval-poly call that exercises the real eval-poly word end-to-end, and a negative test for the new type-mismatch error.

[claude]

Code Review - PR 400: auto capture (Issue 395)

This is a solid, well-scoped feature. The three-branch should_capture logic is clean and clearly commented, the closure-pop type unification is the right soundness fix, and the sss.seq rewrite - 18 lines of pick/roll juggling replaced by a single fold - is a satisfying demonstration of the feature.

Below are observations in rough priority order.

---

Highest priority

1. eval-poly is never directly tested

test-horner-poly inlines its own Horner fold and passes coefficients high-to-low. But the rewritten eval-poly in sss.seq reverses the list first, so it expects low-to-high input. Calling eval-poly [2, 1, 4] 3 would produce 41, not 25. The inlined fold test validates auto-capture mechanics (good), but it does not exercise eval-poly itself. A direct test would catch any regression in the rewritten word, which is the headline change in the PR.

Suggested addition:

: test-eval-poly ( -- )
  list-of 4 lv 1 lv 2 lv   # low-to-high: 4 + x + 2x^2
  3 eval-poly
  25 test.assert-eq          # 4 + 3 + 18 = 25
;

2. No negative tests for the new soundness check

Both the topmost-type alignment check in calculate_captures and the unification in the closure-pop loop can now return errors, but there are no tests that verify a mismatched quotation is actually rejected at compile time. A single negative test (a body that captures the wrong type) would guard against a future regression silently dropping the check.

---

Moderate priority

3. test-each-capture has no assertion

This catches crashes only. Even a minimal runtime check - accumulating into an aux and checking its value - would add meaningful coverage. If the language makes this impossible right now, a comment explaining why and linking a follow-up issue is better than silent omission.

4. No test for multiple simultaneous captures

All five tests capture exactly one value. A test that captures two values (e.g., a fold body that captures both a multiplier and an offset) would exercise the multi-capture slice in calculate_captures end-to-end and confirm the bottom-to-top ordering is correct under load.

---

Minor

5. No-op >aux aux> in test-filter-capture

Stashing and immediately retrieving threshold is a no-op - the stack is already ( elem threshold ) and i.< works directly. This pattern is necessary in the fold test where aux is used to interleave values, but not here. Removing it simplifies the test and avoids teaching the wrong idiom.

6. Type-variable exemption in calculate_captures is correct but undocumented

The exemption (is_var check) is the right call - type variables are resolved by downstream unification - but there is no comment explaining this. A future reader might wonder why a mismatch involving type variables produces no error here. Worth a brief comment so the intent is clear.

---

What is working well

• The three-branch should_capture guard (empty / concrete / row-var-only) correctly handles spawn, fold/map/filter/each, and weave without conflating them.
• Adding type unification in the Type::Closure pop loop is a genuine soundness improvement; the error message gives the right context.
• Extracting extract_concrete_types for reuse is clean, and the module-level import is correctly placed.
• The sss.seq header update is more honest about what remains non-idiomatic and why.
• The updated eval-poly comment with per-line stack annotations is exactly the right level of documentation for an aux-heavy word.

The main asks before merging: a direct test-eval-poly call (item 1) and at least one negative type-mismatch test (item 2). Items 3-4 are meaningful coverage gaps; items 5-6 are cleanup.