Pith. sign in

REVIEW 1 major objections 5 minor 18 references

Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming

T0 review · 1 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Reference counting can be tuned—by reusing dead cells, borrowing references, and avoiding atomic updates—so that eager pure functional programs match or beat tracing-GC compilers in benchmarks.

desk verdict A serious systems paper on RC for eager pure FP with real benchmarks; the reset/reuse and borrow-inference pieces are new, and the main open question is the missing layout-compatibility check in the formal reuse rule. read the letter →

arxiv 1908.05647 v3 pith:I5YWDV53 submitted 2019-08-15 cs.PL

Sebastian Ullrich , Leonardo de Moura This is my paper · ORCID
classification cs.PL
keywords purelyfunctionalprogrammingreferencecountingmemoryreusedestructiveupdateborrowedreferencesthread-safeLeancompilergarbagecollection
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper argues that reference counting, long considered inferior to tracing garbage collection for functional languages, can be made competitive for eager, purely functional code. The key move is to treat an object's reference counter as runtime evidence of ownership: when the counter is one, the object is not shared and its memory can be reused for the next same-kind object instead of being freed and reallocated. The authors implement this in the next Lean compiler, adding reset/reuse instructions, automatic borrow inference to skip most counter updates, and a thread-tagging scheme that avoids expensive atomic operations for single-threaded values. Benchmarks across several workloads show the generated code is competitive with, and often faster than, established functional-language compilers.

What carries the argument

The mechanism has three load-bearing parts. First, the reset/reuse instruction pair is the machine for destructive updates: reset inspects the counter, clears the children of a unique cell, and returns the cell; reuse stores a new constructor into that cell, or allocates if reset saw a shared value. Second, borrowed references are a calling-convention annotation marking parameters the callee will not consume, so no inc/dec is emitted for them, and a fixpoint heuristic infers which parameters can be borrowed. Third, values are tagged as single-threaded, multi-threaded, or persistent; only multi-threaded values pay for atomic reference-count operations, and the tags are propagated at task creation rather than at every store.

What would settle it

Instrument each reset site in the compiled runtime to record the fraction of executions where the object is shared, and run the included benchmarks plus proof-automation workloads; if the shared fraction is high where reuse was inserted, the reset/reuse mechanism is not driving the reported speedups.

Watch

Extended reading notes

Core claim

The central discovery is that in a purely functional, eager language, reference counting's exact knowledge of sharing unlocks memory reuse that tracing collectors cannot exploit. Concretely, the compiler inserts a reset before a constructor call and a reuse at the call: if the old value's counter is one, the constructor cell is overwritten in place; if the value is shared, reset falls back to a decrement and reuse allocates anew. Combined with borrowed parameters—arguments the callee only inspects and therefore need not be incremented or decremented—the scheme can remove most counting operations. The paper reports that this implementation, with a single/multi-threaded value tag that avoids memory fences, keeps pure quick sort, red-black tree insertion, and symbolic constant folding competitive with or faster than several established compilers, with much less time spent deallocating memory.

Load-bearing premise

The load-bearing premise is the resurrection hypothesis—objects die just before a same-kind object is created—together with the object being unshared at the reset point; if real workloads do not show that pattern, the memory-reuse optimization and the reported edge largely disappear.

Editorial extensions

If this is right

  • If the scheme works as claimed, purely functional data-structure code can get destructive updates for free whenever the input is unshared, removing allocations in map, swaps, and tree rebalancing.
  • Borrowed-reference inference means the speedup does not require hand-written annotations, making the intermediate representation a practical target for other pure functional languages.
  • Since single-threaded values avoid atomic reference-count operations, multithreading support adds little overhead to single-threaded execution.
  • Benchmarks indicate garbage-collection time drops to a small fraction of runtime on symbolic workloads, which is relevant for proof assistants and compilers that manipulate large expressions.
  • The same runtime supports destructive array and string updates when arrays are unshared, extending the scheme from constructor cells to primitive containers.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The reset/reuse heuristic is not tied to Lean; another eager pure language with an A-normal-form intermediate representation and accurate sharing information could apply the same dead-variable search and substitution transformation.
  • The paper's runtime can count how often a reset finds a shared versus unique object, so collecting those counts on proof-assistant and compiler traces would directly test how far the resurrection hypothesis extends beyond the included benchmarks.
  • A linear-logic or lifetime-based type system could make borrow annotations static, eliminating the need for the inference fixpoint and potentially removing the runtime tag checks.
  • Because the scheme does not handle cyclic data, extending it to languages with cycles would require layering a cycle collector on top; the paper notes the orthogonality but does not build that extension.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 5 minor

Summary. This paper proposes a reference-counting memory management scheme for eager purely functional languages, implemented in the next Lean compiler. The authors introduce λpure and λRC, where λRC extends λpure with explicit inc/dec instructions and a reset/reuse pair that allows a nonshared constructor cell to be reused for a later constructor allocation, effectively performing destructive updates in pure code. They also propose borrowed parameters to reduce reference-count traffic, a heuristic for inferring borrow annotations, a thread-safe RC design based on tagging values as single-threaded, multi-threaded, or persistent, and destructive-update support for arrays and strings. Finally, they report benchmark comparisons of Lean against GHC, ocamlopt, MLton, MLKit, and Swift, concluding that the approach is competitive and often faster.

Significance. If the reset/reuse mechanism is sound, the paper makes a useful contribution: it gives a clean formal account of reuse-based reference counting in a purely functional setting, shows how borrow annotations can be inferred automatically, and provides a low-cost thread-safety scheme that avoids memory fences for single-threaded values. The experiments, though preliminary, cover representative compiler and proof-assistant workloads, report 50-run means with variance markers, and link to the source code. The paper is also honest in Section 10 about the absence of a formal correctness proof. However, the same-arity reuse rule creates a concrete memory-safety risk for the real IR with unboxed fields; until that issue is resolved, the central competitiveness claim rests on an unsound optimization.

major comments (1)
  1. [Sections 4, 5.1, and 7.1] The reset/reuse transformation as presented is not memory-safe for the real IR described in the paper. In Figure 3, the substitution rule S replaces any `ctor_i y` with `reuse w in ctor_i y` whenever `|y| = n`, and the Reuse-Uniq rule in Figure 2 requires only `σ(l) = (ctor_j |y|, 1)`. However, Section 7.1 states that a ctor cell's layout is determined by the number of pointer fields and the number of scalar bytes stored in the header, so two constructors with the same arity can have different cell sizes. For example, `A.mk : UInt8 -> UInt8 -> A` and `B.mk : String -> String -> B` both have arity 2, and a function that matches `A.mk a b` and then constructs `B.mk s1 s2` from dead `a` and `b` would, under the rule, reuse the smaller A cell for the larger B cell, overflowing the allocation. The text in Section 4 says reuse "asserts that its size is compatible with the old cell," but no such check appears in the semantics or in the insertion heuristic, and no invariant relating arity to layout is supplied. This is load-bearing because the claimed performance advantages of reset/reuse depend on it; the rule must be restricted to constructors whose full layout is equal, or extended with a runtime size check and allocation fallback, or the formal model must be extended with scalar field sizes and a proof that the insertion heuristic preserves layout compatibility.
minor comments (5)
  1. [Section 5.3] The tail-call-preservation refinement is described in prose, but the algorithm in Figure 5 as written would still insert `dec y2` after the call in the `f` example; please state the refinement as an explicit modification of the borrow-inference fixpoint or add it to Figure 5.
  2. [Section 7.2] The proposed primitive `asMTg` is introduced without a definition or status; if it is only a potential future extension, mark it as such.
  3. [Section 8, Figures 6 and 7] The normalized tables are dense and the squiggle notation is explained only in the caption; please provide absolute Lean baseline times and describe the variance measure in the text.
  4. [Section 10] The admission that the formal correctness proof is future work is appropriate, but the introduction and abstract should qualify "implements" accordingly, since the formal semantics in Figures 1-2 and the compiler in Figures 3-5 are not yet connected by a theorem.
  5. [Section 2] The inline code has formatting typos such as "lety = reset x" and "reusey in ctori w"; please correct them.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the RC optimization pipeline is defined against a fixed IR, the borrow/reuse heuristics are not fitted to the benchmarks, and the performance claims are validated against external compilers.

full rationale

The paper's central derivation is the compilation from λpure to λRC via three independent transformation steps (reset/reuse insertion, borrow inference, inc/dec insertion). These transformations are defined by algorithms on IR syntax (Figures 3–5) and do not take benchmark outcomes or measured runtimes as inputs. The main experimental claim, competitiveness against GHC, ocamlopt, MLton, MLKit, and Swift, is a comparison against external systems using fixed benchmark programs, so the claimed result is not defined in terms of the measurements. The only explicit empirical premise is the 'resurrection hypothesis' (Section 1), which is stated as a motivating assumption rather than derived from the paper's own equations, and the evaluation in Section 8 directly tests it through rbmap, const_fold, and unionfind. Self-citations (e.g., de Moura et al. 2015 for Lean, Ebner et al. 2017 for metaprogramming) are contextual and not load-bearing for the optimization claims. No equation in the paper defines a predicted quantity in terms of an earlier fitted parameter, and the borrow heuristic is not tuned to the experimental data. The reviewer's concern about same-arity reuse with unboxed fields is a correctness/soundness risk, not a circularity of the derivation chain, and therefore does not affect the circularity score.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

No numeric free parameters are fitted: the borrow inference and reset/reuse heuristics are qualitative, and the resurrection hypothesis is not tuned to the measurements. The central proof obligations are domain assumptions: acyclicity makes cycle handling unnecessary, the resurrection hypothesis makes reuse profitable, and the borrow and reuse-size invariants are needed for soundness. No new physical or ontological entities are introduced; the contributions are algorithmic and implemented in a compiler.

assumptions (5)
  • domain assumption Lean and lambda-pure cannot create cyclic or self-referential data structures.
    Stated in Section 1 and Section 3; it removes the cycle-collection objection to reference counting and is essential for dec to eventually free values and for reset/reuse to be sound.
  • domain assumption Resurrection hypothesis: many objects die just before the creation of an object of the same kind.
    Stated in Section 1 as motivation for reset/reuse. If workloads do not show this liveness pattern, the optimization yields no benefit and the measured speedups on rbmap, unionfind, and const_fold would not generalize.
  • domain assumption Borrowed references are assumed to be kept alive by a surrounding owned reference.
    Introduced in Section 2 and formalized in Section 5.2; the soundness of omitting inc/dec when a parameter is marked borrowed rests on this invariant, and the compiler must ensure borrowed values are not used beyond the owned reference's lifetime.
  • domain assumption The reuse instruction asserts that the new constructor has size compatible with the old cell.
    In Section 4, reuse x in ctori y requires the old cell to be reusable with a compatible size. The generated compiler must only pair reset and reuse with matching arities, otherwise the semantics is undefined.
  • domain assumption Immutable values make single-threaded, multi-threaded, and persistent value tags stable while reachable from a thread.
    Section 7.2; the markMT procedure avoids store barriers because immutability means no mutable store can race with tag transitions. If values were mutable, the tagging scheme would need additional synchronization.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming." pith.science (2026). https://pith.science/paper/I5YWDV53

@misc{pith2026190805647,
  author       = {Pith},
  title        = {Pith review of: Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/I5YWDV53}},
  note         = {Machine review of arXiv:1908.05647}
}
read the original abstract

Most functional languages rely on some garbage collection for automatic memory management. They usually eschew reference counting in favor of a tracing garbage collector, which has less bookkeeping overhead at runtime. On the other hand, having an exact reference count of each value can enable optimizations, such as destructive updates. We explore these optimization opportunities in the context of an eager, purely functional programming language. We propose a new mechanism for efficiently reclaiming memory used by nonshared values, reducing stress on the global memory allocator. We describe an approach for minimizing the number of reference counts updates using borrowed references and a heuristic for automatically inferring borrow annotations. We implemented all these techniques in a new compiler for an eager and purely functional programming language with support for multi-threading. Our preliminary experimental results demonstrate our approach is competitive and often outperforms state-of-the-art compilers.

Figures

Figures reproduced from arXiv: 1908.05647 by the authors.

Figure 1
Figure 1. λRC semantics: the λpure fragment 5 A COMPILER FROM λpure TO λRC Following the actual implementation of our compiler, we will dis￾cuss a compiler from λpure to λRC in three steps: (1) Inserting reset/reuse pairs (Section 5.1) (2) Inferring borrowed parameters (Section 5.2) (3) Inserting inc/dec instructions (Section 5.3) The first two steps are optional for obtaining correct λRC pro￾grams. 5.1 Inserting destructive … view at source ↗
Figure 2
Figure 2. λRC semantics cont. w is a fresh variable introduced by R as the result of a new reset operation. For each arm Fi in a case x of F operation, the function R requires the arity n of the corresponding matched constructor. In the actual implementation, we store this information for each arm when we compile our typed frontend language into λpure. The auxiliary functions D and S implement the dead variable search and sub… view at source ↗
Figure 4
Figure 4. Collecting variables that should not be marked as [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figures from the paper (3 more)
Figure 5
Figure 5. Figure 5: Inserting inc/dec instructions • O − x decrements x if it is both owned and dead. O −(x, F, βl ) decrements multiple variables, which may be needed at the start of a function or case branch. O − x (F, βl ) = dec x; F if βl (x) = O ∧ x < FV(F ) O − x (F, βl ) = F otherw…
Figure 6
Figure 6. Figure 6: Lean variant benchmarks, normalized by the base [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]
Figure 7
Figure 7. Figure 7: Cross-language benchmarks. The measurements include wall clock time (normalized by the Lean base run time), GC [PITH_FULL_IMAGE:figures/full_fig_p011_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

18 extracted references · 13 canonical work pages

  1. [5]

    In Proceedings of the 27th Interna- tional Conference on Parallel Architectures and Compilation Techniques (PACT ’18)

    Biased Reference Counting: Mini- mizing Atomic Operations in Garbage Collection. In Proceedings of the 27th Interna- tional Conference on Parallel Architectures and Compilation Techniques (PACT ’18) . ACM, New York, NY, USA, Article 35, 12 pages. https://doi.org/10.1145/3243176. 3243195 George E. Collins

    work page doi:10.1145/3243176

  2. [15]

    https://doi.org/10.1145/3062341.3062380 J

    ACM, New York, NY, USA, 482–494. https://doi.org/10.1145/3062341.3062380 J. Harold McBeth

    arXiv

  3. [17]

    https://doi.org/10.1145/3133841.3133843 Stephen Weeks

    ACM, New York, NY, USA, 15–26. https://doi.org/10.1145/3133841.3133843 Stephen Weeks

    work page arXiv

  4. [1960]

    A Method for Overlapping and Erasure of Lists. Commun. ACM 3, 12 (Dec. 1960), 655–657. https://doi.org/10.1145/367487.367501 Thierry Coquand and Gérard Huet

    work page arXiv 1960

  5. [1963]

    Letters to the Editor: On the Reference Counter Method. Commun. ACM 6, 9 (Sept. 1963), 575–. https://doi.org/10.1145/367593.367649 James McGraw, Stephen Skedzielewski, Stephen Allan, D Grit, R Oldehoeft, J Glauert, I Dobes, and P Hohensee. 1983.SISAL: streams and iteration in a single-assignment lan- guage. Language reference manual, Version

    work page arXiv 1963

  6. [1977]

    Com- mun

    Shifting Garbage Collection Overhead to Compile Time. Com- mun. ACM 20, 7 (July 1977), 513–518. https://doi.org/10.1145/359636.359713 Johannes Bechberger

    arXiv 1977

  7. [1985]

    InProceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL ’85)

    The Aggregate Update Problem in Functional Programming Systems. InProceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL ’85) . ACM, New York, NY, USA, 300–314. https://doi.org/10.1145/318593.318660 Trevor Jim, J Gregory Morrisett, Dan Grossman, Michael W Hicks, James Cheney, and Yanling Wang

    work page arXiv

  8. [1988]

    The Calculus of Constructions. Inform. and Comput. 76, 2-3 (1988), 95–120. Thierry Coquand and Christine Paulin

    work page 1988

Show all 18 references
  1. [1990]

    In COLOG-88 (Tallinn, 1988)

    Inductively Defined Types. In COLOG-88 (Tallinn, 1988). Lecture Notes in Comput. Sci., Vol

    1988

  2. [1993]

    In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation (PLDI ’93)

    The Essence of Compiling with Continuations. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation (PLDI ’93) . ACM, New York, NY, USA, 237–247. https://doi.org/10.1145/155090.155113 Clemens Grelck and Kai Trojahner

    1993

  3. [1994]

    SIGPLAN Not

    Minimizing Reference Count Updating with Deferred and Anchored Pointers for Functional Data Structures. SIGPLAN Not. 29, 9 (Sept. 1994), 38–43. https://doi.org/10.1145/185009.185016 Jeffrey M. Barth

    1994

  4. [2004]

    InProceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’04)

    The Space Cost of Lazy Reference Counting. InProceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’04). ACM, New York, NY, USA, 210–219. https://doi.org/10.1145/964001. 964019 Joachim Breitner

    doi

  5. [2006]

    In Proceedings of the 2006 Workshop on ML (ML ’06)

    Whole-program Compilation in MLton. In Proceedings of the 2006 Workshop on ML (ML ’06) . ACM, New York, NY, USA, 1–1. https://doi.org/10. 1145/1159876.1159877 Paul R. Wilson

    2006

  6. [2014]

    In Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology (HILT ’14)

    The Rust Language. In Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology (HILT ’14). ACM, New York, NY, USA, 103–104. https://doi.org/10.1145/2663171. 2663188 Luke Maurer, Paul Downen, Zena M. Ariola, and Simon Peyton Jones

    2014 doi

  7. [2015]

    In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, 2015, Proceedings

    The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, 2015, Proceedings. 378–388. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura

    2015

  8. [2016]

    https://doi.org/10.1007/978-3-319-40648-0_12 Cormac Flanagan, Amr Sabry, Bruce F

    Springer-Verlag New York, Inc., New York, NY, USA, 150–165. https://doi.org/10.1007/978-3-319-40648-0_12 Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen

    doi

  9. [2017]

    A Metaprogramming Framework for Formal Verification. Proc. ACM Program. Lang. 1, ICFP (Sept. 2017). https://doi.org/10.1145/3110278 Gaspard Férey and Natarajan Shankar

    2017 doi

  10. [2018]

    Jiho Choi, Thomas Shull, and Josep Torrellas

    A promise checked is a promise kept: Inspection Testing.arXiv preprint arXiv:1803.07130 (2018). Jiho Choi, Thomas Shull, and Josep Torrellas

    2018 arXiv

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.