Understanding operations on composed functor types

Question

According to several sources, the Haskell implementation for composing functors is more or less the following:

import Data.Functor.Compose

newtype Compose f g a = Compose { getCompose :: f (g a) }

instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose x) = Compose (fmap (fmap f) x)

My question is: what is the type of x in the last definition?

I'd say it is f g a, but even there I struggle to 'see' the computation fmap (fmap f) x

Could anyone be as kind as to provide a clear and complete working example of this point? What about fmapping a Tree of Maybe's paying attention to both Empty's and Node's?

Thank you in advance.

Answer 1

what is the type of x in the last definition?

Before saying anything else about the matter: you can ask GHC! GHC 7.8 and above supports TypedHoles, meaning that if you place an underscore in a expression (not pattern), and hit load or compile, you get a message with the expected type of the underscore and the types of the variables in local scope.

newtype Compose f g a = Compose { getCompose :: f (g a) }

instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose x) = _

GHC says now, with some parts omitted:

Notes.hs:6:26: Found hole ‘_’ with type: Compose f g b …
    -- omitted type variable bindings --
    Relevant bindings include
      x :: f (g a)
        (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:21)
      f :: a -> b
        (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:10)
      fmap :: (a -> b) -> Compose f g a -> Compose f g b
        (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:5)
    In the expression: _
    In an equation for ‘fmap’: fmap f (Compose x) = _
    In the instance declaration for ‘Functor (Compose f g)’

There you go, x :: f (g a). And after some practice, TypedHoles can help you tremendously in figuring out complex polymorphic code. Let's try to figure out our current code out by writing out the right hand side from scratch.

We've already seen that the hole had type Compose f g b. Therefore we must have a Compose _ on the right side:

instance (Functor f, Functor g) => Functor (Compose f g) where
    fmap f (Compose x) = Compose _

The new hole has type f (g b). Now we should look at the context:

Relevant bindings include
  x :: f (g a)
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:21)
  f :: a -> b
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:10)
  fmap :: (a -> b) -> Compose f g a -> Compose f g b
    (bound at /home/kutta/home/Dropbox/src/haskell/Notes.hs:6:5)

The goal is to get an f (g b) out of the ingredients in the context. The fmap in the listing above unfortunately refers to the function being defined, which is sometimes helpful, but not here. We're better off knowing that f and g are both functors, therefore they can be fmap-ed over. Since we have x :: f (g a), we guess that we should fmap something over x to get an f (g b):

fmap f (Compose x) = Compose (fmap _ x)

Now the hole becomes g a -> g b. But g a -> g b is very easy now, since we have f :: a -> b and g is a Functor, so we also have fmap :: (a -> b) -> g a -> g b, and therefore fmap f :: g a -> g b.

fmap f (Compose x) = Compose (fmap (fmap f) x)

And we're done.

To wrap up the technique:

1. Start with putting a hole in the place where you don't know how to proceed. Here we started with putting the hole in place of the entire right hand side, but often you will have a good idea about most parts of an implementation and you'll need the hole in a specific problematic subexpression.

2. By looking at the types, try to narrow down which implementations could possibly lead to the goal and which could not. Fill in a new expression and reposition the hole. In proof assistant jargon this is called "refining".

3. Repeat step 2 until you either have the goal, in which case you're done, or the current goal seems impossible, in which case backtrack until the last non-obvious choice you made, and try an alternative refining.

The above technique is sometimes facetiously called "type tetris". A possible drawback is that you can implement complex code just by playing the "tetris", without actually understanding what you're doing. And sometimes after going too far, you get seriously stuck in the game, and then you have to start actually thinking about the problem. But ultimately it lets you understand code that would be otherwise very difficult to grasp.

I personally use TypedHoles all the time and basically as a reflex. I've come to rely so much on it so that on a occasion when I had to move back to GHC 7.6 I felt rather uncomfortable (but fortunately you can emulate holes even there).