# Lenses Are Exactly the Coalgebras for the Store Comonad

The store comonad (better known as the costate comonad) can be defined as

```data Store b a = Store (b -> a) b
```

```extract :: Store b a -> a
extract (Store v b) = v b

fmap :: (a -> c) -> Store b a -> Store b c
fmap f (Store v b) = Store (f . v) b

duplicate :: Store b a -> Store b (Store b a)
duplicate (Store v b) = Store (Store v) b

extend :: (Store b a -> c) -> Store b a -> Store b c
extend f x = fmap f (duplicate x)
```

Given this we can define a lens (aka a functional reference) as follows

```type Lens a b = a -> Store b a
```

A lens can be used as an accessor to a field of a record, though they have many uses beyond this.

```data Entry = { name_ :: String
; city_ :: String
; birthdate_ :: Data
}

name :: Lens Entry String
name entry = Store (\newName -> entry {name_ = newName})) (name_ entry)
```

Above we create a lens to access the name field of this `Entry` structure. We can build similar lenses to access other the fields.

We can write getter and setter functions for an arbitrary lenses.

```get :: Lens a b -> a -> b
get lens a = b
where
Store v b = lens a

set :: Lens a b -> a -> b -> a
set lens a = v
where
Store v b = lens a
```

However, we expect the `get` and `set` functions to obey certain laws. Here are the three laws that Koji Kagawa gives in his paper "Compositional References for Stateful Functional Programming". They are the laws that any second year computer science student would intuitively write down.

• `get l (set l s b) = b`
• `set l s (get l s) = s`
• `set l (set l s b1) b2 = set l s b2`

Today I was trying to rewrite these lens laws to use our comonadic operations on the store comonad instead of `get` and `set`. So after playing around I came up with the following alternative set of laws

• `extract . l = id`
• `fmap l . l = duplicate . l`

Interestingly these laws no longer depend on any special operations of the store comonad. They only use the operations generic for any comonad.

Do these laws look familiar? They should. They are exactly the laws of a coalgebra for a comonad!

I was floored by this. These three, almost arbitrary, set of laws that every computer scientist intuits are exactly the set of laws implied by this abstract nonsense from category theory. I honestly wrote these laws out completely before noticing what they were. I do not recall this fact noted on any paper about lenses that I have read, but it will definitely be mentioned in my upcoming paper.

Below is the Coq code that proves that these two sets of laws are equivalent.

```Set Implicit Arguments.

Section Lens.

Variable B : Type.

Definition W a := ((B -> a) * B)%type.

Definition extract (a:Type) (x : W a) : a := fst x (snd x).

Definition fmap (a b:Type) (f : a -> b) (x : W a) : W b := pair (fun z => f (fst x z)) (snd x).

Definition duplicate (a:Type) (x : W a) : W (W a) := pair (pair (fst x)) (snd x) .

Definition extend (a b:Type) (f : W a -> b) (x : W a) : W b := fmap f (duplicate x).

Variable A : Type.

Variable l : A -> W A.

Definition rd (r : A -> W A) (a:A) : B := snd (r a).
Definition wr (r : A -> W A) (a:A) (b:B) : A := fst (r a) b.

Section Iso1.

Hypothesis coalgebra1 : forall a, extract (l a) = a.
Hypothesis coalgebra2 : forall a, fmap l (l a) = duplicate (l a).

Lemma lawA : forall s t, rd l (wr l s t) = t.
Proof.
intros s t.
generalize (coalgebra2 s).
unfold rd, wr.
destruct (l s) as [f b].
unfold fmap, duplicate.
simpl.
inversion 1.
change (l (f t)) with ((fun z => l (f z)) t).
rewrite H1.
reflexivity.
Qed.

Lemma lawB : forall s, wr l s (rd l s) = s.
Proof.
firstorder.
Qed.

Lemma lawC : forall s t1 t2, wr l (wr l s t1) t2 = wr l s t2.
Proof.
intros s t.
generalize (coalgebra2 s).
unfold rd, wr.
destruct (l s) as [f b].
unfold fmap, duplicate.
simpl.
inversion 1.
change (l (f t)) with ((fun z => l (f z)) t).
rewrite H1.
reflexivity.
Qed.

End Iso1.

Section Iso2.

Hypothesis law1 : forall s t, rd l (wr l s t) = t.
Hypothesis law2 : forall s, wr l s (rd l s) = s.
Hypothesis law3 : forall s t1 t2, wr l (wr l s t1) t2 = wr l s t2.

Lemma coalgebraA : forall a, extract (l a) = a.
Proof.
firstorder.
Qed.

(* One day we will have observational type theory, but for now ... *)
Require Import FunctionalExtensionality.

Lemma coalgebraB : forall a, fmap l (l a) = duplicate (l a).
Proof.
intros a.
apply injective_projections; auto.
apply functional_extensionality; intros x.
simpl.
apply injective_projections.
apply functional_extensionality; intros y.
firstorder.
firstorder.
Qed.

End Iso2.
End Lens.
```
Edit (2011-01-19): I renamed the `Selection` comonad to the `Store` comonad and rearranged the order of some parameters to make it more compatible with Control.Comonad.Trans.Store. Some of the comments below use to the old name.
Tags:
• Post a new comment

#### Error

default userpic
When you submit the form an invisible reCAPTCHA check will be performed.