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 / ii / Solution

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.