Delta Dictionaries

Dictionaries, or finite maps, are a core data structure in any programming language. General-purpose languages implement dictionaries with hash tables or balanced trees, but proof assistants — which favor simplicity and provability over performance — generally employ association lists or finite partial functions. Though suitable for many uses, each solution has drawbacks: association lists allow arbitrary order and may contain duplicates (unless refined with an explicit proof about validity), and partial functions cannot be destructed and their equality is not decidable. This paper illustrates a novel list-based representation, called delta dictionaries, that simultaneously achieves benefits of the conventional representations. Delta dictionaries are semantically total (every type-correct list is semantically valid), extensional (there is a one-to-one correspondence between lists and semantic mappings), destructible (sub-dictionaries can be inspected as needed), and have decidable equality. Included is an implementation of delta dictionaries in Agda, and a discussion of when delta dictionaries may or may not be preferable to conventional solutions.