Why can't the type of id be specialised to (fo

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

I'm not an expert on impredictive types, so this is at once a potential answer and a try at learning something from comments.

It doesn't make sense to specialize

\/ a . a -> a                       (1)

to

(\/ a . a -> a) -> (\/ b . b -> b)  (2)

and I don't think impredictive types are a reason to allow it. The quantifiers have the effect of making the types represented by the left and right side of (2) inequivalent sets in general. Yet the a -> a in (1) implies left and right side are equivalent sets.

E.g. you can concretize (2) to (int -> int) -> (string -> string). But by any system I know this is not a type represented by (1).

The error message looks like it results from an attempt by the Haskel type inferencer to unify the type of id

\/ a . a -> a

with the type you've given

\/ c . (c -> c) -> \/ d . (d -> d)

Here I'm uniqifying quantified variables for clarity.

The job of the type inferencer is to find a most general assignment for a, c, and d that causes the two expressions to be syntactically equal. It ultimately finds that it's required to unify c and d. Since they're separately quantified, it's at a dead end and quits.

You are perhaps asking the question because the basic type inferencer -- with an ascription (c -> c) -> (d -> d) -- would just plow ahead and set c == d. The resulting type would be

(c -> c) -> (c -> c)

which is just shorthand for

\/c . (c -> c) -> (c -> c)

This is provably the least most general type (type theoretic least upper bound) expression for the type of x = x where x is constrained to be a function with the same domain and co-domain.

The type of "restricedId" as given is in a real sense excessively general. While it can never lead to a runtime type error, there are many types described by the expression you've given it - like the aforementioned (int -> int) -> (string -> string) - that are impossible operationally even though your type would allow them.

Answer 3

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.