A Realisability Model of Dependent Type Theory with Sizes
Bastiaan Laarakker

Abstract:
Many proof assistants are based on dependent type theories, and extend the theory with support for defining inductive and coinductive types. For their underlying theory to remain consistent and for type checking to be decidable, proof assistants ensure termination of recursive functions and productivity of corecursive functions using syntactic guardedness conditions. This syntactic approach is often too restrictive, limiting the expressiveness of the language. Sized types are a type-based alternative to determining termination or productivity of (co)recursive functions. With sized types, (co)inductive types can be annotated with additional size information, and a well-founded ordering on these sizes is used to prove termination or productivity.
This work investigates the syntax and semantics of sized types. We construct a realisability model for a dependent type theory with a type of sizes and an impredicative universe. We make use of a form of internal parametricity via axioms, describing how sizes should be treated uniformly. These are validated by the model, thereby also showing how realisability models allow for parametric reasoning. Impredicativity lets us derive initial algebras and terminal coalgebras for all polynomial functors via existential and universal quantification over suitable size-indexed (co)algebras, improving on previous work on encoding (co)inductive types using sized types. We also discuss what is needed for a consistent and robust implementation of sized types, and note some connections with guarded type theory, another type-based approach to productivity checking.