### 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

BSD 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)

### Topics

- Computer science/Functional programming
- Mathematics/Algebra

### Session Optics

- Interp
- Two
- Lens_Laws
- Lens_Algebra
- Lens_Order
- Lens_Symmetric
- Scenes
- Scene_Spaces
- Lens_Instances
- Lenses
- Prisms
- Channel_Type
- Dataspace
- Optics
- Lens_Record_Example
- Lens_State

### Used by

- ConcurrentHOL
- Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming

## Cite

×

Optics-AFP

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

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Jun 1, 2017 : Isabelle2016-1