CODEWITHSUNDEEP
haskellhaskell-lens
sevo
sevo

Reputation: 4609

What is the story behind a Getter?

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?

Upvotes: 5

Views: 245

Answers (3)

dremodaris
dremodaris

Reputation: 372

The type

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

is isomorphic to the type s -> a. The two sides of the isomorphism are given by

toGetter :: (s -> a) -> Getter s a
toGetter h alpha = contramap h . alpha . h
fromGetter :: Getter s a -> (s -> a)
fromGetter getter = getConst . getter Const

It is not hard to see that fromGetter (toGetter h) equals h.

Up to this point (i.e. in order to implement toGetter and fromGetter and to prove that fromGetter . toGetter = id) we have not used the Functor f constraint. This constraint is however necessary in order to prove that toGetter . fromGetter = id.

First assume that f is both a covariant Functor and a Contravariant functor. Then any function g :: x -> y yields functions fmap g :: f x -> f y and contramap g :: f y -> f x. Parametricity, combined with the functor laws, entails that these are mutually inverse, i.e. f x ≅ f y. Hence, f is (up to isomorphism) a constant functor, so we can think of Getter s a as being defined as

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

(as mentioned in dfeuer's answer). By the Yoneda lemma, this is isomorphic to s -> a.

Remarkably, if we lift the Functor f constraint:

OddGetter s a = forall f . Contravariant f => (a -> f a) -> (s -> f s)

then we obtain a subtype of Getter s a that is no longer isomorphic to s -> a, but instead to s -> Aux a s:

newtype Aux a x = Aux {aAux :: a, gAux :: x -> a}
instance Contravariant (Aux a) where
  contramap f (Aux a g) = Aux a (g . f)

toAux :: a -> Aux a a
toAux a = Aux a id

(Aux a, toAux) is the initial of all pairs (F, toF) where F is a contravariant functor and toF :: a -> F a, similar to how (Const a, Const) is the initial of all pairs (F, toF) where F is a co- and contravariant functor and toF :: a -> F a.

The two sides of the isomorphism can be implemented as follows:

toOddGetter :: (s -> Aux a s) -> OddGetter s a
toOddGetter sigma alpha s1 =
    contramap (\s2 -> gAux (sigma s1) s2) $ alpha $ aAux (sigma s1)
fromOddGetter :: OddGetter s a -> (s -> Aux a s)
fromOddGetter getter = getter toAux

Again, it is straightforward to check that fromOddGetter . toOddGetter = id, which already shows that OddGetter s a is not isomorphic to s -> a. To prove that fromOddGetter . toOddGetter = id, we again need a parametricity argument.

Parametricity entails that, for any natural transformation nu :: forall x . d x -> f x, any getter :: OddGetter s a and any alphaD :: a -> d a, we have

nu . getter alphaD = getter (nu . alphaD) :: s -> f s

Now, we instantiate d with Aux a, alphaD with toAux and nu with factor alpha (for an arbitrary alpha : a -> f a):

factor :: (a -> f a) -> forall x . Aux a x -> f x
factor alpha (Aux a g) = contramap g $ alpha a

which has the property that factor alpha . toAux = alpha. Then we have

factor alpha . getter toAux = getter (factor alpha . toAux) = getter alpha :: s -> f s

Now when we apply this to some s1 :: s, we find that getter alpha s1 (the applied RHS) equals

factor alpha (getter toAux s1)
  = contramap (gAux $ getter toAux s1) $ alpha (aAux $ getter toAux s1)
    {-by definition of factor-}
  = contramap (\s2 -> gAux (getter toAux s1) s2) $ alpha $ aAux (getter toAux s1)
    {-by eta-expansion and regrouping-}
  = toOddGetter (getter toAux) alpha s1
    {-by definition of toOddGetter-}
  = toOddGetter (fromOddGetter getter) alpha s1
    {-by definition of fromOddGetter-}

i.e. getter = toOddGetter (fromOddGetter getter).

Given the isomorphisms, it is perhaps remarkable that the type

OddGetter s a ≅ s -> Aux a s

is a subtype of

Getter s a ≅ s -> a

The "coercion" function

\ getter -> getter :: OddGetter s a -> Getter s a

corresponds to the function

\ sigma -> aAux . sigma :: (s -> Aux a s) -> (s -> a)

under these isomorphisms.

Upvotes: 1

dfeuer
dfeuer

Reputation: 48591

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.

Upvotes: 8

leftaroundabout
leftaroundabout

Reputation: 120711

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.

Upvotes: 5

Related Questions