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