Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How (fmap . fmap) typechecks

I have been going through a article(http://comonad.com/reader/2012/abstracting-with-applicatives/) and found the following snippet of code there:

newtype Compose f g a = Compose (f (g a)) deriving Show

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

How does actually (fmap . fmap) typechecks ?

Their types being:

(.)  :: (a -> b) -> (r -> a) -> (r -> b)
fmap :: (a -> b) -> f a -> f b
fmap :: (a -> b) -> f a -> f b

Now from here I can see in no way in which fmap . fmap will typecheck ?

like image 941
Sibi Avatar asked Apr 12 '14 12:04

Sibi


2 Answers

First let's change the type variables' names to be unique:

(.)  :: (a -> b) -> (r -> a) -> (r -> b)
fmap :: Functor f => (c -> d) -> f c -> f d
fmap :: Functor g => (x -> y) -> g x -> g y

Now the first parameter to . has type a -> b and we supply an argument of type (c -> d) -> (f c -> f d), so a is c -> d and b is f c -> f d. So so far we have:

(.) :: Functor f => -- Left operand
                    ((c -> d) -> (f c -> f d)) ->
                    -- Right operand
                    (r -> (c -> d)) ->
                    -- Result
                    (r -> (f c -> f d))

The second parameter to . has type r -> a a.k.a. r -> (c -> d) and the argument we give has type (x -> y) -> (g x -> g y), so r becomes x -> y, c becomes g x and d becomes g y. So now we have:

(.)       :: (Functor f, Functor g) => -- Left operand
                                       ((g x -> g y) -> (f (g x) -> f (g y))) -> 
                                       -- Right operand
                                       ((x -> y) -> (g x -> g y)) ->
                                       -- Result
                                       (x -> y) -> f (g x) -> f (g y)
fmap.fmap :: (Functor f, Functor g) => (x -> y) -> f (g x) -> f (g y)
like image 113
sepp2k Avatar answered Oct 13 '22 12:10

sepp2k


The expression fmap . fmap has two instances of fmap which can, in principle, have different types. So let's say their types are

fmap :: (x -> y) -> (g x -> g y)
fmap :: (u -> v) -> (f u -> f v)

Our job is to unify types (which amounts to coming up with equality relations between these type variables) so that the right-hand side of the first fmap is the same as the left-hand side of the second fmap. Hopefully you can see that if you set u = g x and v = g y you will end up with

fmap :: (  x ->   y) -> (   g x  ->    g y )
fmap :: (g x -> g y) -> (f (g x) -> f (g y))

Now the type of compose is

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

To make this work out, you can pick a = x -> y and b = g x -> g y and c = f (g x) -> f (g y) so that the type can be written

(.) :: ((g x -> g y) -> (f (g x) -> f (g y)))    ->    ((x -> y) -> (g x -> g y))    ->    ((x -> y) -> (f (g x) -> f (g y)))

which is pretty unwieldy, but it's just a specialization of the original type signature for (.). Now you can check that everything matches up such that fmap . fmap typechecks.


An alternative is to approach it from the opposite direction. Let's say that you have some object that has two levels of functoriality, for example

>> let x = [Just "Alice", Nothing, Just "Bob"]

and you have some function that adds bangs to any string

bang :: String -> String
bang str = str ++ "!"

You'd like to add the bang to each of the strings in x. You can go from String -> String to Maybe String -> Maybe String with one level of fmap

fmap bang :: Maybe String -> Maybe String

and you can go to [Maybe String] -> [Maybe String] with another application of fmap

fmap (fmap bang) :: [Maybe String] -> [Maybe String]

Does that do what we want?

>> fmap (fmap bang) x
[Just "Alice!", Nothing, Just "Bob!"]

Let's write a utility function, fmap2, that takes any function f and applies fmap to it twice, so that we could just write fmap2 bang x instead. That would look like this

fmap2 f x = fmap (fmap f) x

You can certainly drop the x from both sides

fmap2 f = fmap (fmap f)

Now you realize that the pattern g (h x) is the same as (g . h) x so you can write

fmap2 f = (fmap . fmap) f

so you can now drop the f from both sides

fmap2 = fmap . fmap

which is the function you were interested in. So you see that fmap . fmap just takes a function, and applies fmap to it twice, so that it can be lifted through two levels of functoriality.

like image 35
Chris Taylor Avatar answered Oct 13 '22 12:10

Chris Taylor