Type Universes as Allocation Effects
<|reference_start|>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 \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 $\lambda$-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.<|reference_end|>
@article{koronkevich2024type,
    title={Type Universes as Allocation Effects},
    author={Paulette Koronkevich and William J. Bowman},
    journal={arXiv preprint arXiv:2407.06473},
    year={2024},
    archivePrefix={arXiv},
    eprint={2407.06473},
    primaryClass={cs.PL}
}