Graded Monoids for Dependently Typed Array Programming
summary
Defines graded monoids as indexing algebras that let a single fold compute both values and index metadata, proven by a monoid-homomorphism that lifts to an algebra homomorphism; implements catamorphic and psychomorphism recursion schemes over lists so folds produce a sigma with a cost grade and data, demonstrated on CSV parsing that accepts 5 elements in 14 steps and rejects 9 blanks, and runs as Lean 4 elaboration-time parsing on a 4,433-row file (works interactively but is impractical for TB-scale IO).
AI-written summary · about
chapters (13)
- 0:00Graded monoids in array programming
- 1:16Graded monoids over folds
- 2:20Catamorphisms for parsing
- 4:27CSV example with graded monoids
- 6:58Index algebras correctness
- 8:22Shapely types refinements
- 10:51Recursion schemes intermission
- 11:35Parsing in Lean runtime
- 13:03Compile-time parsing for shapely types
- 14:50Free semiring extensions
- 15:33Takeaways and future work
- 16:17Summary and closing
- 16:48Q&A
related talks
55mMonoids, Monoids, Monoids
33mOptimising your code with math
25mA well-known representation of monoids and its application to the function ‘vect...
30mA Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
34mAdditive Cellular Automata Graded-Monadically
29mMonoids and Software Engineering
34mThe Monoiad: an epic poem on monoids
57mApplied category theory and abstract algebra