Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Type Universes as Allocation Effects

Paulette Koronkevich, William J. Bowman

TL;DR

The paper links type universe hierarchies to memory allocation by treating universes as heap regions that govern where values are allocated, introducing the simply-typed λ-calculus λ_PR with higher-order references. It proves termination for a predicative universe hierarchy using a step-indexed logical-relations model with worlds and a lowering operation that acts as semantic garbage collection, thereby preventing cycles in the heap. It then extends the framework with an impredicative base universe to permit full-ground references and explores universe polymorphism to enable fine-grained region-based memory management, suggesting a general declarative approach to allocation reasoning and potential new language designs for memory safety and Low-level memory reasoning.

Abstract

In this paper, we explore a connection between type universes and memory allocation. Type universe hierarchies are used in dependent type theories to ensure consistency, by forbidding a type from quantifying over all types. Instead, the types of types (universes) form a hierarchy, and a type can only quantify over types in other universes (with some exceptions), restricting cyclic reasoning in proofs. We present a perspective where universes also describe \emph{where} values are allocated in the heap, and the choice of universe algebra imposes a structure on the heap overall. The resulting type system provides a simple declarative system for reasoning about and restricting memory allocation, without reasoning about reads or writes. We present a theoretical framework for equipping a type system with higher-order references restricted by a universe hierarchy, and conjecture that many existing universe algebras give rise to interesting systems for reasoning about allocation. We present 3 instantiations of this approach to enable reasoning about allocation in the simply typed $λ$-calculus: (1) the standard ramified universe hierarchy, which we prove guarantees termination of the language extended with higher-order references by restricting cycles in the heap; (2) an extension with an \emph{impredicative} base universe, which we conjecture enables full-ground references (with terminating computation but cyclic ground data structures); (3) an extension with \emph{universe polymorphism}, which divides the heap into fine-grained regions.

Type Universes as Allocation Effects

TL;DR

The paper links type universe hierarchies to memory allocation by treating universes as heap regions that govern where values are allocated, introducing the simply-typed λ-calculus λ_PR with higher-order references. It proves termination for a predicative universe hierarchy using a step-indexed logical-relations model with worlds and a lowering operation that acts as semantic garbage collection, thereby preventing cycles in the heap. It then extends the framework with an impredicative base universe to permit full-ground references and explores universe polymorphism to enable fine-grained region-based memory management, suggesting a general declarative approach to allocation reasoning and potential new language designs for memory safety and Low-level memory reasoning.

Abstract

In this paper, we explore a connection between type universes and memory allocation. Type universe hierarchies are used in dependent type theories to ensure consistency, by forbidding a type from quantifying over all types. Instead, the types of types (universes) form a hierarchy, and a type can only quantify over types in other universes (with some exceptions), restricting cyclic reasoning in proofs. We present a perspective where universes also describe \emph{where} values are allocated in the heap, and the choice of universe algebra imposes a structure on the heap overall. The resulting type system provides a simple declarative system for reasoning about and restricting memory allocation, without reasoning about reads or writes. We present a theoretical framework for equipping a type system with higher-order references restricted by a universe hierarchy, and conjecture that many existing universe algebras give rise to interesting systems for reasoning about allocation. We present 3 instantiations of this approach to enable reasoning about allocation in the simply typed -calculus: (1) the standard ramified universe hierarchy, which we prove guarantees termination of the language extended with higher-order references by restricting cycles in the heap; (2) an extension with an \emph{impredicative} base universe, which we conjecture enables full-ground references (with terminating computation but cyclic ground data structures); (3) an extension with \emph{universe polymorphism}, which divides the heap into fine-grained regions.
Paper Structure (8 sections, 1 theorem, 11 equations, 6 figures)

This paper contains 8 sections, 1 theorem, 11 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Type Universes for Acyclic Heaps
  3. Proof of Termination
  4. Interpretations and Our Framework
  5. A Universe Hierarchy with Impredicativity
  6. Type Universe Level Polymorphism
  7. Conclusion
  8. Acknowledgments

Key Result

theorem 1

If $\Gamma \vdash e : \tau$ and $\tau :: \<Type>_i$, then $\forall \gamma \in \mathcal{G}|[ \Gamma |](\mathbf{W}) . \gamma(e) \in \mathcal{E}|[ \tau |]_i(\mathbf{W})$.

Figures (6)

  • Figure 1: $\lambda_{\text{PR}}$ syntax
  • Figure 2: $\lambda_{\text{PR}}$ typing.
  • Figure 3: $\lambda_{\text{PR}}$ kinding.
  • Figure 4: Value relation for reference and function types.
  • Figure 5: Additional definitions for worlds.
  • ...and 1 more figures

Theorems & Definitions (1)

  • theorem 1