$\text{TT}^{\Box}_{\mathcal C}$: a Family of Extensional Type Theories with Effectful Realizers of Continuity
Liron Cohen, Vincent Rahli
TL;DR
This paper introduces TT^Box_C, a family of effectful, extensional type theories with a forcing interpretation parameterized by modalities and time-progressing choice operators. It identifies a concrete subtheory that internally realizes Brouwer-style continuity by computing the modulus of continuity via stateful realizers based on reference cells, enabling an internalization of the modulus within the language. The continuity result hinges on a carefully designed forcing semantics, a purity-restricted realizer, and a trio of steps showing the modulus is a natural number, is the maximal such value encountered, and acts as a modulus for functionals on the Baire space. The work advances the understanding of how effectful computations can underpin constructive continuity principles and provides a unified framework to compare classical- and intuitionistic-leaning instantiations of forcing modalities. It also situates these results within the broader landscape of forcing, dialog-tree models, and prior continuity proofs, while highlighting future directions for broader effect systems and inductive continuity principles.
Abstract
$\text{TT}^{\Box}_{\mathcal C}$ is a generic family of effectful, extensional type theories with a forcing interpretation parameterized by modalities. This paper identifies a subclass of $\text{TT}^{\Box}_{\mathcal C}$ theories that internally realizes continuity principles through stateful computations, such as reference cells. The principle of continuity is a seminal property that holds for a number of intuitionistic theories such as System T. Roughly speaking, it states that functions on real numbers only need approximations of these numbers to compute. Generally, continuity principles have been justified using semantical arguments, but it is known that the modulus of continuity of functions can be computed using effectful computations such as exceptions or reference cells. In this paper, the modulus of continuity of the functionals on the Baire space is directly computed using the stateful computations enabled internally in the theory.