How to prove `view` distributiveness over a lens composition

Learn
#1

In lens tutorial the following law is mentioned:

view (lens1 . lens2) = (view lens2) . (view lens1)

However, I failed to prove it:

view (lh . lk) ≡ view lk . view lh:
  view (lh . lk)
    ≡ getConst . (lh . lk) Const
    ≡ \s -> getConst (lh (lk Const) s)
  view lk . view lh
    ≡ getConst . lk Const . getConst . lh Const
    ≡ \s -> getConst (lk Const (getConst (lh Const s)))

I don’t see how can I make the next step without knowing something about lh and lk.

#2

Indeed! Not all values of the matching type are actually valid, law-abiding, lenses.

#3

I guess you’ll have to use one or more of the three lens laws.

1 Like
#4

I can’t see how it could be done, since Lens law are about one lens but here we have two. And anyway Lens laws are about Lens, but here we have two getters. And in Getter's doc we read:

Since a Getter cannot be used to write back there are no Lens laws that can be applied to it.

That’s why I think this should be provable without extra laws. Or should we add them to Getter's doc? It’s very suspicious, if I’m the first one who recognized this.

#5

I believe it should be possible to prove something like

g . f Const = f (g . Const)
 where
  f :: Lens' A B
  g :: forall x. Const B x -> Const B x
#6

I think you must be missing a parameter.

#7

I don’t see what’s wrong. Can you elaborate? Edit: Ah, my bad.

#8

Const takes two parameters.

1 Like
#9

It’s not true in general, so you do need some law. Perhaps it’s just parametricity of r in type Getting r s a = (a -> Const r a) -> s -> Const r s.

> let getter1 _ x = Const (x * 10)
> let getter2 _ x = Const (x + 1)

> view (getter1 . getter2) 1
10
> (view getter2 . view getter1) 1
11

[EDIT: corrected example]

#10

Yes, I think the key element is that

type Getter s a = forall f. (Contravariant f, Functor f) => (a -> f a) -> s -> f s

which means when use use it as a Getting

type Getting r s a = (a -> Const r a) -> s -> Const r s

the r is parametric. Then you’ll get a free theorem that allows you to proceed with your proof above. I’m not sure what that free theorem is though. Parametricity always puzzles me.

EDIT: In fact, maybe the theorem is just what @jaror said.

#11

That’s the spirit of it. If we have, for instance, a lens…

p :: forall f. Functor f => (a -> f b) -> (s -> f t)

… then f being parametric implies the following property, analogous to the naturality law of Traversable:

-- Given a natural transformation between Functors f and g:
-- t :: forall x. f x -> g x 
p (t . k) = t . p k

In particular:

  • This property does rule out your counterexample: if p were to ignore its argument, we’d be left with t only on the right side of the equation above, which can’t hold in general, as we can encode arbitrary functions as natural transformations between Const functors.

  • @jaror 's property arises as a special case, with k = Const and f ~ g ~ Const a.

The property suffices to resume @Lev135’s derivation:

-- Goal
getConst . (lh . lk) Const = getConst . lk Const . getConst . lh Const
(lh . lk) Const = lk Const . getConst . lh Const
-- RHS
lk Const . getConst . lh Const
getConst . first (lk Const) . lh Const
-- jaror's property: first (lk Const) is a natural transformation
getConst . lh (first (lk Const) . Const)
getConst . lh (Const . lk Const)
-- When applied to a Const value, Const is a natural transformation
getConst . Const . lh (lk Const)
lh (lk Const)
(lh . lk) Const  -- LHS = RHS
3 Likes
#12

Thank’s. I’ve already proved this property by myself, but it seems that your argument is much more general is applicable to many other places, where I’d like to prove such things.

#13

Does this hold for more restrictive constraints like (Functor f, Contravariant f)? How can it be proved? It’s important here, since I need to prove it for Getter's here and in even more restrictive case.

#14

EDIT: I misunderstood the question

More restrictive contexts make it easier to hold. Less restrictive contexts are in question, for example Traversals, that is

p :: forall f. Applicative f => (a -> f b) -> (s -> f t)

But I believe the condition holds for these, too.

#15

Does this hold for more restrictive constraints

I think “more restrictive” might be the wrong term, but if you mean by adding more constraints on the type of f, it doesn’t hold in general. If the constraints allows manufacturing an f t out of thin air, things can go wrong.

Consider

data T a = L | R
instance Functor T where
  fmap _ L= L
  fmap _ R = R
class IsoT f where
  toT :: f a -> T a
  fromT :: T a -> f a
instance IsoT T where
  toT = id
  fromT = id

-- and lets pick some values of p, t and k
p :: (Functor f, IsoT f) => (a -> f b) -> (s -> f t)
p _ _ = fromT R

t :: T x -> T x
t _ = L

k :: a -> T a
k _ = L

-- (t . p k) () = L
-- p (t . k) () = R
#16

I don’t understand why it’s should be easier. If p knows about f more, it can do something with it so that it will not distribute in this manner, isn’t it?

#17

Yes, of course. That’s why I asked when does it hold/how to prove this (to be able to prove in those situation, when it’s so by myself)

#18

Um, yes, I beg your pardon. I misunderstood what you meant by “more restrictive” (and then I failed to check your example).

Sure, you’re asking whether it works for (Functor f, Contravariant f) and I’m asking whether it works for Applicative f. Both are “more restrictive” on the type parameter f but less restrictive on the terms of the type

forall f. C f => (a -> f b) -> (s -> f t)

so they may not satisfy the desirable property.

I think the correct approach is to desugar the constraint into its dictionary and then obtain the free theorem a la Theorems for free!. So, for (Functor f, Contravariant f) the type in question would be

forall f. (Functor f, Covariant f) => (a -> f b) -> (s -> f t)

which desugars to

forall f a b s t.
    (forall p q. (p -> q) -> f p -> f q) ->
    (forall p q. (p -> q) -> f q -> f p) ->
    (a -> f b) ->
    (s -> f t)

But I’m not very good at deriving free theorems. Perhaps @duplode can help.

#19

In general, we do have to be careful with additional constraints, as only natural transformations which preserve the extra class operations will be admissible. That’s why, for instance, the naturality law of Traversable only holds for natural transformations which preserve pure and (<*>). If we are only dealing with Functor and Contravariant, though, no restrictions are necessary, as parametricity on its own is enough to ensure fmap and contramap are preserved.

Indeed: the requirement that the class methods are preserved follows from that.

1 Like