Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Stratified Type Theory

Jonathan Chan, Stephanie Weirich

TL;DR

Stratified Type Theory (StraTT) replaces traditional universe hierarchies with stratified typing judgments indexed by levels, restricting dependent-function domains to strictly lower levels to preserve consistency even under type-in-type. The framework introduces subStraTT (consistency via Agda) and full StraTT (type safety via Coq), with floating nondependent functions to recover expressivity, and a prototype checker supporting datatypes and level/displacement inference. While full consistency remains an open problem due to cumulativity interactions, the approach provides a concrete path toward alternative foundations for theorem provers and illustrates practical feasibility through a working implementation and extensive metatheoretic discussion. The work situates StraTT as a principled design space between universe polymorphism and fixed hierarchies, offering insights into how levels, displacement, and floating domains can influence usability and consistency in dependently-typed programming.

Abstract

A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent functions and the type-in-type rule. In this work, we argue that a universe hierarchy is not the only option for a type theory with a type universe. Taking inspiration from Leivant's 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 functions to strictly lower levels. Even with type-in-type, this restriction suffices to enforce consistency. In StraTT, we consider a number of extensions beyond just stratified dependent functions. First, the subsystem subStraTT employs McBride's crude-but-effective stratification (also known as displacement) as a simple form of level polymorphism where global definitions with concrete levels can be displaced uniformly to any higher level. Second, to recover some expressivity lost due to the restriction on dependent function domains, the full StraTT includes a separate nondependent function type with a "floating" domain whose level matches that of the overall function type. Finally, we have implemented a prototype type checker for StraTT extended with datatypes and inference for level and displacement annotations, along with a small core library. We have proven subStraTT to be consistent and StraTT to be type safe, but consistency of the full StraTT remains an open problem, largely due to the interaction between floating functions and cumulativity of judgements. Nevertheless, we believe StraTT to be consistent, and as evidence have verified the failure of some well-known type-theoretic paradoxes using our implementation.

Stratified Type Theory

TL;DR

Stratified Type Theory (StraTT) replaces traditional universe hierarchies with stratified typing judgments indexed by levels, restricting dependent-function domains to strictly lower levels to preserve consistency even under type-in-type. The framework introduces subStraTT (consistency via Agda) and full StraTT (type safety via Coq), with floating nondependent functions to recover expressivity, and a prototype checker supporting datatypes and level/displacement inference. While full consistency remains an open problem due to cumulativity interactions, the approach provides a concrete path toward alternative foundations for theorem provers and illustrates practical feasibility through a working implementation and extensive metatheoretic discussion. The work situates StraTT as a principled design space between universe polymorphism and fixed hierarchies, offering insights into how levels, displacement, and floating domains can influence usability and consistency in dependently-typed programming.

Abstract

A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent functions and the type-in-type rule. In this work, we argue that a universe hierarchy is not the only option for a type theory with a type universe. Taking inspiration from Leivant's 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 functions to strictly lower levels. Even with type-in-type, this restriction suffices to enforce consistency. In StraTT, we consider a number of extensions beyond just stratified dependent functions. First, the subsystem subStraTT employs McBride's crude-but-effective stratification (also known as displacement) as a simple form of level polymorphism where global definitions with concrete levels can be displaced uniformly to any higher level. Second, to recover some expressivity lost due to the restriction on dependent function domains, the full StraTT includes a separate nondependent function type with a "floating" domain whose level matches that of the overall function type. Finally, we have implemented a prototype type checker for StraTT extended with datatypes and inference for level and displacement annotations, along with a small core library. We have proven subStraTT to be consistent and StraTT to be type safe, but consistency of the full StraTT remains an open problem, largely due to the interaction between floating functions and cumulativity of judgements. Nevertheless, we believe StraTT to be consistent, and as evidence have verified the failure of some well-known type-theoretic paradoxes using our implementation.
Paper Structure (33 sections, 18 theorems, 29 equations, 4 figures)

This paper contains 33 sections, 18 theorems, 29 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Stratified Type Theory
  3. The subsystem subStraTT
  4. Floating functions
  5. Examples
  6. The identity function
  7. Decidable types
  8. Leibniz equality
  9. Metatheory
  10. Consistency of subStraTT
  11. The problem with floating functions
  12. Type safety of StraTT
  13. Basic properties
  14. Restriction
  15. Restricted floating
  16. ...and 18 more sections

Key Result

Lemma 1

https://github.com/plclub/StraTT/tree/main/coq/restrict.v:DTyping_cumul If $\Delta ; \Gamma \vdash \mathit{a} :^{ \mathit{j} } \mathit{A}$ and $\mathit{j} \leq \mathit{k}$ then $\Delta ; \Gamma \vdash \mathit{a} :^{ \mathit{k} } \mathit{A}$.

Figures (4)

  • Figure 1: Typing rules (subStraTT)
  • Figure 2: Definitional equality rules (subStraTT)
  • Figure 3: Typing and definitional equality rules (floating functions)
  • Figure 4: Call-by-name reduction

Theorems & Definitions (18)

  • Lemma 1: Cumulativity
  • Lemma 2: Displaceability (empty context)
  • Lemma 3: Implementation of definitional equality
  • Lemma 4: Cumulativity
  • Lemma 5: Conversion
  • Lemma 6: Backward preservation
  • Theorem 7: Soundness
  • Corollary 8: Consistency
  • Lemma 11: Weakening
  • Lemma 12: Substitution
  • ...and 8 more