paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A completely unique account of enumeration

一种完全唯一的枚举理论
ICFP 6(ICFP)2022匹配度 1/10 · 论文属于函数式编程与类型论中的泛型枚举/记忆化研究,核心是正则类型与索引族的完备、唯一、公平枚举,与用户关注的静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析均无直接交集。引用 2 inbox
Cas van der Rest, Wouter Swierstra
crossref: 2026-09-10

AI 速览

一句话:提出适用于正则类型与索引族的泛型枚举器,保证完备、唯一且公平,并尽可能记忆化已枚举值。

本文研究如何枚举代数数据类型的居民。作者提出一种数据类型泛型的枚举方案,适用于所有正则类型和索引族。其枚举器可证明同时具备完备性与唯一性:最终会恰好生成每个值一次;同时具备公平性,在组合枚举器时避免偏向。方法上通过泛型构造处理递归与索引结构,并尽可能对已枚举值进行记忆化,避免重复计算递归结果。关键结果是为代数数据类型提供了一个统一、无偏且高效的枚举方法,并给出相应的性质证明。

问题
如何为代数数据类型枚举其所有居民,并保证枚举过程不遗漏、不重复且在组合枚举器时保持公平。
方法
提出一种适用于正则类型与索引族的数据类型泛型枚举器;通过泛型构造实现完备性、唯一性和公平性,并对已枚举值尽可能记忆化。
评估
通过证明枚举器的完备性、唯一性与公平性,并说明记忆化避免重复计算递归结果来评估该方案。
原文摘要(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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1483,
  title = {A completely unique account of enumeration},
  author = {Cas van der Rest and Wouter Swierstra},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {6},
  number = {ICFP},
  year = {2022},
  doi = {10.1145/3547636}
}