How to keep your neighbours in order

Tools

McBride, Conor; (2014) How to keep your neighbours in order. In: ICFP '14 Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. ACM, New York, NY., pp. 297-309. ISBN 9781450328739 (https://doi.org/10.1145/2628136.2628163)

[thumbnail of McBride-ICFP-2014-How-to-keep-your-neighbours-in-order]
Preview
 Text. Filename: McBride_ICFP_2014_How_to_keep_your_neighbours_in_order.pdf
Accepted Author Manuscript
Download (283kB)| Preview

Abstract

I present a datatype-generic treatment of recursive container types whose elements are guaranteed to be stored in increasing order, with the ordering invariant rolled out systematically. Intervals, lists and binary search trees are instances of the generic treatment. On the journey to this treatment, I report a variety of failed experiments and the transferable learning experiences they triggered. I demonstrate that a total element ordering is enough to deliver insertion and flattening algorithms, and show that (with care about the formulation of the types) the implementations remain as usual. Agda's instance arguments and pattern synonyms maximize the proof search done by the typechecker and minimize the appearance of proofs in program text, often eradicating them entirely. Generalizing to indexed recursive container types, invariants such as size and balance can be expressed in addition to ordering. By way of example, I implement insertion and deletion for 2-3 trees, ensuring both order and balance by the discipline of type checking.

ORCID iDs

McBride, Conor ORCID logoORCID: https://orcid.org/0000-0003-1487-0886;
CORE (COnnecting REpositories)