Optics

Simon Foster and Frank Zeyda

25 May 2017

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.
BSD License

Change history

[2020-03-02] 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)
[2021-01-27] 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)
[2021-11-15] 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)

Topics

Theories

Cite

×
@article{Optics-AFP,
  author  = {Simon Foster and Frank Zeyda},
  title   = {Optics},
  journal = {Archive of Formal Proofs},
  month   = May,
  year    = 2017,
  note    = {\url{http://isa-afp.org/entries/Optics.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download