Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Functional programming, design and analysis of algorithms / 1 / b

In the type signature map :: (u -> v) -> [u] -> [v], the supplied function is concat :: [[a]] -> [a]. Type inference therefore identifies u with [[a]] and v with [a]. Consequently,

map concat :: [[[a]]] -> [[a]]

Thus $\boxed{[[[\alpha ]]]\to [[\alpha ]]}$ is the principal type. For example, map concat [[[1],[2,3]],[[4],[]]] gives [[1,2,3],[4]]: it concatenates each inner group, preserving the outermost grouping.

Both uses of x in this definition have the same monomorphic type within the body. Write x :: u -> v. The inner application x z forces z :: u and has type v; the outer application x (x z) forces v = u. Thus x :: u -> u. Finally, x (x z) is applied to y, so u must itself be a function type, say a -> b. This gives

f :: ((a -> b) -> a -> b) -> a -> (a -> b) -> b
f x y z = x (x z) y

The principal type is thereforeThe argument x transforms a function into another function of the same type. The body transforms z twice, then applies the resulting function to y; no recursive type equation is required.