Skip to content

compile record copy (m(field = e)) to match+reconstruct, enabling in-place update#909

Draft
TimWhiting wants to merge 5 commits into
koka-lang:devfrom
TimWhiting:opt/copy-fbip
Draft

compile record copy (m(field = e)) to match+reconstruct, enabling in-place update#909
TimWhiting wants to merge 5 commits into
koka-lang:devfrom
TimWhiting:opt/copy-fbip

Conversation

@TimWhiting

@TimWhiting TimWhiting commented Jul 12, 2026

Copy link
Copy Markdown
Collaborator

The record-update idiom m(field = e) previously compiled (even at -O2, with the copy inlined) to one runtime OptArg/NoOptArg scrutiny per field plus one borrowing accessor match per unchanged field — and on the unique path Perceus freed the record and allocated a fresh one.

It now compiles to a single destructure that Perceus turns into an in-place field update when the value is unique (falling back to dup+alloc when shared):

fun bump(m) m(a = m.a + 1)
-- core at -O2:
match m { Model(a,b,c,d,e) -> Model(a+1, b, c, d, e) }   -- with constructor reuse

Three changes:

  • Copy synthesis (Kind/Infer.synCopyCon): the copy constructor is one match on @this reconstructing with either the given optional argument or the matched field, instead of per-field accessor calls as optional-argument defaults. No call-site-specialized copies: the definition inlines (InlineAlways) and the optional arguments — always literal OptArg/NoOptArg at a call site — fold away statically.

  • Simplify, known-constructor folding (kmatchPattern): answers NoMatch on constructor-name mismatch regardless of pattern arity (a single Unknown previously blocked branch selection entirely), handles nullary polymorphic constructor scrutinees and @box applications against @Box patterns, and A-normalizes non-total constructor arguments in let bindings (val x = Con(f(e))val y = f(e); val x = Con(y), same evaluation order) so the constructor binding is total and can inline into its match when used once (splitting only non-total arguments makes this a one-step fixpoint — total ones would inline back).

  • Simplify, known scrutinee: trailing let bindings sink into an irrefutable singleton match, and a match on a scrutinee variable folds inside a branch that already destructured it (wildcard fields are enriched to fresh pattern variables as needed) — so the m.a read in m(a = m.a + 1) becomes the pattern variable itself instead of a second borrow-match.

10M single-field updates of a five-field struct: 62ms → 16ms, flat rss.

test/parc/parc22/parc23 recorded core is regenerated and now pins the reuse shape (@con-fields-assign on the unique path inside @copy); parc15/parc16 exercise nested same-scrutinee matches, which now fold before Parc, and are regenerated likewise. Full test suite passes.

🤖 Generated with Claude Code

Copilot AI review requested due to automatic review settings July 12, 2026 20:36

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

Synthesize the copy constructor as one match on the copied value that
reconstructs with either the given optional argument or the matched field,
instead of per-field accessor calls as optional-argument defaults. After
inlining at a call site the optional scrutinies fold away statically,
leaving a single match+reconstruct that Perceus turns into an in-place
field update when the value is unique.

Simplify gains the missing pieces for that folding: a known-constructor
match reduction that answers NoMatch on constructor-name mismatch
regardless of pattern arity (one Unknown previously blocked branch
selection), handles nullary polymorphic constructors and box applications
against Box patterns, and A-normalizes non-total constructor arguments in
let bindings so the constructor binding itself becomes total and a
single-use binding can inline into its match.

10M single-field updates of a five-field struct: 62ms -> 11ms at -O2.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@TimWhiting
TimWhiting marked this pull request as draft July 12, 2026 21:11
TimWhiting and others added 2 commits July 12, 2026 15:27
Sink trailing let bindings into an irrefutable singleton match, and fold
matches on a scrutinee variable inside a branch that already destructured
it (enriching wildcard fields to fresh pattern variables as needed). A
record update m(a = m.a + 1) now compiles to a single destructure that
uses the matched field directly:

  match m { Model(a,b,c,d,e) -> Model(a+1, b, c, d, e) }

test/parc/parc15 and parc16 exercise nested same-scrutinee matches; their
recorded core is regenerated (the inner match now folds before Parc).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Matching can have effects in Koka: forcing a lazy value overwrites the
cell in place, so a later match on the same variable can see a different
constructor. Exclude thunk-constructor patterns from the known-scrutinee
fold and from irrefutability (whnf constructors remain eligible: forcing
is monotone). Values inside refs were already safe by construction: the
fold only unifies matches on the same immutable binding, and a ref read
is an application producing a fresh binding.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@TimWhiting

Copy link
Copy Markdown
Collaborator Author

Soundness note on the known-scrutinee fold (folding a nested match on an already-destructured variable): it relies on the scrutinee binding being immutable between the two matches, which holds in Koka core with one exception.

  • ref / var contents: safe by construction — the fold only unifies matches on the same core variable, and every !r / local-get read is an application producing a fresh binding, so matches on two reads never unify. Interior ref fields bind the ref pointer (immutable identity), not its contents.
  • Perceus reuse: runs after Parc; the fold runs on pre-Parc, immutable core.
  • Lazy values: the real exception — forcing overwrites the cell in place, so a match before a force and a match after can see different constructors. Thunk-constructor patterns are now excluded as witnesses (and from irrefutability for the let-sinking rule); whnf-constructor patterns remain eligible since forcing is monotone (thunk → value, never back).

🤖 Generated with Claude Code

TimWhiting and others added 2 commits July 20, 2026 12:55
…ation

The constructor witness built by enrichConPattern reused the pattern's
constructor name, whose instantiated type does not survive core
(de)serialization: the core parser resolves constructors to their
generic scheme, so a bare polymorphic Con application inlined
cross-module became ill-typed core (flagged by --checkcore as
'expecting function type in application'; runtime was unaffected).

Build the witness at the generic constructor scheme with an explicit
type application derived from the pattern result type, and skip the
fold in the (unexpected) case the instantiation cannot be recovered.

test/parc/parc24 pins the typed witness shape (--showcoretypes) and
runs with --checkcore, covering both the as-pattern nested match and
the polymorphic record-copy path.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <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.

2 participants