In the past I have blogged about functional references. From now on I will conform to most of the rest of the world, and call these things lenses.

Giving a presentation on these objects has forced me to think about them some more. As a result of this thinking I have a new favorite representation, at least from a theory point of view:

A lens from typeatobis a bijection betweenaand a pair ofband some residualr.

In pseudo-code we would write that as

type Lens a b = exists r. a <-> (b,r)

Except that Haskell has no `exists` keyword, so you have to use a newtype wrapper:

-- Isomorphisms/bijections between type @a@ and @b@ data Iso a b = Iso { fw :: a -> b, bw :: b -> a } -- Lenses with a data wrapper, in practice you might want to unpack the Iso type data Lens a b = forall r. Lens (Iso a (b,r))

So, why do I like this representation so much?

I believe this representation captures the intuition of what a lens does extremely well:
You have some record type `a`, and you want to take out and a field of (a smaller) type `b`. When you do that you are left with some residual, which you can think of as `a-b` (or should that be `a/b`?).

I imagine this graphically as

,

where we have a square record `a`, containing a smaller circular field of type `b`.

Implementing the usual `get`, `modify` and `set` functions is now very easy, by going back and forth through the lens.

get :: Lens a b -> a -> b get (Lens l) = fst . fw l modify :: Lens a b -> (b -> b) -> (a -> a) modify (Lens l) f = bw l . first f . fw l set :: Lens a b -> b -> a -> a set l b a = modify l (const b) a

The nice thing about the existential quantification is that the residual type `r` can be anything you like.
In some cases it is obvious what it could be, such as the case of tuples:

myFst :: Lens (a,b) a myFst = Lens (Iso id id) -- r = b

but we could also pick any other representation,

myCrazyFst :: Lens (a,String) a myCrazyFst = Lens (Iso fw bw) -- r = strings starting with "Banana" where fw (a,b) = (a, "Banana" ++ b) bw (a,'B':'a':'n':'a':'n':'a':b) = (a,b)

For this to be an actual isomorphism we have to restrict the residual to only strings that start with `"Banana"`. That is not something we can actually enforce in Haskell, but then again, we don't check that a lens is an isomorphism at all.

Besides the simple intuition and the freedom in declaring them, there is another reason for liking these lenses.

There are two (or one, depending on how you count) obvious laws you want isomorphisms to satisfy:

fw i . bw i = bw i . fw i = id

On the other hand, there are several less obvious laws for lenses:

set l (get l a) a = a get l (set l b a) a = b set l c (set l b a) = set l c a

And now comes the magic: with isomorphism lenses all of these laws follow from the simple laws of isomorphisms. Here are the quick and dirty proofs. One:

set l (get l a) a = {- expanding definitions of get and set -} (bw l . first (const ((fst . fw l) a)) . fw l) a = {- let x = fw l a, rewrite -} bw l (first (const (fst x)) x) where x = fw l a = {- (first (const (fst x)) x) = x -} bw l x where x = fw l a = {- fill in x and rewrite -} (bw l . fw l) a = {- isomorphism law -} a

Two:

get l (set l b a) a = {- expanding definitions of get and set, rewrite to use composition -} fst . fw l . bw l . first (const b) . fw l $ a = {- isomorphism law -} fst . first (const b) . fw l $ a = {- expanding fst, first and const -} (\(x,y) -> x) . (\(x,y) -> (b,y)) . fw l $ a = {- composing the two lambda terms -} const b . fw l $ a = {- definition of const -} b

Three:

set l c (set l b a) = {- expanding definition of set, rewrite to use composition -} bw l . first (const c) . fw l . bw l . first (const b) . fw l $ a = {- isomorphism law -} bw l . first (const c) . first (const b) . fw l $ a = {- first f . first g = first (f . g) -} bw l . first (const c . const b) . fw l $ a = {- const c . const b = const c -} bw l . first (const c) . fw l $ a = {- definition of set -} set l c a

So there you have it. A simple representation of lenses that gives a nice intuition of what these things actually do. And as an added bonus, the laws for lenses follow directly from the definition. Finally I should say that this representation is not my idea, it has been around in the literature for quite some time.

## Comments

When you do that you are left with some residual, which you can think of as a-b (or should that be a/b?).I think that should properly be ∂a/∂b, for reasons you're well aware of. Since the b does not intersect a (in general), a-b doesn't make sense; and since not all a contain b (in general) the quotient a/b doesn't make sense either.

For the record, I really hate the ∂a/∂b notation. It really should be just a single operator applied to a. We almost get that when it's written as (∂/∂b)a, when a is some complex expression; but even that is quite heavy-handed IMO. Unfortunately Newton's notation doesn't work in general since the (∂/∂b) operator is parameterized by b.

Any reason then why you don't write differentiation the way geometrists/topologists do? ∂_b f is the function ∂ applied to the direction b and the function f. This function ∂ is bilinear, and if you furthermore fix a point x where to evaluate the derivative, you have a bilinear form. (Not sure if this bilinearity can in some obscure sense be transferred to the zipper/lens setting.)

Mostly just because I haven't enough familiarity with geometry/topology to be familiar with it. I've seen the notation a couple times, and I rather like it, but I don't know how popular it is (i.e., how easily it'd be recognized by non-topologists; I try my best to avoid confusing notation).

I think that the residual really should be

(a/b), not(∂a/∂b). Let me explain.For a lens from

atobto exist, the typeahas to contain absomewhere, otherwise you can not extract it. You might think thatconst :: b -> Lens a bwas a valid lens function, but it is not. It would fail to satisfy the lawget l (set l b a) = b. The only valid constant lens isconst () :: Lens a (). The residual would then bea/1=a.Consider

Lens (a,a) a. This lens could either extract the first field, or the second one, and in both bases there is onealeft, so I claim that the residual should bea²/a = a. This gives the type(a,a) <-> (a,a)for this lens. There are exactly two bijections of this type:idandswap, corresponding to a lens selecting the first and the second element respectively.On the other hand, if you were to try to use

(∂(a,a)/∂a) = 2aas the residual type, it would not work. In fact, there are no bijections(a,a) <-> (a,2a), since you lose information by going from right to left.Finally, look at the lens

mod :: (n::PositiveNatural) -> Lens Integer {0..n-1}, here using some pseudo dependent type notation. The result type ofmod nwill be an integer in the range 0 to n-1, or equivalently, an element of the equivalence class of integers modulon, ℤ/nℤ. The residual is of type ℤ/(ℤ/nℤ) = nℤ ≈ ℤ.It should be relatively obvious why the derivative is incorrect here--

2adescribes not merely the residual data, but also the location from which it was extracted. A lens already identifies a location, therefore the residual can't. Note that, as you point out, there are exactly two lenses to choose from, so for these purposes2ais equivalent to(Lens (a, a) a, a).Could it be possible to see a small example of the lens' usage, say, the three basic functions on a tuple?

Diseq: here are a couple of examples. First some definitions:

Now to use these lenses:

The "GHCi" background on the first snippet seems wrong. I guess it's intentional on the ones after it.

Thanks, Anonymous. Fixed.

## Reply