
Well anyway, I was under the impression that id :: x -> x, so I'm not really sure why this wouldn't work without Rank-2 types...
The matter at hand is the type of the function /f/, not of the function /id/. I'll address the question of applying /f/ to /id/ at the end, but the interesting question is how to assign a type to /f/ at all. In Bob's example, f g x = (g g) x let us try to give /f/ a type. The rank-1 type we might first attempt is: f :: (a -> a) -> a -> a (which is the same thing as /f :: forall a. (a -> a) -> a -> a/). But under this type, we would have /g :: a -> a/, and then the expression /g g/ is illegal. If we try again, f :: ((a -> a) -> (a -> a)) -> a -> a we again find that the expression /g g/ is illegal. Experimenting further along this line will quickly convince you of the difficulty of typing /f/. However, it can be done using rank-2 types:
f :: (forall a. a -> a) -> b -> b f g x = (g g) x
In the expression /g g/, both /g/s have the same rank-1 type /forall a. a -> a/ (which is the same as the type /a -> a/); in the second usage of /g/, we assign /b/ to the type variable /a/, and in the first usage of /g/, we assign /b -> b/ to the type variable /a/. (Thus, the second usage of /g/ has type /a -> a/, and the first usage has type /(a -> a) -> (a -> a)/.) This is the essential point of the /forall a/ -- it allows the type variable /a/ to be instantiated differently as /g/ is used in different places. In other words, it is polymorphic. Going back to /id/, recall that id :: a -> a which is the same thing as id :: forall a. a -> a (i.e., /id/ is a polymorphic function). Since the type of /id/ unifies with the first argument of /f/, the function application /f id/ is well-typed. Note that we could "simplify" Bob's example down to: f2 g = g g although the type of this /f2/ is less pleasant: f2 :: (forall a. a -> a) -> (forall a. a -> a) Say, wouldn't a syntax like "(forall a => a -> a)" or "(a => a -> a)" or something similar to that be more consistent with syntax for contexts, e.g. "(Ord a => a -> a)"? Eric