Towards Optic-Based Algebraic Theories: the Case of Lenses
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
LICENSE
README.md
Sect1.v
Sect2.v
Sect3.v
Sect4.v
Sect5.v
figure.jpg
towards.pdf

README.md

Towards Optic-Based Algebraic Theories

This repository contains the supplementary material associated to the article Towards Optic-Based Algebraic Theories: the Case of Lenses (J. López-González and Juan M. Serrano), submitted to Trends in Functional Programming 2018. In essence, it contains Coq definitions and theories revolving around very well-behaved lenses and MonadState. They are summarized in the following figure.

alt text

Broadly, we show that:

  1. MonadState generalizes lens. Particularly, MonadState A (state S) is isomorphic to lens S A. Given this situation, we will refer to MonadState as lens algebra (lensAlg).
  2. A monad morphism state A ~> state S is isomorphic to lens S A.
  3. We can abstract away state S from the aforementioned monad morphism, obtaining lensAlg' as a result. In other words, natLens S A is exactly lensAlg' (state S) A.
  4. lensAlg is isomorphic to lensAlg', and hence MonadState.
  5. We can also abstract away state A from lensAlg', obtaining lensAlgHom. In other words, lensAlg' p A is exactly lensAlgHom p (state A) A.
  6. lensAlgHom p q A induces a lawful lensAlg A p.