To exploit the expressivity of being able to refer to the type of types, such as for large elimination, dependent type systems will either employ a universe hierarchy or else contend with an inconsistent type-in-type rule. However, these are not be the only possible options. Taking inspiration from Stratified System F, we introduce Stratified Type Theory (StraTT), where rather than stratifying universes by levels, we stratify typing judgements and restrict the domain of dependent function types to some fixed level strictly lower than that of the overall type. Even in the presence of type-in-type, this restriction suffices to enforce consistency of the system. We explore the expressivity of several extensions atop this design. First, the subsystem subStraTT employs McBride's crude-but-effective stratification (also known as displacement) as a simple form of level polymorphism where top-level definitions can be displaced uniformly to any higher level as needed, which is valid due to level cumulativity and plays well with stratified judgements. Second, to recover some expressivity lost due to the restriction on dependent function domains, the full StraTT system includes a separate nondependent function type with floating domains, whose level instead matches that of the overall type. Finally, we have implemented a prototype type checker for StraTT extended with datatypes along with a small type checked core library. While it's possible to show that the subsystem is consistent, showing consistency for the full system with floating nondependent functions remains open. Nevertheless, we believe that the full system is also consistent and have mechanized a syntactic proof of subject reduction. Furthermore, we use our implementation to investigate various well-known type-theoretic type-in-type paradoxes. These examples all fail to type check in expected ways as evidence towards consistency.

翻译：为了利用能够引用类型之类型（例如用于大消除）的表达能力，依赖类型系统要么采用宇宙层级，要么必须处理不一致的类型-包含-类型规则。然而，这些并非唯一可能的方案。受分层系统F的启发，我们引入了分层类型理论（StraTT）。在该理论中，我们并非按层次对宇宙进行分层，而是对类型判断进行分层，并将依赖函数类型的域限制为严格低于整体类型的固定层级。即使在类型-包含-类型存在的情况下，这一限制也足以确保系统的一致性。我们探索了基于此设计的多种扩展的表达能力。首先，子系统subStraTT采用了McBride的粗略而有效的分层（也称为位移）作为一种简单的层级多态形式，其中顶层定义可根据需要统一位移到任何更高层级。由于层级累积性，这一操作是有效的，并且与分层判断兼容。其次，为了恢复因依赖函数域限制而损失的部分表达能力，完整的StraTT系统包含一个独立的非依赖函数类型，其域可浮动，且层级与整体类型匹配。最后，我们为扩展了数据类型的StraTT实现了一个原型类型检查器，以及一个小型经过类型检查的核心库。虽然能够证明子系统的一致性，但证明具有浮动非依赖函数的完整系统的一致性仍是一个开放问题。尽管如此，我们相信完整系统也是一致的，并机械化地完成了主题归约的语法证明。此外，我们利用实现探讨了各种著名的类型理论中的类型-包含-类型悖论。这些示例均以预期方式类型检查失败，作为一致性的证据。