Lance Myers

A lens is basically just a getter and setter, so one might expect something like the implementation below.

data Lens a b = Lens
    { get :: a -> b
    , set :: (b -> b) -> (a -> a)
    }


data Pair a b = Pair a b 

_1 :: Lens (Pair a b) a
_1 = Lens get set 
	where 
		get (Pair x _) = x
		set f (Pair x y) = Pair (f x) y

_2 :: Lens (Pair a b) b
_2 = Lens get set 
	where 
		get (Pair _ y) = y
		set f (Pair x y) = Pair x (f y)

Unfortunately, it is not that simple. We would like lenses to be more polymorphic than that, so we introduce two more type parameters.

data Lens s t a b = Lens 
	{ get :: s → a
	, set :: s → b → t
	}

Here s is the type of the overall structure, a the type of the subpart being focussed on, b the new type of the subpart after being set, and t the type of the whole structure after being set. While this is more flexible, it still does not compose nicely. If we want a lens that focuses on x_2 in Pair x_1 (Pair x_2 x_3), we want to just write _1 . _2. In the lens library, lenses are actually implemented as

type Lens' s t a b = forall f. Functor f ⇒ (a → f b) → (s → f t)

This is called a Van Laarhoven lens and contains the same data as the previous definition, just a bit obfuscated.

To show that this is isomorphic, we will need some basic category theory. The Yoneda lemma says that in a category $C$, for any functor $F : C \to \mathsf{Set}$ and object $a$ in $C$, we have the following natural isomorphism.

$\mathsf{Nat}(C(a, -), F) \cong F a$

In haskell, with $C = \mathsf{Set}$, we would write

	Functor f ⇒ Reader a ~> f ≅ f a

where

	type Reader a b = a → b
	type f ~> g = ∀ x. f x → g x

If we take $F = C(b, -)$ for some object $b$ in $C$, then we have

$\mathsf{Nat}(C(a, -), C(b, -)) \cong C(b, a)$

In haskell for $C = \mathsf{Set}$

	Reader a ~> Reader b ≅ b → a

Now we consider $C = [\mathsf{Set}, \mathsf{Set}]$, the category of endofunctors on $\mathsf{Set}$.

$\mathsf{Nat}([\mathsf{Set}, \mathsf{Set}](G, -), [\mathsf{Set}, \mathsf{Set}(H, -)] ) \cong [ \mathsf{Set}, \mathsf{Set} ](H, G)$

In haskell, this is written

	∀ f. Functor f ⇒ (g ~> f) → (h ~> f) ≅ h ~> g

Notice that we know have a quantification over all functors, just like in the definition of Van Laarhoven lenses. Now we just have to choose the right functors for g and h. We would like to have

	h ~> g ≅ s → (a, b → t) 
		   ≅ (s → a, b → t) 
		   ≅ Lens s t a b

and for all functors f,

    (g ~> f) → (h ~> f) ≅ (a → f b) → (s → f t)

For now, let’s focus on choosing g such that

	∀ f. Functor f ⇒ g ~> f ≅ ∀ f. Functor f ⇒ a → f b

We have an isomorphism between hom-sets, so we should look for adjoint functors. Lets rewrite the right hand side as a → R₁ f where R₁ is the functor R₁ f = f b. We need to find L₁ left adjoint to R₁.

	t → R₁ f
	≅ t → f b
	≅ t → Reader b ~> f
	≅ ∀ x. t → (b → x) → f x
	≅ ∀ x. (t, b → x) → f x

Let L₁ t x = (t, b → x). Then

	t → R₁ f
	≅ ∀ x. (t, b → x) → f x
	≅ L₁ t ~> f 

which shows that L₁ is left adjoint to R₁. Recall we want g ~> f ≅ a → f b, so we choose g = L₁ a.

	  g ~> f
	≅ L₁ a ~> f
	≅ a → R₁ f
	≅ a → f b

Similarly, define R₂ f = f t, L₂ x y = (x, s -> y), and h = L₂ s to get h ~> f ≅ s → f t. Now, let’s go back to the right hand side.

	  h ~> g
	≅ L₂ s ~> L₁ a
	≅ s → R₂ (L₁ a)
	≅ s → L₁ a t
	≅ s → (a, b → t)
	≅ Lens s t a b

Therefore,

	∀ f. Functor f ⇒ (a → f b) → (s → f t) ≅ Lens s t a b