2012/02/10 by Mauro Jaskelioff, Ondrej Rypacek, Ondřej Rypáček
Computer Science · #Computability, Logic, AI Algorithms #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.PL
paper · pdf · doi:10.4204/eptcs.76.5
published as EPTCS 76, 2012, pp. 40-49 · In Proceedings MSFP 2012, arXiv:1202.2407
openalex publication_date 2012/02/10 · arxiv created 2012/02/14 · arxiv updated 2012/02/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/31
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.