What You Needa Know About Yoneda
summary
Explains the Yoneda lemma concretely and shows how two ubiquitous Haskell encodings are isomorphic: getter/setter pairs ↔ profunctor representations. Uses Haskell code (map and identity directions), the profunctor optics abstraction, and the co/contra variants to prove lenses, prisms and adapters compose where naive pairs don’t. Gives concrete examples — lists (difference-list fast reverse), orders, monoids, and an IoT toaster command GADT — and demonstrates the isomorphisms shorten proofs and enable free-monad-style ASTs where the naïve type wasn’t a functor, so the approach is both practical and verified.
AI-written summary · about
chapters (4)
- 0:00Start
- 17:53Making Commands
- 25:23Compositional References to Components within Composite Data Structures
- 30:56Pro Functor Optics
related talks
46mProfunctor Optics: The Categorical Approach
54mCategory Theory Through Functional Programming (part 3/3)
21mEffectful Lenses: There and Back with Different Monads
34mFormalizing the ∞-categorical Yoneda lemma
56mCategory Theory Through Functional Programming (part 2/3)
01h 08mType Arithmetic and the Yoneda Lemma
21mCompositions for Free: Reasoning about Effectful Lenses
29mMonoids and Software Engineering
