Explanation. The definition is

  (f x) y = y x

  f = x |→ (y |→ y x)

Remember that juxtaposition is function application. In expression (y x), y is being applied to x. So y must be a function. Let's say that y has type α → β. Since y is applied to x, x must have type α. Expression (y x) has type β.

f takes x (of type α) and yields a function that takes y (of type α → β) and yields (y x) (which has type β). So the type of f is (α → ((α → β) → β). By convention, → is right-associative. So the type of f can be written α → (α → β) → β.