Effectful Lenses: There and Back with Different Monads
summary
Framework introduces effectful lenses that allow different monads in the two directions, using the lenses with complements encoding plus user-specified roundtrip relations to describe how effects interact. Examples combine Reader, Error, and IO to handle context, failures, and user queries; composition preserves the generalized roundtrip properties and a combinator language (ID, composition, product, sum, complement ops) supports modular construction. Paper gives a lambda-names↔de Bruijn case study with three converter variants and a mechanized implementation with reusable artifacts.
AI-written summary · about
chapters (9)
- 0:00Effectful lenses intro
- 2:13Lenses need monadic effects
- 4:20Traditional lens challenges
- 7:54Monadic lenses questions
- 9:41Lenses with complements
- 12:14Combinator language for lenses
- 13:19Bidirectional conversion case
- 15:06Contributions summary
- 16:11Q&A
related talks
21mCompositions for Free: Reasoning about Effectful Lenses
43mFunctional Programming with Effects
57mLet's Lens - Part 2 of 5
31mThe Eff monad, one monad to rule them all
50mFunctional Programming with Effects
28mA Series of Unfortunate Effects
32mFunctional Lenses in JavaScript
01h 16mFunctional Composition Beyond Monads