一句话：为证明助手提出 sort 多态及其元理论，并在 Coq 中实现，解决跨种类定义复用与扩展问题。
基于依赖类型论的证明助手（如 Coq、Lean、Agda）用多个宇宙分类类型，包括可计算类型的预测式层级与证明无关命题的非预测式宇宙。每个宇宙由种类（Type、Prop 等）和层级刻画；近期研究引入更多种类以结构化处理不同逻辑/计算原则（如 univalence、异常、定义性证明无关）。但现有证明助手对种类间多态的支持是特设且受限的，导致定义难以复用和扩展。本文提出 sort polymorphism（种类多态）及其元理论，重点研究单态化、大消除与参数性；在 Coq 中实现该机制，并给出基于新种类多态 prelude 的基础定义与自动化示例。该方案有效克服当前局限，为未来多种类类型论奠定基础。
Proof assistants based on dependent type theory, such as Coq, Lean and Agda, use different universes to classify types, typically combining a predicative hierarchy of universes for computationally-relevant types, and an impredicative universe of proof-irrelevant propositions. In general, a universe is characterized by its sort, such as Type or Prop, and its level, in the case of a predicative sort. Recent research has also highlighted the potential of introducing more sorts in the type theory of the proof assistant as a structuring means to address the coexistence of different logical or computational principles, such as univalence, exceptions, or definitional proof irrelevance. This diversity raises concrete and subtle issues from both theoretical and practical perspectives. In particular, in order to avoid duplicating definitions to inhabit all (combinations of) universes, some sort of polymorphism is needed. Universe level polymorphism is well-known and effective to deal with hierarchies, but the handling of polymorphism between sorts is currently ad hoc and limited in all major proof assistants, hampering reuse and extensibility. This work develops sort polymorphism and its metatheory, studying in particular monomorphization, large elimination, and parametricity. We implement sort polymorphism in Coq and present examples from a new sort-polymorphic prelude of basic definitions and automation. Sort polymorphism is a natural solution that effectively addresses the limitations of current approaches and prepares the ground for future multi-sorted type theories.
@article{paperbot3224,
title = {All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants},
author = {Josselin Poiret and Gaëtan Gilbert and Kenji Maillard and Pierre-Marie Pédrot and Matthieu Sozeau and Nicolas Tabareau and Éric Tanter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704912}
}