On November 3, I gave a talk named “Programming and Proving with Guarded Recursion” at the PSSV’23 workshop on a topic I’ve been working intensively on for the last couple of months - guarded recursion. I’ll make a short synopsis here; more details are found in the slides and the GitHub repo.
Briefly, the idea of guarded recursion can be characterized as the calculus of thunks; it goes back to modal logics of provability (Gödel-Löb system and similar ones). In the guarded type system, the deferred computation returning A is denoted as ▷A. This type constructor is equipped with the structure of an applicative functor, i.e., as basic operations, we can defer the computation for one step (next : A → ▷A) and apply a function to an argument at the next step (ap : ▷(A → B) → ▷A → ▷B). The main working construction, however, is the (unique) guarded fixed point operator fix : (▷A → A) → A. From a programmer’s point of view, it behaves like a recursion that returns control to the caller after each iteration, which allows total algorithms to be written in a productive form, i.e., as potentially infinite series of terminating computations that can be interrupted after each step. Potentially infinite computations are ubiquitous in practice - they are all sorts of server-side programs and streaming data transformations.
Classical structures that can be defined using guarded recursion are:
- infinite streams
- co-lists (i.e., sequences that can be both finite and infinite)
- extended Peano numbers (where we have a term denoting ∞)
- the so-called partiality monad (i.e., some value whose acquisition is delayed for an indefinite number of steps, from 0 to ∞)
Applications of deferred recursion can be conceptually divided into two classes: working with infinite structures directly and encoding non-strictly positive recursive types. As a representative of the first class, we can refer to the definition and verification of Bird’s replaceMin algorithm and its further generalizations to MonadFix / value recursion. Non-strictly positive definitions can be demonstrated by the example of Hofmann’s algorithm for breadth-first tree traversal; in general, such constructions (+ the partiality monad mentioned above) often come up when working with models of PLs by the method of logical relations and constructing denotational semantics. These ideas are the basis of a young branch of PLT called (synthetic) guarded domain theory, where any type is simultaneously a domain - this allows the work to be simplified considerably, eliminating numerous proofs of “domainness”.
It is worth noting that using the guarded modality alone severely restricts the possibility of manipulating thunks. On the one hand, such a ubiquitous type-based control is convenient. Classical approaches to dealing with infinite structures in proof-assistants, such as coinductive mechanisms, suffer from a lack of compositionality - since productivity checking used in them works syntactically, this regularly leads to a situation where the proof-engineer receives an error about a violation of totality only after the completion of a time-consuming proof, which, of course, is quite demoralizing. On the other hand, the coinductive reasoning cannot be entirely reproduced using guards - intuitively, when working with a deferred computation, we can only maintain or increase the degree of its “deferral”; in other words, thunks can never be “collapsed” at the design stage. This limitation can be circumvented by extending the system with special clock variables, quantification by them (a particular case of this idea is the so-called “constant” modality), and the force primitive, which allows us to dynamically run chunks of deferred computation in contexts safe for this purpose.