# Productive Coprogramming with Guarded Recursion

## Publication Information

Robert Atkey and Conor McBride.

*Productive Coprogramming with Guarded Recursion*. In

*18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013)*. 2013.

DOI:

10.1145/2500365.2500597## Abstract

Total functional programming offers the beguiling vision that, just
by virtue of the compiler accepting a program, we are guaranteed
that it will always terminate. In the case of programs that are not
intended to terminate, e.g., servers, we are guaranteed that
programs will always be *productive*. Productivity means that,
even if a program generates an infinite amount of data, each piece
will generated in finite time. The theoretical underpinning for
productive programming with infinite output is provided by the
category theoretic notion of final coalgebras. Hence, we speak of
*co*programming with non-well-founded *co*data, as a dual
to programming with well-founded data like finite lists and trees.

Systems that offer facilities for productive coprogramming, such as
the proof assistants Coq and Agda, currently do so through syntactic
guardedness checkers. Syntactic guardedness checkers ensure that all
self-recursive calls are guarded by a use of a constructor. Such a
check ensures productivity. Unfortunately, these syntactic checks
are not compositional, and severely complicate coprogramming.

Guarded recursion, originally due to Nakano, is tantalising as a
basis for a flexible and compositional type-based approach to
coprogramming. However, as we show, by itself, guarded recursion is
not suitable for coprogramming due to the fact that there is no way
make finite observations on pieces of infinite data. In this paper,
we introduce the concept of *clock variables* that index
Nakano's guarded recursion. Clock variables allow us to ``close
over'' the generation of infinite data, and to make finite
observations, something that is not possible with guarded recursion
alone.

## Additional Information

Thanks to Edward Z. Yang for spotting the following typos in this paper: **(1)** On page 4, there a lot of instances of `μX. F`

, which should be `μX. F[X]`

, indicating explicitly that the `X`

can appear in `X`

. **(2)** On page 8, in the first displayed formula in the *Co-inductive Streams* section, the last `A`

ought to be an `X`

. So the whole formula ought to be: `Stream A = ∀κ. μX. A × ▷κ X`

. **(3)** Again on page 8, in the display giving the type of `step`

, the first `×`

ought to be a `+`

.