A well-known representation of monoids and its application to the function ‘vect...
summary
Shows how representing a monoid as endofunctions yields difference Naturals so monoidal laws hold definitionally, letting a tail-recursive accumulator for ‘vector reverse’ typecheck without explicit arithmetic proofs. Builds a generalized fold that threads an index (a.k.a. fold indexed by N) and a small monoid solver that normalizes expressions; the result is a linear-time, proof-free vector reverse and a lightweight decision procedure for any monoid-indexed equality.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 0:52EGA
- 10:10Structure matters
- 10:55Difference Naturals
- 15:00Decon Operations
- 19:55Monoids
- 23:40Questions
related talks
21mGraded Monoids for Dependently Typed Array Programming
29mMonoids and Software Engineering
33mOptimising your code with math
55mMonoids, Monoids, Monoids
34mThe Monoiad: an epic poem on monoids
56mCategory Theory Through Functional Programming (part 2/3)
58mMonoids, Monads, and Applicative Functors: Repeated Software Patterns
35mAdjunctions in Everyday Life