A completely unique account of enumeration

Cas Van Der Rest; Wouter Swierstra

doi:10.1145/3547636

A completely unique account of enumeration

Cas Van Der Rest, Wouter Swierstra

Programming Languages

Research output: Contribution to journal › Article › Scientific › peer-review

1 Citation (Scopus)

60 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 language	English
Article number	105
Number of pages	27
Journal	Proceedings of the ACM on Programming Languages
Volume	6
Issue number	ICFP
DOIs	https://doi.org/10.1145/3547636
Publication status	Published - 2022

Keywords

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

Access to Document

10.1145/3547636

3547636Final published version, 286 KBLicence: CC BY

Cite this

@article{8b970ae1e3aa4a61a5aeb50d900a1e7a,

title = "A completely unique account of enumeration",

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.",

keywords = "Agda, datatype generic programming, dependently typed programming, interactive proof assistants, property-based testing",

author = "{Van Der Rest}, Cas and Wouter Swierstra",

year = "2022",

doi = "10.1145/3547636",

language = "English",

volume = "6",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery (ACM)",

number = "ICFP",

}

TY - JOUR

T1 - A completely unique account of enumeration

AU - Van Der Rest, Cas

AU - Swierstra, Wouter

PY - 2022

Y1 - 2022

N2 - 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.

AB - 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.

KW - Agda

KW - datatype generic programming

KW - dependently typed programming

KW - interactive proof assistants

KW - property-based testing

UR - http://www.scopus.com/inward/record.url?scp=85139400498&partnerID=8YFLogxK

U2 - 10.1145/3547636

DO - 10.1145/3547636

M3 - Article

AN - SCOPUS:85139400498

SN - 2475-1421

VL - 6

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - ICFP

M1 - 105

ER -

A completely unique account of enumeration

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this