A completely unique account of enumeration

Cas Van Der Rest, Wouter Swierstra

Research output: Contribution to journalArticleScientificpeer-review

1 Citation (Scopus)
16 Downloads (Pure)

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.

Original languageEnglish
Article number105
Number of pages27
JournalProceedings of the ACM on Programming Languages
Volume6
Issue numberICFP
DOIs
Publication statusPublished - 2022

Keywords

  • Agda
  • datatype generic programming
  • dependently typed programming
  • interactive proof assistants
  • property-based testing

Cite this