Issue #577: A tree rebuilt by value reuses the memory of the node it replaces (Lean 4 / Koka “functional but in place”)

Open and answer this issue on GitHub.

compiler, note · opened 2026-10-10 · updated 2026-10-10 · 0 comments

Where this comes from

From the decision on #576 / #558 (2026-10-10, ADR-094 D7). Two ways change a tree in Nikaia:

• In place, through a mut parameter: take the parts in a match arm, change them, assign the whole again. ADR-094 D7 allows this, with two conditions: the parameter is whole on every way out, and no throw and no call that can fail stands between taking and giving back (the owner chose this strict form, “A1”).
• By value: fn wrap(e: E) -> E { return match e { E::Add(a, b) => E::Add(wrap(a), wrap(b)), … } }. This runs today.

Below, a recursive enum’s children are Box<E>. The by-value form frees each node’s box and allocates a new one of the same size, once per node. Lean 4 and Koka write the same functional code. Where the old node is no longer referenced, their compilers hand its memory to the new node (“reuse analysis”, Perceus / “functional but in place”), so the program reads functionally and runs in place.

Why it is low priority

• D7 already gives the in-place path. A rewrite that needs no failing call is written with a mut parameter and needs no new node at all. That path depends on how #576 lowers it: it should keep the boxes (*e = E::Add(a, b) with the same Boxes) rather than unbox and rebox them. That belongs in #576, not here.
• The allocator often does it by accident. A free immediately followed by a malloc of the same size class usually returns the same block from the thread cache. What is left is the cost of the two calls, and that is not measured.
• Nothing measured asks for it. No benchmark or self-hosting module is known to be bound by this.

What value is left once D7 (A1) is built

1. Rewrites that can fail. A1 forbids a failing call while a part is out, so every tree rewrite that calls something throws must be written by value. This is the main remaining case. Checker and emitter walks that report errors may be among them once they are Nikaia (#558).
2. Code that is by value by nature: desugaring, constant folding (fold.nika), text_tiers-style rewrites that build a new tree from an old one, and code moved from Rust that was already written that way.
3. Cheaper in Nikaia than in Lean/Koka. Their reuse checks a reference count at run time. In Nikaia a value held by a mut or by-value parameter has one owner, which the compiler already knows (ADR-005, ADR-094). So the reuse can be decided statically, with no check left in the program.
4. Not for Vec: Rust’s into_iter().map(..).collect() already reuses the buffer when the element layouts match. The gain is boxed enum nodes, and possibly String.

To find out first (the measurement is owed before anything is built)

1. A tree of 10^5-10^6 nodes rewritten once by a by-value function (wrap above) and once by the D7 in-place form, both through nikaia run. Count instructions and mispredicted branches with callgrind, against hand-written Rust that reuses the box (CLAUDE.md: count, never time). The same output first.
2. From callgrind_annotate: what share of the by-value version is malloc/free.
3. Only if that share matters: a design for the lowering (where a match arm takes a node by value and builds a node of the same variant size, write into the old box), and a record (ADR) for it.

Until 1 and 2 are measured this issue stays note.

Back to Open Issues