When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking

Basic Information

• Paper ID: 2509.04253
• Title: When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
• Authors: Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf (Purdue University, Augusta University)
• Classification: cs.PL (Programming Languages)
• Publication Date: October 10, 2025 (arXiv v2)
• Paper Link: https://arxiv.org/abs/2509.04253

Abstract

Static resource management remains challenging in programming languages, stemming primarily from tensions between controllability, expressiveness, and flexibility. Region-based systems provide bulk deallocation through lexically-scoped regions, but regions and their resources are second-class citizens that cannot escape scope or be freely returned. Ownership and linear type systems, exemplified by Rust, provide non-lexical lifetimes and strong static guarantees, but their underlying invariants restrict higher-order patterns and expressive sharing.

This work proposes a novel type system that unifies these advantages. The system treats all heap-allocated resources as first-class values while allowing programmers to control lifetimes and granularity through three allocation modes: (1) fresh allocation of individual non-lexical references; (2) co-allocation of collectively grouped resources within shadow arenas; (3) scoped allocation with lexically-bounded lifetimes following stack discipline. Regardless of allocation mode, all resources share a unified type, indistinguishable in generic abstractions, preserving the language's higher-order parametric properties.

Research Background and Motivation

Problem Definition

The core problem this research addresses is implementing safe, flexible, and controllable resource management in higher-order functional languages. Traditional approaches face the following dilemmas:

1. Stack vs. Heap Allocation Trade-off: Stack values have strict lexical lifetimes, are safe and efficient but are inherently second-class citizens; heap allocation produces freely flowing first-class values but sacrifices predictable deallocation control.
2. Limitations of Existing Systems:
   • Region-based systems (e.g., MLKit, Cyclone): provide bulk deallocation but regions and resources are second-class citizens
   • Ownership type systems (e.g., Rust): provide non-lexical lifetimes but restrict higher-order patterns and expressive sharing
   • Reachability type systems: support higher-order functions but are constrained by telescope structures, unable to handle cyclic storage structures

Research Motivation

The authors aim to unify the advantages of different resource management strategies: the safety of stack discipline, the expressiveness of higher-order languages, and the flexibility of treating resources as first-class entities.

Core Contributions

1. Unified Resource Handling: All memory resources are first-class values with a single reference type, abstracting stack and heap allocation, allowing client code to remain generic with respect to the specific storage model of references.
2. Flexible Control: Memory resources can be made non-lexical or lexical through user control, can be individual or collective, with no type distinction.
3. Static Safety Guarantees: Reachability types track memory resource flow and ensure safe usage; users can impose selective stack discipline through flow-insensitive reasoning to guarantee predictable deallocation and freedom from use-after-free errors.
4. Expressive Higher-Order Features: The system supports higher-order functions with mutable sharing and cyclic storage structures, surpassing the expressiveness of previous reachability systems.

Methodology Details

Core Concepts

1. Shadow Arenas

Shadow arenas are the key innovation of the system with the following characteristics:

• Implicit Identification: Arenas have no explicit names or constructors in surface syntax, identified implicitly through references
• Three Allocation Forms:

  val fr = new Ref(42)           // fresh allocation
  val ar = new Ref(42) scoped    // scoped allocation  
  val a1 = new Ref(42) at ar     // co-allocation
  

2. Coarse-Grained Reachability Tracking

The system employs a two-dimensional storage model where each reference is indexed by arena location and internal offset (ℓ, o):

• Reachability is tracked coarsely at the arena level ℓ
• All objects within the same arena share the same reachability identifier
• Eliminates telescope constraints, supporting arbitrary internal arena object graphs

Type System Design

A^q<: Calculus

The base system extends the F^q<: calculus with:

• Non-lexical Shadow Arenas: supporting references escaping their lexical scope
• Co-allocation Syntax: ref t1 at t2 places new references in existing arenas
• Unified Reference Type: all allocation forms share the Ref[T]^q type

{A}^q<: Calculus

Extends A^q<: adding scoped resource management:

• Scoped Allocation: ref t as x in b creates lexically-bounded references
• Flow-Insensitive Reasoning: ensures safe deallocation through dynamic tracking of local locations
• Bulk Deallocation: automatically deallocates entire arenas at scope end

Technical Innovations

1. Relaxation of Telescope Structures: allows cyclic structures within and across arenas through coarse-grained tracking
2. Unified Type Abstraction: eliminates type distinction between first-class and second-class resources
3. Selective Stack Discipline: provides predictable deallocation while maintaining flow-insensitive reasoning

Experimental Setup

Formal Verification

• Mechanized Proofs: all formal results mechanized in Rocq
• Type Safety: proved progress and preservation theorems
• Memory Safety: guarantees freedom from use-after-free errors

Case Studies

The paper validates system expressiveness through three case studies:

1. Callback Registration: demonstrates how non-lexical arenas support event-driven programming patterns
2. Generic Fixed-Point Combinator: proves the system overcomes limitations of previous reachability types
3. Cyclic Storage Structures: demonstrates safe construction and reclamation of multi-hop cycles

Experimental Results

Main Results

Type Safety Proofs

Theorem 4.1 (Progress): If [∅ | Σ] φ ⊢ t : Q and Σ ok,
then t is a value or there exist t', σ' such that t | σ → t' | σ'

Theorem 4.2 (Preservation): If a well-typed term reduces,
then there exists an extended type environment such that the 
reduction result remains well-typed

Expressiveness Enhancement

Comparison with existing systems shows this system achieves the intersection of the following features:

• ✓ Stack discipline
• ✓ Expressive sharing
• ✓ First-class resources
• ✓ Higher-order functions

This is the first work implementing all these properties in a unified system.

Case Analysis

Callback Registration Pattern

val makeHandler = {
  val rp = new Ref() // non-lexical resource pool
  (cb: Int => Unit) => {
    val h = new Ref(cb) at rp
    h // return handler
  }
}

Demonstrates how non-lexical arenas manage callback lifetimes.

Cyclic Structure Handling

{ // scope begins
  val a = new Ref() scoped
  val c1, c2, c3 = new Ref(f) at a
  c1 := x => { (!c2)(x) } // form cycle
  c2 := x => { (!c3)(x) }
  c3 := x => { (!c1)(x) }
} // bulk deallocation of {a, c1, c2, c3}

Demonstrates safe construction and deallocation of cyclic reference structures.

Related Work

Region/Arena Systems

• MLKit: implicit region management in functional languages
• Cyclone: explicit regions and existential types in C-style languages
• Linear Regions: combining linear types and region concepts

Ownership and Linear Types

• Rust: unique ownership and single mutable access paths
• Pony: implicit regions and fractional capabilities
• Vergio: ownership combined with explicit regions

Reachability Types

• F^q<:: polymorphic reachability type system
• λ^◦: extension supporting self-cycles
• Capture Types: effect safety system in Scala

Conclusions and Discussion

Main Conclusions

The paper successfully unifies reachability types, arena-based resource management, and stack discipline, providing a lightweight and expressive foundation for safe resource management in higher-order languages.

Limitations

1. Cyclic Construction Constraints: while supporting cyclic structures, requires at least two cells
2. Flow-Sensitive Extensions: explicit deallocation still requires additional flow-sensitive effect extensions
3. Implementation Complexity: the two-dimensional storage model increases runtime implementation complexity

Future Directions

1. Performance Optimization: investigating efficient implementations of the two-dimensional storage model
2. Concurrency Extensions: extending the system to concurrent settings
3. Practical Language Integration: implementing the system in actual programming languages

In-Depth Evaluation

Strengths

1. Significant Theoretical Contribution: first to achieve the intersection of stack discipline, expressive sharing, first-class resources, and higher-order functions in a unified system
2. Outstanding Technical Innovation: shadow arenas and coarse-grained reachability tracking are important innovations
3. Formal Rigor: complete mechanized proofs enhance result credibility
4. Enhanced Expressiveness: overcomes telescope structure limitations of previous reachability type systems

Weaknesses

1. Limited Practical Applicability: not yet implemented in actual languages, practical value remains to be verified
2. Insufficient Performance Considerations: lacks analysis of performance impact of the two-dimensional storage model
3. Steep Learning Curve: system complexity may affect programmer adoption

Impact

This work has significant importance in programming language theory, providing new theoretical foundations for resource management and potentially influencing future programming language design. Particularly for systems programming requiring precise resource control, this approach offers new possibilities.

Applicable Scenarios

1. Systems Programming: low-level systems requiring precise memory management
2. Embedded Systems: safe programming in resource-constrained environments
3. Functional Languages: higher-order functional languages requiring resource management capabilities
4. Concurrent Systems: safe resource sharing in multi-threaded environments

References

The paper cites important works in programming language theory, including:

• Grossman et al. 2002: Cyclone region systems
• Tofte et al. 2001: MLKit region inference
• Wei et al. 2024: polymorphic reachability types
• Clarke et al. 2013: Rust ownership types
• Bao et al. 2021: foundational reachability type theory