How to keep your neighbours in order

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

58 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationICFP '14 Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming
Place of PublicationNew York, NY.
Number of pages14
Publication statusPublished - 19 Aug 2014


  • agda
  • balancing
  • dependent types
  • ordering
  • sorting
  • binary trees
  • computer programming languages
  • containers
  • generic treatment
  • learning experiences


Dive into the research topics of 'How to keep your neighbours in order'. Together they form a unique fingerprint.

Cite this