Skip to content

Fuse curried lambdas into multi-argument lambda productions - #376

Open
kavigupta wants to merge 1 commit into
ns-abstraction-typingfrom
ns-abstraction-lambda-fusion
Open

Fuse curried lambdas into multi-argument lambda productions#376
kavigupta wants to merge 1 commit into
ns-abstraction-typingfrom
ns-abstraction-lambda-fusion

Conversation

@kavigupta

Copy link
Copy Markdown
Owner

PR 2 of 4. Stacks on #375. Review/merge that one first.

What

DreamCoder curries higher-order arguments as nested single-argument lambdas, but the list DSL types mapi/reducei with uncurried multi-argument arrows ((i, i) -> R, (i, R, i) -> R). A nested (lambda (lambda ...)) never unified against those, so the abstraction was skipped.

The stitch-body converter (_convert_stitch_node) is now type-directed: at each argument slot it reads the arrow arity the consuming primitive expects and fuses that many nested single-argument lambdas into the DSL's matching multi-argument lambda production (lam_1, lam_2).

Fusing a group reverses binder order (a native multi-arg lambda numbers $k by argument position; curried nesting numbers innermost-first), so enclosed de Bruijn variables are remapped via absolute binder levels — correct even for references from deeper nested lambdas.

Reproducing test

tests/s_exp/dreamcoder_abstractions_test.py::TestCurriedLambdaFusion

  • #(lambda (mapi_1 (lambda (lambda 0)) $0))[i] -> [i] (was skipped)
  • reducei_1 3-arg callback → [i] -> i
  • order-discriminating mapi_3 (index $1 $0) types, swapped (index $0 $1) is rejected
  • deeply nested cross-group reference → [[i]] -> [[i]]

🤖 Generated with Claude Code

DreamCoder curries higher-order arguments as nested single-argument lambdas,
but the list DSL types `mapi`/`reducei` with uncurried multi-argument arrows
(`(i, i) -> R`, `(i, R, i) -> R`), so a nested `(lambda (lambda ...))` never
unified against them and the abstraction was skipped.

Rewrite the stitch-body converter (`_convert_stitch_node`) to be type-directed:
at each argument slot it reads the arrow arity the consuming primitive expects
and fuses that many nested single-argument lambdas into the DSL's matching
multi-argument lambda production (`lam_1`, `lam_2`). Fusing a group reverses
the binder order (a native multi-arg lambda numbers `$k` by argument position,
whereas curried nesting numbers innermost-first), so enclosed de Bruijn
variables are remapped via absolute binder levels -- correct even for
references from deeper nested lambdas.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant