Every Lens' is a Traversal'... how?

Question

Control.Lens.Tutorial says:

type Traversal' a b = forall f . Applicative f => (b -> f b) -> (a -> f a) 
type Lens'      a b = forall f . Functor     f => (b -> f b) -> (a -> f a) 

Notice that the only difference between a Lens' and a Traversal' is the type class constraint. A Lens' has a Functor constraint and Traversal' has an Applicative constraint. This means that any Lens' is automatically also a valid Traversal' (since Functor is a superclass of Applicative).

I simply don't follow the logical sequence here. We know that every Applicative is a Functor. From this, should it not follow, if at all, that every Traversal' is a Lens'? The tutorial however reaches the converse conclusion.

Answer 1

A Lens' works for all functors, which includes all applicative functors, so if a function g is a Lens', then g is also a Traversal'.

A Traversal' works for all applicative functors, but not necessarily all functors. So if a function h is a Traversal', it is not necessarily a Lens'.

(I'm not the one to describe this formally, but to me at least, it looks like the types are "contravariant" in their constraints. Lens' is a subtype of Traversal' precisely because Functor is a superclass of Applicative.)

Answer 2

I'm not usually a fan of cute "real-world entity" analogies, but this matter probably does become clearer by considering the following example:

class Animal a where feed :: a -> ArmouredGlove -> IO String

instance Animal Cat where feed _ _ = print "Miaow"
instance Animal Dog where feed _ _ = print "Woof"
instance Animal Lion where feed _ _ = print "Rwaaar"

class Animal a => Pet a where cuddle :: a -> UnprotectedHand -> IO String

instance Pet Cat where cuddle _ _ = print "Purr"
instance Pet Dog where cuddle _ _ = print "Yawn"

type PetOwner = ∀ a . Pet a => a -> IO String
type ZooWarden = ∀ a . Animal a => a -> IO String

peter :: PetOwner
peter = \pet -> cuddle pet peter'sHand

zoey :: ZooWarden
zoey = \animal -> feed animal zoey'sGlove

Here, ZooWarden is a subtype of PetOwner. Zoey can handle a pet just fine, she can feed any dog as well as lions. But Peter does not have such qualification, he can only handle harmless pets. So, precisely because he is restricted to a more specific class of animals, he himself is member of a more general type of person than the specialised zoo warden.

Answer 3

Consider the dictionary-passing view of type classes. This is how type classes are actually implemented in GHC.

Background

In this form, type classes like Functor and Applicative look something like this:

data Functor f =
  MkFunctor
    { fmap :: (a -> b) -> f a -> f b }

data Applicative f =
  MkApplicative
    { appFunctor :: Functor f
    , pure :: a -> f a
    , (<*>) :: f (a -> b) -> f a -> f b
    }

Instances are values of those types, for example like this:

listFunctor :: Functor []
listFunctor =
  MkFunctor
    { fmap = map }

Lenses and traversals

Now, let's say we have a lens someLens :: Lens' A B and we want to turn it into a traversal. Let's expand the type synonym and use dictionary passing:

someLens :: Functor f -> (b -> f b) -> (a -> f a)

In this style, you might use it with the list functor like this someLens listFunctor.

We want a traversal someTraversal :: Traversal' A B. When we implement this, we will need to provide someLens with a Functor f value. But we already have an Applicative f value:

someTraversal :: Applicative f -> (b -> f b) -> (a -> f a)
someTraversal applicativeDict = someLens (appFunctor applicativeDict)

We can just use the field accessor that gets the Functor implementation for the Applicative instance we were given, and we have a Traversal. The field accessor has type appFunctor :: Applicative f -> Functor f.