Playing with the type system

Given these definitions:
(.) :: (b -> c) -> (a -> b) -> a -> c
map :: (a -> b) -> [a] -> [b]
head :: [a] -> a

Find the type of (map . head)

1. (f . g) x = f (g x)
(map . head) x = map (head x)

2. If we set
x :: [a -> b]
then we have
head x :: a -> b

3. \x -> map (head x) :: [a -> b] -> [a] -> [b]
=>
map . head :: [a -> b] -> [a] -> [b]

Let’s now try to find a senseful definition of [a -> b] -> [a] -> [b] by using hole-driven approach (inspired by http://www.youtube.com/watch?v=52VsgyexS8Q):

In this example we are using a silent hole (i.e. undefined). We are also writing the types of each argument (xs and ys)

{-# LANGUAGE ScopedTypeVariables #-}

f :: forall a b. [a -> b] -> [a] -> [b]
f xs ys = undefined
    where
    _ = xs :: [a -> b]
    _ = ys :: [a]

It’s compiling. But it does nothing.

Let’s try to do the same with a noisy hole:

data Hole = Hole

f :: forall a b. [a -> b] -> [a] -> [b]
f xs ys = Hole
    where
    _ = xs :: [a -> b]
    _ = ys :: [a]

We get this error:
Couldn’t match expected type `[b]’ with actual type `Hole’

How do we get from Hole to [b]? We have xs :: [a -> b]. What if instead we tried map?

f :: forall a b. [a -> b] -> [a] -> [b]
f xs ys = map Hole Hole
    where
    _ = xs :: [a -> b]
    _ = ys :: [a]

We now get these errors:
Couldn’t match expected type `a0 -> b’ with actual type `Hole’
Couldn’t match expected type `[a0]’ with actual type `Hole’

The second hole is obviously just ys:

f :: forall a b. [a -> b] -> [a] -> [b]
f xs ys = map Hole ys
    where
    _ = xs :: [a -> b]
    _ = ys :: [a]

Now we get:
Couldn’t match expected type `a -> b’ with actual type `Hole’

What if we try to use just xs instead of Hole?

Couldn’t match expected type `a -> b’ with actual type `[a -> b]’

Now it wants just x, not xs.

One way to get to that is to use (head xs)

f :: forall a b. [a -> b] -> [a] -> [b]
f xs ys = map (head xs) ys
    where
    _ = xs :: [a -> b]
    _ = ys :: [a]

This makes it happy.

Conclusion:
The function of type [a -> b] -> [a] -> [b] is not unique, because we could use something else for map instead of just (head xs).

Bonus:
id’ :: forall a. a -> a
id’ x = Hole
    where
    _ = x :: a

Couldn’t match expected type `a’ with actual type `Hole’

id’ x = x