Lenses as algebras for a monad

Bryce Clarke – 26 August 2020

Lenses are a mathematical structure used to capture the notion of synchronisation between a pair of systems. While several kinds of lenses may be understood as algebras for a monad, the class of delta lenses was instead characterised by Johnson and Rosebrugh as certain algebras for a semi-monad. In this talk, we show that delta lenses are algebras for a monad, using the construction of the free delta lens on a functor due to Richard Garner, and explore the implications of this result.