LoCalMem: Type-directed adaptive serialization for location- and content-addressable memory

Functional programming languages support non-destructive updates via structural sharing, creating a fundamental tradeoff in memory representation: pointer-based heaps preserve sharing but degrade layout locality, while serialized heaps prioritize locality at the cost of duplication. Gibbon addresses this tradeoff by using adaptive serialization: as the program updates its heap, the memory manager improves locality through serialization, falling back to indirection where sharing is unavoidable.

In this work, we formalize key parts of Gibbon's memory model, including the statics and dynamics of adaptive serialization. We then present a unified, type-directed memory model with two realizations: location-addressable memory (LAM) for local execution and content-addressable memory (CAM) for persistence and distributed deduplication. The key abstraction in both models is a notion of explicit boundary datatypes mediating between sharing and serialization. In LAM, boundaries facilitate adaptive serialization and enable our soundness proofs. In CAM, the same boundaries enable an efficient chunking policy, whereby candidate chunk points are selected via rolling-hash cuts. We establish efficiency via a static bound on the number of tokens between consecutive boundaries, bounding reserialization costs.

We work in the purely functional setting, where structural sharing is observationally transparent and content-addressed identity is well defined. We formalize both models with operational semantics and prove soundness with respect to ordinary functional values. For CAM, we prove a locality theorem: the work required for an update scales with the depth of the modified path rather than the size of the value. Consequently, large persistent values can be updated incrementally, with unchanged substructures shared automatically across versions and across machines. Together, these results show that a single boundary discipline can unify local structural sharing and distributed deduplication within one type-theoretic foundation.