Fix quadratic term construction under nested binders - #726
Merged
Conversation
`defdata` rebuilds a subterm when it renames bound variables. Re-entering `defdata` for the rebuild recomputed binders and renamed children again at every level, so nested binders re-traversed the subtree once per level. Rebuild with a single-pass `_reconstruct` instead, and seed each freshly built term's `_typeof` cache with the type analysis `defdata` already computed, so a parent's `_typeof` on a new child is a cache hit. Adds `test_bench_nested_binder_construction`; the existing `test_bench_term_construction` builds a binder-free term and never reaches this path. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
eb8680
marked this pull request as ready for review
July 28, 2026 15:25
eb8680
marked this pull request as draft
July 28, 2026 16:08
eb8680
marked this pull request as ready for review
July 28, 2026 16:08
jfeser
requested changes
Jul 28, 2026
Remove `_seed_typeof`. It is not what fixes the quadratic regression -- `_evaluate_term` already caches a node's typeof result whenever `_typeof` is called on it, so by the time `defdata` finishes a node every descendant is cached and the parent's `_typeof` on the fresh child is one level deep. The asymptotic fix is the `apply` rule, which stops the rebuild from re-entering `defdata` and re-running `__fvs_rule__` + renaming at every level. Seeding was a constant factor (~1.8x on nested construction, ~1.5x binder-free) bought by writing into a cache that `_evaluate_term` owns. `effectful/ops/semantics.py` is now unchanged by this branch. With the seeding gone, the rebuild rule and the tail of `defdata` are identical, so both become the module-level `_build_term`: `defdata` minus the renaming step. It takes `__dispatch` as a parameter rather than closing over it, so it lives at module level instead of being rebuilt on every `defdata` call; the `functools.partial` is allocated only on the renaming path. `test_bench_nested_binder_construction`: 572.8 ms before the branch, 17.2 ms now (33x). `test_bench_term_construction` returns to its baseline 3.5 ms, giving up the constant factor that the removed seeding provided. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
jfeser
self-requested a review
July 28, 2026 19:10
jfeser
approved these changes
Jul 28, 2026
jfeser
left a comment
jfeser
left a comment
Contributor
There was a problem hiding this comment.
Fine to merge once CI passes.
This was referenced Aug 3, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The regression
#716 ("Add cached interpretations and use for
typeof") madedefdatacompute thefull type analysis of every term it builds, in order to pick the right term
constructor. That interacts badly with binders: when an operation binds variables,
defdatarenames them throughout the body, which rebuilds the body by re-enteringdefdataviaapply. Re-enteringdefdatarecomputes binders and renames eachchild again at every level, so nesting binders re-traverses the subtree once per
level of nesting.
The changes
effectful/ops/syntax.py:evaluate_with_renamingnow rebuilds nodes with_build_terminstead of re-enteringdefdata. The subterm was already renamedwhen it was first built, so the rebuild only needs to re-dispatch each node, not
redo binder analysis and renaming.
_build_termisdefdataminus the renaming step, and is shared:defdataitself ends with
return _build_term(__dispatch, op, *args_, **kwargs_), and therebuild installs
functools.partial(_build_term, __dispatch)as theapplyrule.The change does not alter any observable result.
Benchmark
tests/test_ops_syntax.py::test_bench_nested_binder_constructionbuilds a termof 10 nested
let-style binders, each variable used in the body below it. Theexisting
test_bench_term_constructionbuilds a binder-free term, so it neverreaches this path and stays fast even when nested construction blows up.
Measured on this branch vs. the same test with the
effectful/change reverted(mean of pytest-benchmark rounds):
test_bench_nested_binder_constructiontest_bench_term_constructionAn earlier revision of this PR also seeded
defdata's already-computed typeanalysis into the per-term evaluation cache, which bought a further ~1.8x on
nested construction and ~1.5x on binder-free construction. That was dropped at
review: it reached past
_evaluate_term, which owns that cache, and it is aconstant factor rather than the asymptotic fix (with and without, nested
construction is quadratic in depth, at a flat ~1.8x ratio from depth 10 to 40).
Testing
Full test suite: 18749 passed, 1 skipped, 2108 xfailed.
mypyandruffcleanon the changed files.
Split out of #724 for review.
🤖 Generated with Claude Code