Reference. Type Universes as Allocation Effects

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 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 impredicative base universe, which we conjecture enables full-ground references (with terminating computation but cyclic ground data structures); (3) an extension with universe polymorphism, which divides the heap into fine-grained regions.

Cite

Cite as @koronkevich-2024-type (helia, typst) · \cite{koronkevich-2024-type} (LaTeX)
BibTeX
bibtex · 8 lines
@misc{koronkevich-2024-type,
  author = {Paulette Koronkevich and William J. Bowman},
  title = {Type Universes as Allocation Effects},
  year = {2024},
  month = {7},
  eprint = {2407.06473},
  archiveprefix = {arXiv}
}
hayagriva YAML (typst)
yaml · 9 lines
koronkevich-2024-type:
  type: misc
  title: Type Universes as Allocation Effects
  author:
  - Koronkevich, Paulette
  - Bowman, William J.
  date: 2024-07
  serial-number:
    arxiv: '2407.06473'
Cited by (1)

From Linearity to Borrowing wagner-2025-from

Linear type systems are powerful because they can statically ensure the correct management of resources like memory, but they can also be cumbersome to work with, since even benign uses of a resource require that it be explicitly threaded through during computation. Borrowing , as popularized by Rust, reduces this burden by allowing one to temporarily disable certain resource permissions (e.g., deallocation or mutation) in exchange for enabling certain structural permissions (e.g., weakening or contraction). In particular, this mechanism spares the borrower of a resource from having to explicitly return it to the lender but nevertheless ensures that the lender eventually reclaims ownership of the resource. In this paper, we elucidate the semantics of borrowing by starting with a standard linear type system for ensuring safe manual memory management in an untyped lambda calculus and gradually augmenting it with immutable borrows, lexical lifetimes, reborrowing, and finally mutable borrows. We prove semantic type soundness for our Borrow Calculus ( BoCa ) using Borrow Logic ( BoLo ), a novel domain-specific separation logic for borrowing. We establish the soundness of this logic using a semantic model that additionally guarantees that our calculus is terminating and free of memory leaks. We also show that our Borrow Logic is robust enough to establish the semantic safety of some syntactically ill-typed programs that temporarily break but reestablish invariants.
PDF · DOI · pldb
Cites 19 works (1 here)
With notes (1)

An Order-Theoretic Analysis of Universe Polymorphism houfavonia-2023-an

We present a novel formulation of universe polymorphism in dependent type theory in terms of monads on the category of strict partial orders, and a novel algebraic structure, displacement algebras, on top of which one can implement a generalized form of McBride’s “crude but effective stratification” scheme for lightweight universe polymorphism. We give some examples of exotic but consistent universe hierarchies, and prove that every universe hierarchy in our sense can be embedded in a displacement algebra and hence implemented via our generalization of McBride’s scheme. Many of our technical results are mechanized in Agda, and we have an OCaml library for universe levels based on displacement algebras, for use in proof assistant implementations.
PDF · DOI · pldb
External (18)
koronkevich-2024-type reference entries/refs/koronkevich-2024-type/koronkevich-2024-type.hel