Simon Foster 📧, Christian Pardillo-Laursen 📧 and Frank Zeyda 📧

May 25, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Lenses provide an abstract interface for manipulating data types through spatially-separated views. They are defined abstractly in terms of two functions, get, the return a value from the source type, and put that updates the value. We mechanise the underlying theory of lenses, in terms of an algebraic hierarchy of lenses, including well-behaved and very well-behaved lenses, each lens class being characterised by a set of lens laws. We also mechanise a lens algebra in Isabelle that enables their composition and comparison, so as to allow construction of complex lenses. This is accompanied by a large library of algebraic laws. Moreover we also show how the lens classes can be applied by instantiating them with a number of Isabelle data types.


BSD License


October 5, 2022
Added Scene Spaces, which are used to model variable sets algebraically. Improvements to the alphabet command, including additional theorems. Additional prisms and associated laws. (revision 771b88d61c21)
November 15, 2021
Improvement of alphabet and chantype commands to support code generation. Addition of a tactic rename_alpha_vars that removes the subscript vs in proof goals. Bug fixes and improvements to alphabet command ML implementation. Additional laws for scenes. (revisions 9f8bcd71c121 and c061bf9f46f3)
January 27, 2021
Addition of new theorems throughout, particularly for prisms. New chantype command allows the definition of an algebraic datatype with generated prisms. New dataspace command allows the definition of a local-based state space, including lenses and prisms. Addition of various examples for the above. (revision 89cf045a)
March 2, 2020
Added partial bijective and symmetric lenses. Improved alphabet command generating additional lenses and results. Several additional lens relations, including observational equivalence. Additional theorems throughout. Adaptations for Isabelle 2020. (revision 44e2e5c)


Session Optics