Classical (Co)Recursion: Programming

TL;DR

This paper explores how structural corecursion, traditionally used in pure functional languages, can be applied across various programming paradigms and languages, enhancing expressiveness especially when combined with effects.

Contribution

It demonstrates the adaptation of structural corecursion to multiple languages including Scheme, Python, and Java, and shows how effects can expand its capabilities.

Findings

Corecursion can be implemented in strict functional languages like Scheme.

Combining corecursion with effects increases its expressive power.

Classical corecursion enables new stream-processing algorithms.

Abstract

Our aim here is to illustrate how the benefits of structural corecursion can be found in a broader swath of the programming landscape than previously thought. Beginning from a tutorial on structural corecursion in the total, pure functional language Agda, we show how these same ideas are mapped to familiar concepts in a variety of different languages. We show how corecursion can be done in strict functional languages like Scheme, and even escapes the functional paradigm entirely, showing up in the natural expression of common object-oriented features found in languages like Python and Java. Opening up structural corecursion to a much wider selection of languages and paradigms -- and therefore, also to a much larger audience of programmers -- lets us also ask how corecursion interacts with computational effects. Of note, we demonstrate that combining structural corecursion with effects can increase its expressive power. We show a classical version of corecursion -- using first-class control made possible by Scheme's classical call/cc -- that enables us to write some new stream-processing algorithms that aren't possible in effect-free languages.