A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures

TL;DR

This paper explores how traversals over infinite structures in Haskell can be productive and well-behaved despite non-termination, using guarded recursion and equational reasoning.

Contribution

It introduces a framework for understanding traversals over infinite data structures in non-strict Haskell, leveraging guarded recursion to ensure productivity.

Findings

Traversals can operate over infinite structures productively.

Guarded recursion enables reasoning about infinite traversals.

Infinite traversals can yield finite, terminating results in certain contexts.

Abstract

Functors with an instance of the Traversable type class can be thought of as data structures which permit a traversal of their elements. This has been made precise by the correspondence between traversable functors and finitary containers (also known as polynomial functors) -- established in the context of total, necessarily terminating, functions. However, the Haskell language is non-strict and permits functions that do not terminate. It has long been observed that traversals can at times in fact operate over infinite lists, for example in distributing the Reader applicative. The result of such a traversal remains an infinite structure, however it nonetheless is productive -- i.e. successive amounts of finite computation yield either termination or successive results. To investigate this phenomenon, we draw on tools from guarded recursion, making use of equational reasoning directly in Haskell.