Compositions for Free: Reasoning about Effectful Lenses
summary
Presents a construction that composes two different monads into a free polymonad so effects run in two staged layers and most roundtrip laws become theorems rather than axioms. Replaces the original five roundtrip axioms for effectful lenses with two (identity and composition), shows product and sum combinators still satisfy correctness, and gives concrete specifications for error, reader and state effects. Formal lifting preserves associativity and identity, and the framework directly re-bases the ICFP paper’s roundtrip relation proofs, reduces five axioms to two.
AI-written summary · about
chapters (10)
- 0:00Effectful isomorphisms introduction
- 1:50Composing different monads
- 4:40Free composition structure
- 7:35Polymonads vs monads
- 9:39Free composition significance
- 12:12Reasoning with free composition
- 12:34Arrow effects examples
- 13:59Lifting to reader and state
- 15:27Conclusion and applications
- 16:30Q&A
related talks
21mEffectful Lenses: There and Back with Different Monads
43mFunctional Programming with Effects
28mA Series of Unfortunate Effects
01h 14mBeyond Free Monads
50mFunctional Programming with Effects
01h 06mThe Evolution of Effects
15mLatent Effects for Reusable Language Components
57mLet's Lens - Part 2 of 5