From dbfc62a12da375eb8d13cd1a7f52e5a5d3252368 Mon Sep 17 00:00:00 2001 From: Eli Date: Tue, 28 Jul 2026 11:23:02 -0400 Subject: [PATCH 1/2] Fix quadratic term construction under nested binders `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) --- effectful/ops/semantics.py | 19 +++++++++++++++++ effectful/ops/syntax.py | 29 +++++++++++++++++++++++--- tests/test_ops_syntax.py | 42 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 87 insertions(+), 3 deletions(-) diff --git a/effectful/ops/semantics.py b/effectful/ops/semantics.py index b04ead5a3..e911c7c06 100644 --- a/effectful/ops/semantics.py +++ b/effectful/ops/semantics.py @@ -306,6 +306,25 @@ def _(self, op, *args, **kwargs): _TYPEOF_INTP = _TypeofIntp() +def _seed_typeof(expr: Expr, full_type: Any) -> None: + """Record a term's already-computed type analysis in its cache. + + :func:`~effectful.ops.syntax.defdata` computes the type of every term it + builds in order to pick a constructor. Storing that result here means a + parent's :func:`_typeof` on a freshly built child is a cache hit rather + than a fresh traversal of the whole subterm -- without which term + construction is quadratic in subterm size, and compounds multiplicatively + through nested binders. + """ + from effectful.internals.unification import Box + + if not isinstance(expr, Term): + return + cache = _term_cache(expr) + if cache is not None: + cache[_TYPEOF_INTP] = Box(full_type) + + def _typeof(term: Expr): """Evaluate the cached type analysis without unwrapping its result.""" return evaluate(term, intp=_TYPEOF_INTP) diff --git a/effectful/ops/syntax.py b/effectful/ops/syntax.py index 86c07a42a..1efb80838 100644 --- a/effectful/ops/syntax.py +++ b/effectful/ops/syntax.py @@ -491,7 +491,13 @@ def __call__(self: collections.abc.Callable[P, T], *args: P.args, **kwargs: P.kw it is reconstructed as a :class:`_CallableTerm`, which implements the :func:`__call__` method. """ from effectful.internals.runtime import interpreter - from effectful.ops.semantics import _simple_type, _typeof, apply, evaluate + from effectful.ops.semantics import ( + _seed_typeof, + _simple_type, + _typeof, + apply, + evaluate, + ) # If this operation binds variables, we need to rename them in the # appropriate parts of the child term. @@ -514,9 +520,24 @@ def evaluate_with_renaming(expr, ctx): # Note: coproduct cannot be used to compose these interpretations # because evaluate will only do operation replacement when the handler # is operation typed, which coproduct does not satisfy. - with interpreter({apply: defdata} | renaming_ctx): + # + # Rebuild with ``_reconstruct`` rather than ``defdata``: the subterm was + # already renamed when it was first built, so re-entering ``defdata`` + # here would recompute binders and rename each child again at every + # level, re-traversing the subtree once per level of nesting. + with interpreter({apply: _reconstruct} | renaming_ctx): return evaluate(expr) + def _reconstruct(op, *args, **kwargs): + """Rebuild one node, reusing its children's cached type analysis.""" + typed = tuple(_typeof(a) for a in args) + typed_kw = {k: _typeof(v) for k, v in kwargs.items()} + node_type = op.__type_rule__(*typed, **typed_kw) + node_dispatch = _simple_type(node_type) + node = __dispatch(node_dispatch)(node_dispatch, op, *args, **kwargs) + _seed_typeof(node, node_type) + return node + renamed_args = op.__signature__.bind(*args, **kwargs) renamed_args.apply_defaults() @@ -534,7 +555,9 @@ def evaluate_with_renaming(expr, ctx): typed_kwargs = {k: _typeof(v) for k, v in kwargs_.items()} full_type = op.__type_rule__(*typed_args, **typed_kwargs) dispatch_type = _simple_type(full_type) - return __dispatch(dispatch_type)(dispatch_type, op, *args_, **kwargs_) + result = __dispatch(dispatch_type)(dispatch_type, op, *args_, **kwargs_) + _seed_typeof(result, full_type) + return result def _construct_dataclass_term[T]( diff --git a/tests/test_ops_syntax.py b/tests/test_ops_syntax.py index 413f701e3..a5fdb749c 100644 --- a/tests/test_ops_syntax.py +++ b/tests/test_ops_syntax.py @@ -1457,3 +1457,45 @@ def _make_benchmark_term(size: int) -> Term[int]: result = benchmark(_make_benchmark_term, 25) assert isinstance(result, Term) + + +def test_bench_nested_binder_construction(benchmark): + """Benchmark term construction under *nested* binders. + + Constructing an operation that binds a variable renames that variable + throughout the body, which rebuilds the body. Nesting binders means each + level rebuilds everything beneath it, so a rebuild that is not single-pass + compounds multiplicatively with depth rather than adding to it. + + ``test_bench_term_construction`` builds a binder-free term, so it never + reaches this path -- it is fast even when nested construction is + exponential in depth. + """ + + @defop + def _benchmark_let[S, T, A]( + var: Annotated[Operation[[], S], Scoped[A]], + val: S, + body: Annotated[T, Scoped[A]], + ) -> T: + raise NotHandled + + @defop + def _benchmark_add(x: int, y: int) -> int: + raise NotHandled + + def _make_nested_term(depth: int) -> Term[int]: + """A term of ``depth`` nested binders, each used in the body below it.""" + if depth < 1: + raise ValueError("depth must be positive") + + body: Expr[int] = 0 + for index in range(depth): + var = defop(int, name=f"_benchmark_var_{index}") + body = _benchmark_let(var, 1, _benchmark_add(var(), body)) + + assert isinstance(body, Term) + return body + + result = benchmark(_make_nested_term, 10) + assert isinstance(result, Term) From a288c1c81c57b6505d34cc0e8b2f52c60aee6b56 Mon Sep 17 00:00:00 2001 From: Eli Date: Tue, 28 Jul 2026 14:37:22 -0400 Subject: [PATCH 2/2] Address review: drop _seed_typeof, share one term builder 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) --- effectful/ops/semantics.py | 19 -------------- effectful/ops/syntax.py | 52 ++++++++++++++++++-------------------- 2 files changed, 25 insertions(+), 46 deletions(-) diff --git a/effectful/ops/semantics.py b/effectful/ops/semantics.py index e911c7c06..b04ead5a3 100644 --- a/effectful/ops/semantics.py +++ b/effectful/ops/semantics.py @@ -306,25 +306,6 @@ def _(self, op, *args, **kwargs): _TYPEOF_INTP = _TypeofIntp() -def _seed_typeof(expr: Expr, full_type: Any) -> None: - """Record a term's already-computed type analysis in its cache. - - :func:`~effectful.ops.syntax.defdata` computes the type of every term it - builds in order to pick a constructor. Storing that result here means a - parent's :func:`_typeof` on a freshly built child is a cache hit rather - than a fresh traversal of the whole subterm -- without which term - construction is quadratic in subterm size, and compounds multiplicatively - through nested binders. - """ - from effectful.internals.unification import Box - - if not isinstance(expr, Term): - return - cache = _term_cache(expr) - if cache is not None: - cache[_TYPEOF_INTP] = Box(full_type) - - def _typeof(term: Expr): """Evaluate the cached type analysis without unwrapping its result.""" return evaluate(term, intp=_TYPEOF_INTP) diff --git a/effectful/ops/syntax.py b/effectful/ops/syntax.py index 1efb80838..cd66f5cd6 100644 --- a/effectful/ops/syntax.py +++ b/effectful/ops/syntax.py @@ -432,6 +432,26 @@ def deffn[T, A, B]( raise NotHandled +def _build_term[T]( + __dispatch: Callable[[type], Callable[..., Expr[T]]], + op: Operation[..., T], + *args, + **kwargs, +) -> Expr[T]: + """Build a single node from arguments whose bound variables are already renamed. + + This is :func:`defdata` without the renaming step: it computes the node's + type from the types of its arguments and dispatches on that type to pick a + constructor. + """ + from effectful.ops.semantics import _simple_type, _typeof + + typed_args = tuple(_typeof(arg) for arg in args) + typed_kwargs = {k: _typeof(v) for k, v in kwargs.items()} + dispatch_type = _simple_type(op.__type_rule__(*typed_args, **typed_kwargs)) + return __dispatch(dispatch_type)(dispatch_type, op, *args, **kwargs) + + @_CustomSingleDispatchCallable def defdata[T]( __dispatch: Callable[[type], Callable[..., Expr[T]]], @@ -491,13 +511,7 @@ def __call__(self: collections.abc.Callable[P, T], *args: P.args, **kwargs: P.kw it is reconstructed as a :class:`_CallableTerm`, which implements the :func:`__call__` method. """ from effectful.internals.runtime import interpreter - from effectful.ops.semantics import ( - _seed_typeof, - _simple_type, - _typeof, - apply, - evaluate, - ) + from effectful.ops.semantics import apply, evaluate # If this operation binds variables, we need to rename them in the # appropriate parts of the child term. @@ -521,23 +535,14 @@ def evaluate_with_renaming(expr, ctx): # because evaluate will only do operation replacement when the handler # is operation typed, which coproduct does not satisfy. # - # Rebuild with ``_reconstruct`` rather than ``defdata``: the subterm was + # Rebuild with ``_build_term`` rather than ``defdata``: the subterm was # already renamed when it was first built, so re-entering ``defdata`` # here would recompute binders and rename each child again at every # level, re-traversing the subtree once per level of nesting. - with interpreter({apply: _reconstruct} | renaming_ctx): + rebuild = functools.partial(_build_term, __dispatch) + with interpreter({apply: rebuild} | renaming_ctx): return evaluate(expr) - def _reconstruct(op, *args, **kwargs): - """Rebuild one node, reusing its children's cached type analysis.""" - typed = tuple(_typeof(a) for a in args) - typed_kw = {k: _typeof(v) for k, v in kwargs.items()} - node_type = op.__type_rule__(*typed, **typed_kw) - node_dispatch = _simple_type(node_type) - node = __dispatch(node_dispatch)(node_dispatch, op, *args, **kwargs) - _seed_typeof(node, node_type) - return node - renamed_args = op.__signature__.bind(*args, **kwargs) renamed_args.apply_defaults() @@ -550,14 +555,7 @@ def _reconstruct(op, *args, **kwargs): for (k, v) in renamed_args.kwargs.items() } - # Build the final term using the cached type analysis of its children. - typed_args = tuple(_typeof(arg) for arg in args_) - typed_kwargs = {k: _typeof(v) for k, v in kwargs_.items()} - full_type = op.__type_rule__(*typed_args, **typed_kwargs) - dispatch_type = _simple_type(full_type) - result = __dispatch(dispatch_type)(dispatch_type, op, *args_, **kwargs_) - _seed_typeof(result, full_type) - return result + return _build_term(__dispatch, op, *args_, **kwargs_) def _construct_dataclass_term[T](