haskell functor scalaz category-theory scala-cats

Why must fmap map every element of a List?

Having read the book Learn you a Haskell For Great Good, and the very helpful wiki book article Haskell Category Theory which helped me overcome the common category mistake of confusing category objects with the programming objects, I still have the following question:

Why must fmap map over every elements of a List?

I like that it does, I just want to understand how this is justified category theoretically. ( or perhaps it is easier to justify using HoTT? )

In Scala notation, List is a functor that takes any type and maps that into an type from the set of all list types, eg it maps the type Int to the type List[Int] and it maps the functions on Int eg

Int.successor: Int => Int to Functor[List].fmap(successor) : List[Int] => List[Int]
Int.toString: Int => String to Functor[List].fmap(toString): List[Int] => List[String]

Now every instance of List[X] is a monoid with a empty function (mempty in Haskell) and combine function (mappend in Haskell). My guess is that one can use the fact that Lists are Monoids, to show that map has to map all elements of a list. My feeling here is that if one adds the pure function from Applicative, this gives us a list with just one element of some other type. e.g Applicative[List[Int]].pure(1) == List(1). Since map(succ) on those elements gives us the singleton list with the next element, this covers all those subsets. Then I suppose the combine function on all those singletons gives us all the other elements of the lists. Somehow I suppose that constrains the way map has to work.

Another suggestive argument is that map has to map functions between lists. Since every element in a List[Int] is of type Int, and if one maps to List[String] one has to map every element of it, or one would not the right type.

So both of those arguments seem to point in the right direction. But I was wondering what was needed to get the rest of the way.

Counterexample?

Why is this not a counterexample map function?

def map[X,Y](f: X=>Y)(l: List[X]): List[Y] = l match {
  case Nil => Nil
  case head::tail=> List(f(head))
}

It seems to follow the rules

val l1 = List(3,2,1)
val l2 = List(2,10,100)

val plus2 = (x: Int) => x+ 2
val plus5 = (x: Int) => x+5

map(plus2)(List()) == List()
map(plus2)(l1) == List(5)
map(plus5)(l1) == List(8)

map(plus2 compose plus5)(l1) == List(10)
(map(plus2)_ compose map(plus5)_)(l1) == List(10)

Ahh. But it does not fit the id law.

def id[X](x: X): X = x

map(id[Int] _)(l1) == List(3)
id(l1) == List(3,2,1)

Solution

This relies on a theoretical result called "parametricity", first defined by Reynolds and then developed by Wadler (among others). Perhaps the most famous paper on this topic is "Theorems for free!" by Wadler.

The key idea is that from the polymorphic type of a function only, we can get some information about the semantics of the function. For instance:

foo :: a -> a

From this type alone, we can see that, if foo terminates, it is the identity function. Intuitively, foo can not distinguish between different as since in Haskell we do not have e.g. Java's instanceof which can inspect the actual runtime type. Similarly,

bar :: a -> b -> a

must return the first argument. And baz :: a -> a -> a must return either the first or the second. And quz :: a -> (a -> a) -> a must apply some fixed number of times the function to the first argument. You probably get the idea now.

The general property which can be inferred from a type is quite complex, but luckily it can be computed mechanically. In category-theory, this is related to the notion of natural transformation.

For the map type, we get the following scary property:

forall t1,t2 in TYPES, f :: t1 -> t2.
 forall t3,t4 in TYPES, g :: t3 -> t4.
  forall p :: t1 -> t3.
   forall q :: t2 -> t4.
    (forall x :: t1. g (p x) = q (f x))
    ==> (forall y :: [t1].
          map_{t3}_{t4} g (map2_{t1}_{t3} p y) =
          map2_{t2}_{t4} q (map_{t1}_{t2} f y))

Above, map is the well-known map function, while map2 is any arbitrary function which has type (a -> b) -> [a] -> [b].

Now, further assume that map2 satisfies the functor laws, in particular map2 id = id. We then can choose p = id and t3 = t1. We get

forall t1,t2 in TYPES, f :: t1 -> t2.
 forall t4 in TYPES, g :: t1 -> t4.
   forall q :: t2 -> t4.
    (forall x :: t1. g x = q (f x))
    ==> (forall y :: [t1].
          map_{t1}_{t4} g (map2_{t1}_{t1} id y) =
          map2_{t2}_{t4} q (map_{t1}_{t2} f y))

Applying the functor law on map2:

forall t1,t2 in TYPES, f :: t1 -> t2.
 forall t4 in TYPES, g :: t1 -> t4.
   forall q :: t2 -> t4.
    (forall x :: t1. g x = q (f x))
    ==> (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t2}_{t4} q (map_{t1}_{t2} f y))

Now, let's choose t2 = t1 and f = id:

forall t1 in TYPES.
 forall t4 in TYPES, g :: t1 -> t4.
   forall q :: t1 -> t4.
    (forall x :: t1. g x = q x)
    ==> (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t1}_{t4} q (map_{t1}_{t1} id y))

By the functor law of map:

forall t1, t4 in TYPES.
   forall g :: t1 -> t4, q :: t1 -> t4.
    g = q
    ==> (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t1}_{t4} q y)

which means

forall t1, t4 in TYPES.
 forall g :: t1 -> t4.
    (forall y :: [t1].
          map_{t1}_{t4} g y =
          map2_{t1}_{t4} g y)

which means

forall t1, t4 in TYPES.
          map_{t1}_{t4} = map2_{t1}_{t4}

Summing up:

If map2 is any function with polymorphic type (a -> b) -> [a] -> [b], and such that it satisfies the first functor law map2 id = id, then map2 must be equivalent to the standard map function.

Note that in Scala the above holds only if you do not use x.isInstanceOf[], and other reflection tools, which can break parametricity.