A Completely Unique Account of Enumeration
summary
A datatype generic enumerator is built that works for all regular types and indexed families and is proven complete and unique: every inhabitant appears eventually and at most once when iterating. The implementation and machine-checked proofs live in Agda, use a universe of type descriptions and combinators (empty, pure, choice, map, recursive), and add a generic memoisation / tabulation layer to avoid repeated recursion; benchmarks show measurable speedups for heavily shared indices.
AI-written summary · about
chapters (7)
- 0:00Start
- 0:03What Is Enumeration
- 3:14Completeness
- 4:58The Identity Function
- 9:16Finite Sets
- 10:53Generic Memorization Technique
- 11:50Conclusion
related talks
01h 08mType Arithmetic and the Yoneda Lemma
59mHaskell Design Patterns for Genericity & Asynchronous Behavior
41mLiving the Monadstic Life
17mComputing with Generic Trees in Agda
55mMonoids, Monoids, Monoids
30mThe conatural numbers form an exponential commutative semiring
21mGraded Monoids for Dependently Typed Array Programming
16mSyntax-Generic Operations, Reflectively Reified (Extended Abstract)