An Investigation of the Laws of Traversals

TL;DR

This paper explores the algebraic properties of traversable data structures, proposing new laws to better characterize traversals and demonstrating their applicability to finitary containers.

Contribution

It introduces laws that more accurately capture the intuition behind traversals, extending the theoretical understanding of traversable functors.

Findings

Finitary containers are traversable under the proposed laws.

Traversable structures ensure each element is visited exactly once.

The new laws better align with the conceptual intuition of traversals.

Abstract

Traversals of data structures are ubiquitous in programming. Consequently, it is important to be able to characterise those structures that are traversable and understand their algebraic properties. Traversable functors have been characterised by McBride and Paterson as those equipped with a distributive law over arbitrary applicative functors; however, laws that fully capture the intuition behind traversals are missing. This article is an attempt to remedy this situation by proposing laws for characterising traversals that capture the intuition behind them. To support our claims, we prove that finitary containers are traversable in our sense and argue that elements in a traversable structure are visited exactly once.