How does get function typecheck in lens

Question

I have been reading this post to understand lens. They initially define a type synonym like this:

type RefF a b = forall f. Functor f => (b -> f b) -> (a -> f a)

Const is defined like this:

newtype Const a b = Const { getConst :: a }

How does the get function typecheck:

get :: RefF a b -> a -> b
get r = getConst . r Const

The type of getConst is something like this:

getConst :: Const a b -> a

The type of r Const which I guess is something like this:

r Const = (b -> f b) -> (Const -> f Const)

Then how does both getConst and r Const get's composed to give a -> b?

Answer 1

The type of r is obtained by substituting the const functor for f; since we'll need a b result that has to be the first argument (only x is actually found in the Const x y type)

    r :: (b -> Const b b) -> (a -> Const b a)

Now the argument is simple: that's merely the Const constructor.

    r Const :: a -> Const b a

And if you post-compose that with getConst :: Const b a -> b, you end up with

    getConst . r Const :: a -> b

Answer 2

One way to understand the type of a Lens

type Lens s a = forall f . Functor f => (a -> f a) -> (s -> f s)

is to read it as "if you tell me how to put the (focused) subpart into some Functor I can tell you how to put the whole thing into that Functor". The forall means that the person using the lens gets to choose the Functor, though, so we can play tricks.

The Const Functor is a trick Functor in that it has two type parameters, but while it's Functorial over the second one... it actually only contains a value of the first.

newtype Const real fake = Const { getConst :: real }

Thus, the constructor Const is a function

Const :: real -> Const real fake

which secrets away the real value being wrapped and results in a Functor which pretends to be carrying any type fake whatsoever.

---

To be clear, the Functor instance for Const looks like

instance Functor (Const b) where
  fmap _ (Const b) = Const b

in other words, fmap is essentially a no-op.

---

So let's see what happens when we pass Const to a lens:

l       :: Lens s a
Const   :: a -> Const a a
l Const :: s -> Const a s

In other words, our Lens got tricked into injecting the subpart, a, into Const and ignoring the whole-part, s. Then we just extract it with getConst.

getConst :: Const real fake -> real

getConst . l Const :: s -> a