一句话：为 sort 多态引入带界的 sort 变量与消去约束，恢复多排序类型论的表达力与主类型推断。
本文关注依赖类型论证明助手（如 Agda、Lean、Rocq）中 sort 多态的表达力不足问题。现有 sort 多态采用无界形式，无法用单一多态 schema 抽象出跨 sort 的合法定义：例如从无关（proof-irrelevant）sort 消去到相关（relevant）sort 的泛型函数无法多态化，封装不同 sort 属性的多态记录也无法定义，并且破坏了主类型推断。作者提出扩展 sort 多态，为 sort 变量加上反映所需消去约束的界，从而精确控制不同 sort 之间的交互以保证可靠性。文章给出了有界 sort 多态的元理论，特别分析了所得约束图的一致性，并在 Rocq 证明助手中实现该机制。通过具体示例，作者展示了该设计如何自然、通用地解决现有局限，促进多排序类型论的发展与实验。
Proof assistants based on dependent type theory—such as Agda , Lean , and Rocq —employ different universes to classify types, typically combining a predicative tower for computationally relevant types with a possibly impredicative universe for proof-irrelevant propositions. Several other universes with specific logical and computational principles have been explored in the literature. In general, a universe is characterized by its sort (e.g., Type, Prop, or SProp) and, in the predicative case, by its level. To improve modularity and better avoid code duplication, sort polymorphism has recently been introduced and integrated in the Rocq prover. However, we observe that, due to its unbounded formulation, sort polymorphism is currently insufficiently expressive to abstract over valid definitions with a single polymorphic schema. Indeed, to ensure soundness of a multi-sorted type theory, the interaction between different sorts must be carefully controlled, as exemplified by the forbidden elimination of irrelevant terms to produce relevant ones. As a result, generic functions that eliminate values of inductive types from one sort to another cannot be made polymorphic; dually, polymorphic records that encapsulate attributes of different sorts cannot be defined. This lack of expressiveness also breaks the possibility to infer principal types, which is highly desirable for both metatheoretical and practical reasons. To address these issues, we extend sort polymorphism with bounds that reflect the required elimination constraints on sort variables. We present the metatheory of bounded sort polymorphism, paying particular attention to the consistency of the resulting constraint graph. We implement bounded sort polymorphism in Rocq and illustrate its benefits through concrete examples. Bounded sort polymorphism with elimination constraints is a natural and general solution that effectively addresses current limitations and fosters the development of, and practical experimentation with, multi-sorted type theories.
@article{RosainDMSTTW26,
title = {Bounded Sort Polymorphism with Elimination Constraints},
author = {Johann Rosain and Tomás Díaz and Kenji Maillard and Matthieu Sozeau and Nicolas Tabareau and Éric Tanter and Théo Winterhalter},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776732}
}