Oleg's gists — Archive

Finding correct (lens) laws

Posted on 2018-12-12 by Oleg Grenrus lens, agda

#Introduction

In this post I’ll try to convince you that optic laws (as in the lens package documentation) are the right ones. For example recall the Lens laws (law names come from alternative naming of the operations: view = get and set = put1.

  • GetPut: You get back what you put in:

    view l (set l v s) ≡ v

  • PutGet: Putting back what you got doesn’t change anything:

    set l (view l s) s ≡ s

  • PutPut: Setting twice is the same as setting once:

    set l v' (set l v s) ≡ set l v' s

Why there are these three laws (why three?). How we know these three laws are "enough", or that they don’t require too much?

The solution is to consider a representation which is obviously a Lens (or Prism or ...), but for which also the "laws" are obvious. Then when we write conversion functions between this and more concrete representation we’ll find out what laws are needed.

The Iso - an isomorphism is the simplest example. The concrete representation is

data Iso s a = Iso { to :: s -> a, from :: a -> s }

But the an obvious definition in math world (citing Awodey 2010): In any category \mathcal{C} , an arrow f : S \to A is called an isomorphism, if there is an arrow g : A \to S in \mathcal{C} such that g \circ f \equiv 1_S and f \circ g \equiv 1_A . We write S \cong A if there exists an isomorphism between S and A .

Here, the mathematical conditions tells precisely which laws are required, namely for a (RecordWildCards destructed) Iso fields:

to . from ≡ id
from . to ≡ id

The isomorphism case is trivial. In the post I’ll go through more interesting optics:

  • Lens and Prism. Their laws should not be surprising to people familiar with lens library. However we discover a new law for Prism.

  • Affine (traversal). I discussed affine traversal in a post about them and give laws in Glassery. These laws were written based purely on intuition, which we’ll now verify.

  • Achromatic lens. There are my quickly written notes from March 2018. Turns out, I missed few bits.

  • Grate. Russel O’Connor gives laws for a van Laarhoven Grate (a two functor variant) in Grate: A new kind of Optic. We formulate them for "normal" Grates: grate :: ((s -> a) -> b) -> t. In the process we also learn more about Grate.

At the end we discuss a little about Setters. And conclude the post with general thoughts.

The Isomorphism lenses by Twan van Laarhoven makes the same things for lenses; we do it for more classes of optics.

#Lens

A Lens is a purely functional reference. Concrete Lens representation is

data Lens s a = Lens { view :: s -> a, set :: s -> a -> s }

Note: Here and later we work with so called monomorphic optics, i.e. optics which don’t allow type change. Hopefully I will lift this restriction in a future blog post. Also we swapped the arguments for set (in lens library set :: ASetter s t a b -> b -> s -> t). This version is easier to do math with (we will partially apply it).

We claim that a Lens should be a subject to the following three laws:

  • view (set s a) ≡ a

  • set s (view s) ≡ s

  • set (set s a) a' ≡ set s a'

Let’s show that the laws are both sound (not asking too much) and complete (asking enough). For that we’ll need another representation of lenses: an existential formulation:

\quad \mathsf{Lens}\;S\;A = \exists C, S \cong C \times A

This formulation isn’t novel (e.g. Russel O’Connor have a footnote about affine traversal in A representation theorem for second-order functionals), but I haven’t seen it used to highlight the laws. In Lenses Are Exactly the Coalgebras for the Store Comonad the laws of a coalgebra for a comonad are used. As my category theory knowledge is not very deep, I find the "coalgebra for a comonad" intimidating. I don’t know if and how "Lenses are the coalgebras for the costate comonad" is generalisable to other optics. Existential formulation on the other hand works for everything.

#Soundness

We can define view and set operations using existential formulation:

\begin{aligned} \quad &\mathsf{view} : S \to A \\ &\mathsf{view}\;s = \mathsf{snd}\; (f\;s) \\ &\mathsf{set} : S \to A \to S \\ &\mathsf{set}\;s\;a = g\; (\mathsf{pair}\;(\mathsf{fst}\;(f\;s))\;a) \end{aligned}

where f : S \to C \times A is the forward direction, and g : C \times A \to S is the backward direction of the isomorphism.

We can prove that Lens laws are sound by showing that this definitions satisfy the laws. For example the first GetPut law:

\begin{aligned} \quad &\mathsf{view}\; (\mathsf{set}\; s\; a) &&\equivvia{ \text{definitions} } \\ &\mathsf{snd}\;(f\; (g\; (\mathsf{pair}\;(\mathsf{fst}\;(f\;s))\;a))) &&\equivvia{ f \circ g \equiv 1 } \\ &\mathsf{snd}\;(\mathsf{pair}\;(\mathsf{fst}\;(f\;s))\;a) &&\equivvia{ \mathsf{snd}\;(\mathsf{pair}\;x\;y) = y } \\ &a &&\;\blacksquare \end{aligned}

The remaining PutGet and PutPut laws can be proved sound using similar direct calculation. In fact, I mechanized the proofs in this post; and soundness properties are proven mostly by a very simple tactic.

#Completeness

The other direction, completeness, is more interesting. Given \mathsf{view} : S \to A and \mathsf{set} : S \to A \to S , such that the three laws above hold, construct a \mathsf{Lens}\;S\;A .

The key insight is to pick the right "left overs" type C . I found the process of mechanizing proofs helpful, you will immediately rule out e.g. bare S . The A \to S (partially applied \mathsf{set} ) is better, but still too "big". We need to use a smaller, refined type:

\quad C = \{ c : A \to S \mid \exists s : S, c \equiv \mathsf{set}\; s \}

All three options make sense if you consider how lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b can be defined using e.g. Profunctor encoding, Glassery uses:

lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
lens getter setter pab = dimap
     -- c = s
     (\s -> (getter s, s))
     (\(b, s) -> setter s b)
     (first' pab)

but you can also write

lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
lens getter setter pab = dimap
     -- c = b -> t; or refined
     -- c = { f : b -> t | exists s. f = setter s }
     (\s -> (getter s, setter s))
     (\(b, f) -> f b)
     (first' pab)

Anyway, after a C is found, we can define an isomorphism. The arrows are defined as in the latter Profunctor example:

\begin{aligned} \quad &f : S \to C \times A \\ &f\; s = \mathsf{pair}\; (\mathsf{set}\;s \mid \mathsf{exists}\;s\;\mathsf{refl})\; (\mathsf{view}\; s) \\ &g : C \times A \to S \\ &g\;(\mathsf{pair}\; (c \mid -)\; a) = c\; a \end{aligned}

The proof obligation for the C refinement is not really an obligation at all, the equality is definitionally true ( \mathsf{refl} ). However, next we need to prove the isomorphism properties. The backwards direction is easy, it’s essentially a PutGet-law:

\begin{aligned} \quad &g\; (f\; s) &&\equivvia{\text{definition of $f$}} \\ &g\; (\mathsf{pair}\; (\mathsf{set}\;s \mid \mathsf{exists}\;s\;\mathsf{refl})\; (\mathsf{view}\; s)) &&\equivvia{ \text{definition of $g$} } \\ &\mathsf{set}\;s\;(\mathsf{view}\;s) &&\equivvia{ \text{\textbf{PutGet}-law} } \\ &s &&\;\blacksquare \end{aligned}

Forward direction is more involved. Here we will use proof irrelevance for the refinement proofs. Those proofs aren’t computationally relevant, so this is justified. I think it’s possible to encode these proofs in Cubical Agda. I also use functional extensionality, but it’s a theorem in Cubical Agda (it’s used once in the following part of the proof, try to spot it!) We will need to use both PutPut and GetPut laws, for the both halves of the product (pair), respectively.

\begin{aligned} \quad &f\; (g\; (\mathsf{pair}\;(c \mid \mathsf{exists}\; s\; \mathit{proof})\;a)) &&\equivvia{ \text{definition of $g$} } \\ &f\; (c\; a) &&\equivvia{ \text{rewrite using $\mathit{proof}$} } \\ &f\; (\mathsf{set}\;s\; a) &&\equivvia{ \text{definition of $f$} } \\ &\mathsf{pair}\; (\mathsf{set}\; (\mathsf{set}\;s\; a) \mid -)\;(\mathsf{view}\;(\mathsf{set}\;s\;a)) &&\equivvia{ \text{definition of $g$} } \\ \end{aligned}

We continue by proving the equality of pair halves separately:

\begin{aligned} \quad &\mathsf{set}\; (\mathsf{set}\;s\; a) &&\equivvia{ \text{\textbf{PutPut}-law} } \\ &\mathsf{set}\;s &&\equivvia{ \text{rewrite using $\mathit{proof}$} } \\ &c &&\;\blacksquare_1 \end{aligned}

and the other half:

\begin{aligned} \quad &\mathsf{view}\;(\mathsf{set}\;s\;a) &&\equivvia{ \text{\textbf{GetPut}-law} } \\ &a &&\;\blacksquare_2 \end{aligned}

This completes the completeness proof. We had to use all three laws. I’m sure that intuitively thinking the PutPut-law is simple to forget, but these calculations show that it is important.

#Calculation of the laws

In previous subsections, we knew the right Lens laws (candidates) a priori. We only needed to verify that they are in fact the right ones. But what if we didn’t knew the laws beforehand. Could we somehow calculate them?

In the completeness proof, all branches ended up with the use of some law, however we knew which C to pick, so we end up with a proof goal which is exactly one of the laws we can use. Therefore, trying to write a completeness proof is not a direct calculation way, either we need to know the right existential type to use (in my opinion not entirely obvious), or which laws there possibly are.

Unfortunately I don’t have a definitive answer to this problem. A sketch of the idea is however to start with

\quad S \cong C \otimes A

isomorphism, and try to massage it into something without C . Notice that we work in a category where all arrows are isomorphisms (groupoid), therefore we use \otimes -tensor, not \times- product.

If we assume that we have a Symmetric closed monoidal groupoid, then we can use a property:

\quad \mathrm{Hom}(C\otimes A, S) \cong \mathrm{Hom}(C,[ S, A] )

to find out that C and [S,A] = A \leftrightarrow S are isomorphic. (And this is the hand-wavy part: I don’t understand groupoids enough to say if above reasoning make any sense at all). We need to "remember" how to go back in S \to A direction, not all A \to S are invertible (e.g. const someS). That’s one reasoning to c = \mathsf{set}\; s refinement of C = A \to S .

We could stop here, as we in fact calculated what existential C we have to use (or at least could try). We can also continue, at this point we have

\quad S \cong (A \leftrightarrow S) \otimes A

C -less representation of Lens. If we forget the isomorphisms, the remainders are S \to A \to S and S \to A arrows (when we split the product), these are \mathsf{set} and \mathsf{view} arrows! So we went from existential to concrete representation of Lens without using Yoneda. (What you needa know about Yoneda is an interesting reed anyway!)

But if we stick with this representation, then we can write down the laws too: If left-to-right direction is s \mapsto (\mathsf{set}\;s, \mathsf{view}\;s) and the right-to-left is (\mathsf{set}\;s, a) \mapsto \mathsf{set}\;s\;a (here I hand-wave about, what the first half of the pair should be!) then we get

\begin{aligned} s &= \mathsf{set}\;s\;(\mathsf{view}\;s) && \textbf{PutGet} \\ \mathsf{set}\;s &= \mathsf{set}\;(\mathsf{set}\;s\;a) && \textbf{PutPut} \\ a &= \mathsf{view}\;(\mathsf{set}\;a) && \textbf{GetPut} \end{aligned}

Note how the PutPut-law is in contracted form, the form which we would preferred in the above Lens laws completeness proof (spoiler: that’s where I used functional extensionality, if you haven’t spotted it).

#Prism

In this section we do similar soundness and completeness proofs for prisms. A Prism is a generalized constructor. Concrete Prism representation is (preview and review are often called match and build respectively, I stick with lens-library vocabulary).

data Prism s a = Prism { preview :: s -> Maybe a, review :: a -> s }

We claim that a Prism should be a subject to the following two laws:

  • MatchBuild: First, if I review a value and then preview I will get it back:

    preview (review a) ≡ Just a

  • BuildMatch: Second, if you can extract a value a using a preview from a value s, then the value s is completely described by a prism and a:

    preview s ≡ Just a ⇒ review a ≡ s

The existential formulation of a Prism is similar to Lens’, but instead of product we have a coproduct (or sum):

\quad \mathsf{Prism}\;S\;A = \exists D, S \cong D + A

#Soundness

First step is to define preview and review operations for existential representation:

\begin{aligned} \quad &\mathsf{preview} : S \to \mathsf{Maybe}\;A \\ &\mathsf{preview}\;s = \mathsf{either}\;(d \mapsto \mathsf{nothing})\;(a \mapsto \mathsf{just}\;a) \; (f\;s) \\ &\mathsf{review} : A \to S \\ &\mathsf{review}\;a = g\; (\mathsf{right}\;a) \end{aligned}

where f : S \to D + A is the forward direction, and g : D + A \to S is the backward direction of the isomorphism.

As with Lens none of the laws is hard to show sound. The first one is a direct computation:

\begin{aligned} \quad &\mathsf{preview}\; (\mathsf{review}\; a) &&\equivvia{\text{definitions}} \\ &\mathsf{either}\;(d \mapsto \mathsf{nothing})\;(a \mapsto \mathsf{just}\;a)\; (f\; (g\;(\mathsf{right}\; a))) &&\equivvia{ f\circ g \equiv 1 } \\ &\mathsf{either}\;(d \mapsto \mathsf{nothing})\;(a \mapsto \mathsf{just}\;a)\; (\mathsf{right}\; a) &&\equivvia{\text{$\mathsf{either}$ computation}} \\ &\mathsf{just}\;a &&\;\blacksquare \\ \end{aligned}

and for the second one we need to prepare the precondition. The injectivity of constructors let’s rule out the case when f\;s = \mathsf{left}\;d , because \mathsf{nothing} \not\equiv \mathsf{just}\;x .

\begin{aligned} \quad &\mathsf{preview}\; s\equiv\mathsf{just}\;a &&\equivvia{\text{definitions}} \\ &\mathsf{either}\;(d \mapsto \mathsf{nothing})\;(a \mapsto \mathsf{just}\;a) (f \;s) \equiv \mathsf{just}\;a &&\equivvia{\text{injectivity of constructors}} \\ &f\;s \equiv \mathsf{right}\;a &&\;\blacksquare \end{aligned}

using which we can prove the law itself

\begin{aligned} \quad & \mathsf{review}\; a &&\equivvia{\text{definitions}} \\ & g\; (\mathsf{right }\; a) &&\equivvia{\text{rewrite using a precondition}} \\ & g\; (f\; (\mathsf{just}\;s)) &&\equivvia{g \circ f \equiv 1} \\ & s &&\;\blacksquare \end{aligned}

#Completeness

We need to construct a \mathsf{Prism}\;S\;A from the given \mathsf{review} : A \to S and \mathsf{preview} : S \to \mathsf{Maybe}\;A . Here also, as in the Lens case, we need to pick the right type for the existential. And again we need a refined type:

\quad D = \{ d : S \mid \mathsf{preview}\;d \equiv \mathsf{nothing} \}

And yet again, that type can be found either from Profunctor definition of prism (the either id setter):

prism :: (b -> t) -> (s -> Either t a) -> Prism s t a b
prism setter getter = dimap getter (either id setter) . right'}

or by informal calculation

\quad S \cong D + A \Rightarrow D \cong S - A

Then we can define the arrows of the isomorphism (I’m quite sure that smart enough proof search would find exactly these definitions):

\begin{aligned} \quad &f : S \to D + A \\ &f\; s = \mathsf{maybe\textnormal{-}case}\;(\mathsf{preview}\;s)\; (\mathit{proof} \mapsto \mathsf{left}\;(s \mid \mathit{proof}))\; (a\; \mathit{proof} \mapsto \mathsf{right}\; a)\\ &g : D + A \to S \\ &g\;(\mathsf{left}\; (s \mid - )) = s \\ &g\;(\mathsf{right}\; a) = \mathsf{review}\;a \\ \end{aligned}

We use non-standard \mathsf{maybe\textnormal{-}case} 2, which provides the match proofs too. yet it can be directly coded e.g. in Agda as:

open import Data.Maybe
open import Relation.Binary.PropositionalEquality

maybe-case : ∀ {a b} {A : Set a} {B : Set b}
           → (m : Maybe A)
           → (m ≡ nothing → B)
           → ((a : A) → m ≡ just a → B)
           → B
maybe-case (just a) f g = g a refl
maybe-case nothing  f g = f refl

Next we can show that f and g are inverses. The g \circ f \equiv 1 case:

\begin{aligned} \quad & g\; (f\; s) &&\equivvia{\text{definition of $f$}} \\ & g\; (\mathsf{maybe\textnormal{-}case}\;(\mathsf{preview}\;s)\; (\mathit{proof} \mapsto \mathsf{left}\;(s \mid \mathit{proof}))\; (a\; \mathit{proof} \mapsto \mathsf{right}\; a)) \\ \end{aligned}