What is the story behind a Getter?

Question

I stumbled upon Getter definition having both Functor and Contravariant constraint on f.

It's not surprising that "getter" can't do much with the "contained part" but this signature looks like a Phantom in a "van Laarhoven" setting of (a -> f a) -> s -> f s. Is the implicit constraint "s knows about a" represented this way in lens?

How can I find source code of some concrete instances of a Getter so that I can see map and contramap being used?

Answer 1

The idea of a Getter is that it is a read-only lens. Given a Getter s a you can pull an a out of an s, but you can't put one in. The type is defined thus:

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

When a type is both a Functor and Contravariant, it actually doesn't depend on its type argument at all:

import Data.Void

change :: (Functor f, Contravariant f) => f a -> f b
change = fmap absurd . contramap absurd

Such a functor will always look very much like Const b for some b.

So a Getter s a is essentially

type Getter s a = forall b . (a -> b) -> s -> b

but to make it work with the rest of the lens ecosystem it has extra polymorphism.

Answer 2

Well, a getter is basically just a function. The isomorphism is this:

getter :: (Functor f, Contravariant f) => (s->a) -> (a->f a) -> s->f s
getter f q = contramap f . q . f

Here, the contramap will in effect do nothing but coerce the types, because as you say, combining Functor and Contravariant amounts to requiring that f x doesn't actually contain an x. Basically, ensuring this is also the only reason the Functor constraint is there.