Why can't the type of id be specialised to (forall a. a -> a) -> (forall b. b -> b)?

Question

Take the humble identity function in Haskell,

id :: forall a. a -> a 

Given that Haskell supposedly supports impredicative polymorphism, it seems reasonable that I should be able to "restrict" id to the type (forall a. a -> a) -> (forall b. b -> b) via type ascription. But this doesn't work:

Prelude> id :: (forall a. a -> a) -> (forall b. b -> b)  <interactive>:1:1:     Couldn't match expected type `b -> b'                 with actual type `forall a. a -> a'     Expected type: (forall a. a -> a) -> b -> b       Actual type: (forall a. a -> a) -> forall a. a -> a     In the expression: id :: (forall a. a -> a) -> (forall b. b -> b)     In an equation for `it':         it = id :: (forall a. a -> a) -> (forall b. b -> b) 

It's of course possible to define a new, restricted form of the identity function with the desired signature:

restrictedId :: (forall a. a -> a) -> (forall b. b -> b) restrictedId x = x 

However defining it in terms of the general id doesn't work:

restrictedId :: (forall a. a -> a) -> (forall b. b -> b) restrictedId = id -- Similar error to above 

So what's going on here? It seems like it might be related to difficulties with impredicativity, but enabling -XImpredicativeTypes makes no difference.

Answer 1

You are absolutely correct that forall b. (forall a. a -> a) -> b -> b is not equivalent to (forall a. a -> a) -> (forall b. b -> b).

Unless annotated otherwise, type variables are quantified at the outermost level. So (a -> a) -> b -> b is shorthand for (forall a. (forall b. (a -> a) -> b -> b)). In System F, where type abstraction and application are made explicit, this describes a term like f = Λa. Λb. λx:(a -> a). λy:b. x y. Just to be clear for anyone not familiar with the notation, Λ is a lambda that takes a type as a parameter, unlike λ which takes a term as a parameter.

The caller of f first provides a type parameter a, then supplies a type parameter b, then supplies two values x and y that adhere to the chosen types. The important thing to note is the caller chooses a and b. So the caller can perform an application like f String Int length for example to produce a term String -> Int.

Using -XRankNTypes you can annotate a term by explicitly placing the universal quantifier, it doesn't have to be at the outermost level. Your restrictedId term with the type (forall a. a -> a) -> (forall b. b -> b) could be roughly exemplified in System F as g = λx:(forall a. a -> a). if (x Int 0, x Char 'd') > (0, 'e') then x else id. Notice how g, the callee, can apply x to both 0 and 'e' by instantiating it with a type first.

But in this case the caller cannot choose the type parameter like it did before with f. You'll note the applications x Int and x Char inside the lambda. This forces the caller to provide a polymorphic function, so a term like g length is not valid because length does not apply to Int or Char.

Another way to think about it is drawing the types of f and g as a tree. The tree for f has a universal quantifier as the root while the tree for g has an arrow as the root. To get to the arrow in f, the caller instantiates the two quantifiers. With g, it's already an arrow type and the caller cannot control the instantiation. This forces the caller to provide a polymorphic argument.

Lastly, please forgive my contrived examples. Gabriel Scherer describes some more practical uses of higher-rank polymorphism in Moderately Practical uses of System F over ML. You might also consult chapters 23 and 30 of TAPL or skim the documentation for the compiler extensions to find more detail or better practical examples of higher-rank polymorphism.

Answer 2

why is it expecting a type of (forall a. a -> a) -> b -> b

I think the type forall b.(forall a. a -> a) -> b -> b is equivalent to the type you gave. It is just a canonical representation of it, where the forall is shifted as much to the left as possible.

And the reason why it does not work is that the given type is actually more polymorphic than the type of id :: forall c. c -> c, which requires that argument and return types be equal. But the forall a in your type effectively forbids a to be unified with any other type.