A Generalized Modality for Recursion

TL;DR

This paper introduces a generalized modality for guarded recursion called time warps, expanding the expressive power of existing modalities and enabling more precise modeling of input-output dependencies in recursive functions.

Contribution

It proposes a new, flexible modality for guarded recursion that encompasses existing modalities as special cases, improving expressiveness for programming and type theory.

Findings

Unified existing modalities under a new framework

Enhanced expressiveness for guarded recursive definitions

Applicable to various contexts like functional programming and type theory

Abstract

Nakano's later modality allows types to express that the output of a function does not immediately depend on its input, and thus that computing its fixpoint is safe. This idea, guarded recursion, has proved useful in various contexts, from functional programming with infinite data structures to formulations of step-indexing internal to type theory. Categorical models have revealed that the later modality corresponds in essence to a simple reindexing of the discrete time scale. Unfortunately, existing guarded type theories suffer from significant limitations for programming purposes. These limitations stem from the fact that the later modality is not expressive enough to capture precise input-output dependencies of functions. As a consequence, guarded type theories reject many productive definitions. Combining insights from guarded type theories and synchronous programming languages, we propose a new modality for guarded recursion. This modality can apply any well-behaved reindexing of the time scale to a type. We call such reindexings time warps. Several modalities from the literature, including later, correspond to fixed time warps, and thus arise as special cases of ours.