  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.
