Are all lenses record field accessors?

Learn
1

This may be folklore among the category theorists that eat lens families for breakfast. I’ve been trying to prove that the existence of a

Lens a b = forall f. Functor f => (b -> f b) -> a -> f a

implies that a is actually isomorphic to (b,c) for some type c. In other words: All lenses are record field accessors.
Here’s how I’d prove it, but maybe there is a simpler way.

newtype Y b a = Y (forall f. Functor f => f b -> f a)
instance Functor (Y b) where
    fmap h (Y phi) = Y (fmap h . phi)

setY :: b -> Y b b
setY = const (Y id)

This is named Y because it is probably some Yoneda-thing. At least for non-empty b one can show that c ~ Y b (b,c).
Now my proposed isomorphism:

fromTuple :: (b, Y b a) -> a
fromTuple (b, Y phi) = phi id b -- uses the (Reader b) functor

toTuple :: Lens a b -> a -> (b, Y b a)
toTuple l a = (get l a, l setY a)

Maybe someone knows a simpler isomorphism?

2

Can’t you just do this:

-- we already know this is isomorphic to the Van Laarhoven encoding
type Lens a b = (a -> b, a -> b -> a)

to :: Lens a b -> a -> (b, b -> a)
to (get,set) x = (get x, set x)

from :: (b, b -> a) -> a
from (x, f) = f x

I also don’t know if I would consider this to be enough to call it a record field accessor. For example, from record field accessors I’d also expect that you can project multiple fields at once: Given Lens a b and Lens a c we should have a <-> (b, c, d) for some d. It’s not obvious to me if that follows from the single field case. Nevermind, you can always just compose the two lenses into Lens a (b, c) and then get a <-> ((b, c), d) which obviously implies a <-> (b,c,d)

3

No I would not expect that, because the fields accessed by the two lenses might overlap. But it is important to me how one could iterate this process of tuple-splitting.
What I am after is to compute equalisers. Suppose a has some l :: Lens a b and there is another function (not necessarily a getter) f :: a -> b. Then I want to represent the sub-type of a where get l and f coincide. The idea was to split a into the part b accessed by l and some rest c, then use f and the setter of l to compute the b part “on the fly” when constructing an a.

EDIT: Example

data Bill = Bill {
  _netInvoice :: Dollar,
  _tax        :: Dollar,
  _total      :: Dollar
  }

total :: Lens Bill Dollar 

f :: Bill -> Dollar
f (Bill net tax _) = net + tax

-- specification: get total = f

-- residue of Bill not accessed by 'total'
data Bill' = Bill' {
 netInvoice' :: Dollar,
 tax' :: Dollar
 }

equaliser :: Bill' -> Bill
equaliser (Bill' net tax) = let a = Bill net tax undefined 
  in set total (f a) a
4

Thanks! Using that representation, a proof indeed becomes much more manageable: That from.to l = id immediately follows from the second lens law. Hence (b, b -> a) contains a copy of a [*].
However,

(to (get,set).from) (b, const a) = (get a, set a)

which is not the same unless b = get a.

[*] Remark: That (b,b -> a) contains a copy of a follows without the existence of a lens, as long as b is inhabited. Does that also imply that there is no lawful Lens a Void?

1 Like
5

A proof of the isomorphism between the Van Laarhoven representation and the classical representation a -> (b, b -> a) can be found in the paper Profunctor optics: a categorical update, by Clarke et al., Proposition 5.2.

In Haskell syntax:

forall f. Functor f => (a -> f b) -> (s -> f t)
= -- by Yoneda
forall f. Functor f => (forall x. (a, b -> x) -> f x) -> (s -> f t)
= -- by co-Yoneda (sic. I think that's actually Yoneda again but maybe I just don't understand why there's ⊗ in the paper here)
s -> (a, b -> t)

(The integral symbol \int_{X} in the paper can be read as forall X.; there’s another integral symbol \int^{X} which is exists X.. In category theory, these things are called “ends” and “co-ends”. Bartosz Milewski’s blog/book has a chapter about it for Haskellers.)

With b = a, s = t, that gives us Lens' s a = (s -> (a, a -> s)).

We get a pair of function between s and (a, c) (where c = (a -> s)), but this is not necessarily an isomorphism (aka. bijection).

For a stronger property, we want lens laws. The representations forall f. Functor f => (a -> f a) -> (s -> f s) and s -> (a, a -> s) allow unlawful lenses. The claim “s and (a,c) are isomorphic” describes a round-tripping behavior which amounts to laws for lenses.

However, if we make “isomorphism” the law, c = a -> s is too big as a complement. The usual “put-get” law is a weaker requirement than an isomorphism. (EDITED: I previously had a citation here but it was wrong; it turns out that adding the “put-put” law is what gives us the isomorphism; see my next reply.) Let l :: s -> (a, a -> s). Adapting the put-get law to that type of lenses, we get: for all s and a, fst (l (snd (l s) a)) = a. Notably, it says nothing about the second component, that is the complement snd (l (snd (l s) a)) :: a -> s.

There’s a categorical treatment of the laws in Categories of Optics by Mitchell Riley.

6 Likes
6

So you’re saying that s -> (a, a -> s) is not an isomorphism, because the get-set form (s -> a, s -> a -> s) has the lens laws attached and those do not entail that the former representation is an iso? That was not quite what I was after:
I’d be satisfied with a proof that s ~ (a,c) for some object c that may or may not be a sub-object of a -> s, and may not even be representable as a Haskell type function (like my wrong Y) in general.

Of course equally enlightening would be a counterexample, a lawful lens where the type s can not be written as a tuple.

7

Okay, that’s a reasonable ask. In that case, you need the three lens laws (aka. the very well-behaved lens laws): GetPut, PutGet, and PutPut.

-- Suppose there is a lens
get :: s -> a
put :: s -> a -> s

-- satisfying the three laws
GetPut :: forall s. put s (get s) = s
PutGet :: forall s a. get (put s a) = a
PutPut :: forall s a b. put (put s a) b = put s b

Let us recall the definition of the candidate isomorphism:

to :: s -> (a, a -> s)
to s = (get s, put s)

from :: (a, a -> s)
from (a, f) = f a

If we restrict the complement (a -> s) to exactly the subset of functions that can be obtained by put, we can show that (to, from) is an isomorphism. In set comprehension notation:

-- aka. the *image* of put
c = {f :: a -> s | exists s. f = put s}

GetPut proves the roundtrip from s to (a, c) and back.

from (to s) = put s (get s) = s

For the other roundtrip, we start with a pair (a, c), where c is from the image of put. So we actually start with a pair (a, put s).
The from then to roundtrip goes:

to (from (a, put s)) = (get (put s a), put (put s a))

The first component simplifies by PutGet.

get (put s a) = a

The second component simplifies by an eta-reduced reformulation of PutPut:

put (put s a) = put s

Putting these steps together, the from-then-to roundtrip:

to (from (a, put s)) = (a, put s)

Conclusion: to and from form an isomorphism between s and (a, c) where c = {f :: a -> s | exists s. f = put s}.

to . from = id
from . to = id

To show that PutPut is necessary to get an isomorphism, here is a counterexample with a lens that does not satisfy it. Let s be a type with three elements A | B | C, and a be Bool (two elements).

get :: s -> a
get A = True
get B = False
get C = False

put :: s -> a -> s
put _ True = A
put A False = B
put B False = B
put C False = C

It satisfies GetPut and PutGet, but there is no isomorphism between A | B | C and (Bool, c) for any c because 2 does not divide 3.

5 Likes
8

Beautiful, especially the counterexample! I would formulate this a bit more symmetrically:
Fix any lens (get, put) and consider the set

T = {(a,f) :: (a, a -> s) | get (f a) = a, put (f a) = f}

By your argument, this set is isomorphic to s (because to is injective and T is the image of to) and furthermore isomorphic to (a,c) where

I realized that even if a is not empty, the empty function

absurd :: Void -> (a, a -> Void)

is a lawful lens because all three lens laws universally quantify over s. Thus in general a ~ Void implies s ~ Void but not the other way around. Yet in any case s ~ (a,c) because if s ~ Void and a is inhabited, then (a -> s) ~ Void and the tuple is again empty.

We conclude: All lenses are record field accessors for a suitably liberal definition of record field := component of a tuple.

3 Likes