Impredicativity in Linear Dependent Type Theory
Sam Speight, Niels van der Weide
TL;DR
The paper develops a realizability model of linear dependent type theory (LDTT) from a linear combinatory algebra, introducing an impredicative universe with two decoding operations that map codes to cartesian and linear types. It constructs the model as a linear comprehension category, with M and L mediating between linear and cartesian sides, and proves interpretation of key type formers, equalizers, and an impredicative universe. A central contribution is the impredicative encoding of linear inductive types, demonstrated via a refined initial-algebra construction for lists, supported by a formal Rocq implementation. Together these results provide a rigorous semantic foundation for impredicative LDTT and enable robust encodings of inductive types in linear settings, with potential implications for resource-conscious and quantum programming languages.
Abstract
We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, we add a universe with two decoding operations: one takes codes to cartesian types and the other takes codes to linear types. The universe is impredicative in the sense that it is closed under both large cartesian dependent products and large linear dependent products. We also add a rule for injectivity of the modality turning linear terms into cartesian terms. With all of the additions, we are able to encode (linear) inductive types. As a case study, we consider the type of lists over a linear type, and demonstrate that our encoding has the relevant uniqueness principle. The construction of the realizability model is fully formalized in the proof assistant Rocq.