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
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.
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.
External (18)
- The rust language (2014)
- Coeffects: a calculus of context-dependent computation (2014)
- Algorithmic Games for Full Ground References (2012)
- Crude but effective stratification (2011)
- On Stratified Regions (2009)
- Typing termination in a higher-order concurrent imperative language (2007)
- L3: A Linear Language with Locations (2007)
- Logical relations and a case study in equivalence checking (2005)
- Semantics of types for mutable state (2004)
- Extending the Calculus of Constructions with Type:Type (2004)
- Region-based Memory Management (1997)
- Typing in Pure Type Systems (1993)
- Type Checking with Universes (1991)
- An extended calculus of constructions (1990)
- The Mechanical Evaluation of Expressions (1964)
- Letters to the editor: on the reference counter method (1963)
- Universe levels (Agda reference manual)
- Polymorphic universes (Coq reference manual)