An Order-Theoretic Analysis of Universe Polymorphism
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 09, 2023
- Source ID
- 10.1145/3571250
Entities
People
- Carlo Angiuli
- Kuen-Bang Hou
- Reed Mullanix
Organizations
- Air Force Office of Scientific Research
- Carnegie Mellon University
- University of Minnesota