Isomorphism lenses

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 type a to b is a bijection between a and a pair of b and some residual r.

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?

Intuition

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.

Laws

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

wren ng thorntonDate: 2011-05-23T01:15Zx

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.

wren ng thorntonDate: 2011-05-23T01:24Zx

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.

maltemDate: 2011-05-23T16:14Zx

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.)

wren ng thorntonDate: 2011-05-23T21:09Zx

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).

Twan van LaarhovenDate: 2011-05-24T09:48Zx

I think that the residual really should be (a/b), not (&#8706;a/&#8706;b). Let me explain.

For a lens from a to b to exist, the type a has to contain a b somewhere, otherwise you can not extract it. You might think that const :: b -> Lens a b was a valid lens function, but it is not. It would fail to satisfy the law get l (set l b a) = b. The only valid constant lens is const () :: Lens a (). The residual would then be a/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 one a left, so I claim that the residual should be /a = a. This gives the type (a,a) <-> (a,a) for this lens. There are exactly two bijections of this type: id and swap, corresponding to a lens selecting the first and the second element respectively.

On the other hand, if you were to try to use (&#8706;(a,a)/&#8706;a) = 2a as 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 of mod n will be an integer in the range 0 to n-1, or equivalently, an element of the equivalence class of integers modulo n, ℤ/nℤ. The residual is of type ℤ/(ℤ/nℤ) = nℤ ≈ ℤ.

C. McCannDate: 2011-05-24T20:47Zx

It should be relatively obvious why the derivative is incorrect here--2a describes 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 purposes 2a is equivalent to (Lens (a, a) a, a).

DiseqDate: 2011-08-29T16:38Zx

Could it be possible to see a small example of the lens' usage, say, the three basic functions on a tuple?

Twan van LaarhovenDate: 2011-08-31T11:26Zx

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

fst3 :: Lens (a,b,c) a
snd3 :: Lens (a,b,c) b
fst3 = Iso (\(a,b,c) -> (a,(b,c)) (\(a,(b,c)) -> (a,b,c)
snd3 = Iso (\(a,b,c) -> (b,(a,c)) (\(b,(a,c)) -> (a,b,c)

Now to use these lenses:

> let x = ("some example","blank",123)
> get fst3 x
"some example"
> modify snd3 ("not "++) x
("some example","not blank",123)
> set fst3 "first" x
("first","blank",123)
> set fst3 "first" . set snd3 "second" $ x
("first","second",123)
AnonymousDate: 2011-09-19T04:17Zx

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

Twan van LaarhovenDate: 2011-09-19T08:49Zx

Thanks, Anonymous. Fixed.

Reply

(optional)
(optional, will not be revealed)
What greek letter is usually used for anonymous functions?
Use > code for code blocks, @code@ for inline code. Some html is also allowed.