According to the tutorial on Lenses:
type Getting b a b = (b -> Const b b) -> (a -> Const b a)
-- ... equivalent to: (b -> b ) -> (a -> b )
-- ... equivalent to: (a -> b )
Question: Why is (b -> b) -> (a -> b) equivalent to (a -> b)?
The tutorial isn't very precise about this. Here's the full definition of Getting:
type Getting r s a = (a -> Const r a) -> s -> Const r s
Stripping off the newtype noise,
Getting r s a ~= (a -> r) -> s -> r
The interesting isomorphism you should get from this is the following:
(forall r. Getting r s a) ~= s -> a
In a now-deleted comment, chi pointed out that this is a special case of the Yoneda lemma.
The isomorphism is witnessed by
fromGetting :: Getting a s a -> (s -> a)
fromGetting g = getConst . g Const
-- ~= g id
-- Note that the type of fromGetting is a harmless generalization of
-- fromGetting :: (forall r. Getting r s a) -> (s -> a)
toGetting :: (s -> a) -> Getting r s a
toGetting f g = Const . getConst . g . f
-- ~= g . f
-- Note that you can read the signature of toGetting as
-- toGetting :: (s -> a) -> (forall r. Getting r s a)
Neither fromGetting nor toGetting has a rank-2 type, but to describe the isomorphism, the forall is essential. Why is this an isomorphism?.
One side is easy: ignoring the Const noise,
fromGetting (toGetting f)
= toGetting f id
= id . f
= f
The other side is trickier.
toGetting (fromGetting f)
= toGetting (f id)
= \g -> toGetting (f id) g
= \g -> g . f id
Why is this equivalent to f? The forall is the key here:
f :: forall r. Getting r s a
-- forall r. (a -> r) -> s -> r
f has no way to produce an r except by applying the passed function (let's call it p) to a value of type a. It's given nothing but p and a value of type s. So f really can't do anything except extract an a from the s and apply p to the result. That is, f p must "factor" into the composition of two functions:
f p = p . h
So
g . f id = g . (id . h) = g . h = f g