A completely unique account of enumeration

Journal article (2022)

Authors

C.R. van der Rest Programming Languages - EEMCS
Wouter Swierstra Universiteit Utrecht
Research Group
Programming Languages (EEMCS) (TU Delft)
Copyright: © 2022 C.R. van der Rest, Wouter Swierstra
DOI
help_outline
https://doi.org/10.1145/3547636
Agda Datatype generic programming Dependently typed programming Interactive proof assistants Property-based testing
More Info
expand_more

Published Date

2022

Language

English

Faculty

Electrical Engineering, Mathematics and Computer Science

Department

Software Technology

Research Group

Programming Languages

Abstract

How can we enumerate the inhabitants of an algebraic datatype? This paper explores a datatype generic solution that works for all regular types and indexed families. The enumerators presented here are provably both complete and unique - they will eventually produce every value exactly once - and fair - they avoid bias when composing enumerators. Finally, these enumerators memoise previously enumerated values whenever possible, thereby avoiding repeatedly recomputing recursive results.