= 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 therefore
$$
\boxed{((\alpha\to\beta)\to(\alpha\to\beta))\to\alpha\to(\alpha\to\beta)\to\beta.}
$$
The 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.
Back to article page
