How to keep your neighbours in order
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)
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: https://orcid.org/0000-0003-1487-0886;-
-
Item type: Book Section ID code: 51678 Dates: DateEvent19 August 2014PublishedSubjects: Science > Mathematics > Electronic computers. Computer science Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 16 Feb 2015 12:11 Last modified: 18 Sep 2024 00:32 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/51678