The type of (fmap . fmap)

By Steven Leiva

In this post, we will be unifying the types in the expression fmap . fmap.

The reason for this exercise is that we want to show that our informal algorithm for works so far.

In a subsequent post, we will be using the results of this exercise to show where our informal algorithm falls short, and extend it to fix this shortcoming.

Informal Algorithm

As a reminder, our informal algorithm for type unification goes something like this:

  1. Rearrange the expression to make it obvious to spot the function applications
  2. Gather the types of the function application - remember, we only deal with one application at a time
  3. Ensure that the type variable names are unique between function and argument - renaming if necessary
  4. Line up the types to figure out the equalities between type variables
  5. Erase the argument from the function, replacing type variables and adding in constraints

The type of fmap . fmap

Let's see how well this algorithm works on the expression fmap . fmap.

Step #1 - Rearrange Expression

We will re-arrange the expression to make the application of functions to arguments obvious. In our case fmap . fmap is equivalent to (.) fmap fmap.

Step #2 - Gather types of the application

Now that we can clearly spot the two arguments to (.), let's gather the types:

(.) :: (b -> c) -> (a -> b) -> a -> c

fmap :: Functor f => (a -> b) -> f a -> f b

Step 3 - Ensure Unique Type Variable Names

We can see that the type variable names a and b are re-used, so let's rename those in fmap

(.) :: (b -> c) -> (a -> b) -> a -> c

fmap :: Functor f => (d -> e) -> f d -> f e

Step 4 - Line Up the types

(.) :: (b -> c) -> (a -> b) -> a -> c

fmap :: Functor f => (d -> e) -> f d -> f e

Our goal is to unify b -> c with (d -> e) -> f d -> f e.

Remember that the function type constructor is right-associative. If we take advantage of this fact, we can re-write fmap's signature as: (d -> e) -> (f d -> f e). This leads us to unify as follows:

b ~ (d -> e) c ~ (f d -> f e)

Step 5 - Erase the argument

1 -- (.) fmap :: (a -> b) -> a -> c

b ~ (d -> e)
c ~ (f d -> f e)

2 -- (.) fmap :: (a -> (d -> e)) -> a -> (f d -> f e)

3 -- (.) fmap :: Functor f => (a -> d -> e) -> a -> f d -> f e

Second Application

Now that we've figured out the type of (.) fmap, we can rinse and repease:

(.) fmap :: Functor f => (a -> d -> e) -> a -> f d -> f e

fmap :: Functor f => (a -> b) -> f a -> f b

-- Ensure unique type variables
fmap :: Functor g => (c -> b) -> g c -> g b


-- Unify (a -> d -> e) with (c -> b) -> g c -> g b
a ~ (c -> b)
d ~ g c
e ~ g b

-- Erase the first argument
(.) fmap fmap :: a -> f d -> f e

-- Replace type variables, add in constraints
(.) fmap fmap :: (Functor f, Functor g) => (c -> b) -> f (g c) -> f (g b)