Abstract
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.
License
History
- 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)