Calculating Datastructures

Where do datastructures come from? This paper explores how to systematically derive implementations of one-sided flexible arrays from a simple reference implementation. Using the dependently typed programming language Agda, each calculation constructs an isomorphic—yet more efficient—datastructure using only a handful of laws relating types and arithmetic. Although these calculations do not generally produce novel datastructures they do give insight into how certain datastructures arise and how different implementations are related.