Contravariant subtyping formalized and mechanized for type theory
Contravariant Universe Subtyping, Formalized, Mechanized
Programming Languages
Summary
Many proof systems use layers of logical types called universes, where bigger universes include smaller ones. Normally, when checking if one type fits into another, these systems only allow the output parts of functions to vary. This paper studies a more flexible way that also allows input types to vary in the opposite way. The authors build formal, computer-checked proofs and complete algorithms to do this advanced kind of checking. Their work helps improve the foundations behind software that verifies mathematical proofs and programs.
What this means in practice
- •For proof assistant developers: Implement a complete and verified subtyping algorithm that supports contravariant input types in universe hierarchies.
- •For program verification teams: Enhance the type checkers of dependently typed languages with advanced universe subtyping, improving expressiveness in formal program proofs.
A theory result. No direct application yet.
Authors
Shengyi Jiang, Jason Z. S. Hu
Abstract
In a type theory with a cumulative universe hierarchy, \emph{subtyping} is often incorporated to lift lower universe levels to higher ones. In practice, kernels of proof assistants typically implement universe subtyping conservatively: subtyping only propagates covariantly into the output types of $Π$ types, while input types must be equivalent. A full-blown subtyping relation also compares the input types contravariantly. However, contravariant subtyping is not justified by the existing set-theoretic model, and poses challenges in the development of a complete subtyping algorithm. We present \mclttsub, a complete mechanized study of contravariant universe subtyping for a core Martin-Löf type theory (MLTT), built as an extension of the verified McTT kernel in Rocq. We re-establish the syntactic meta-theory and the soundness and completeness properties of the normalization-by-evaluation (NbE) algorithm. To complete the verified pipeline for a type-checker, we give two complete and sound subtyping algorithms. The first one \emph{renormalizes} output types in every $Π$ iteration. Despite a simple completeness proof, this algorithm incurs additional computational cost. The second algorithm hence circumvents this cost by avoiding the renormalization at all. It simply recursively compares two already normalized types structurally. Nevertheless, a completeness proof of this algorithm in a semantic approach requires to reason about normalization in sub-contexts, a capability beyond what the current semantic gadget offers. Instead, we conduct a program equivalence proof through bisimulation relations. Using this technique, we prove that the NbE algorithm returns equal normal forms in sub-contexts up to universe levels, and successfully conclude the completeness of the subtyping algorithm.