corecursive

Corecursive, or corecursion, is a form of definition in computer science in which a function or specification constructs data rather than consuming it to produce a result. It is the dual of recursion: recursive definitions reduce a problem to simpler subproblems to compute an output, while corecursive definitions unfold a data structure from a given state or seed, potentially producing infinite data. Corecursion is often associated with lazy evaluation or with codata and coinductive types, and it relies on the notion of productivity: each finite portion of the output can be produced in finite steps.

Corecursive data structures are typically infinite or open-ended, such as streams, tapes, or infinite trees. A corecursive function emits the next element and returns a new state, possibly deferring further computation. In lazy languages, corecursive definitions are natural; in strict languages, they may require guarded corecursion or the use of lazily evaluated thunks to maintain productivity.

Examples: generating a stream of consecutive integers:

streamFrom n = n : streamFrom (n+1)

This is corecursive because it builds an infinite list by repeatedly supplying the next element.

Another common pattern is unfold, which builds a data structure from a seed by repeatedly applying a step function, yielding either a final value or a new seed and an emitted element.

In practice, corecursion is used to model ongoing processes, infinite data structures, and reactive systems, and is formalized via coinduction and codata in languages and proof systems such as Coq or Agda.