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.

Coranto

I know this is a bit late, but... for what it's worth, in modern GHCs, id :: (forall a. a -> a) -> (forall b. b -> b) does indeed type-check. And with TypeApplications, you can use id @(forall a. a -> a) to (probably) avoid the fragile version-specific behavior of ImpredicativeTypes type-checking. (You still need the ImpredicativeTypes extension on, though.) – Oblivious

Answer 1

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.

Hydranth

Hm, I think you're right that (forall a. a -> a) -> b -> b is equivalent to the type I gave... but then why can't the compiler recognize that? Also if I change to the "canonical form" I still get the given error message. As to the second point, how is it more polymorphic? Instantiating the type variable c at forall a. a -> a yields exactly the type I gave. – Coranto

This seems so, but observe that after writing the type in the canonical form, the b is monomorphic, hence (forall a.a -> a) can never be substituted for (b -> b). – Hydranth

Well, in that case it seems like forall b. (forall a. a -> a) -> b -> b is not equivalent to (forall a. a -> a) -> (forall b. b -> b), wouldn't you agree? I will have to think about this more tomorrow when my brain is fresh... btw, frege looks really cool :) – Coranto

@pelotom - you might also want to read Simon Peyton Jones' "Practical type inference for arbitrary-rank types" paper which is linked on my blogs reading list. He discusses several ways to make a higher rank type "cannonic" and gives a rationale. You coul dtry this stuff alos with Frege, either you discover a compiler error or you get another error message, and the Frege compiler has a -explain option that traces parts of the type inference which could help to understand better. (Yet there is no interpreter yet, you must compile a file) – Hydranth

Thanks for the paper reference... I'll give that a look and see if it brings enlightenment, then accept your answer if it does. +1 – Coranto

Answer 2

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.

Conchita

You seem to be answering a different question than I asked; I'm familiar with all the concepts you're explaining. My question is, why can I not annotate id, which has type forall a. a-> a, with the type (forall a. a -> a) -> (forall a. a -> a)? In System F, which is impredicative, I can certainly prove that any term which has type ∀a. a -> a also has type (∀a. a -> a) -> (∀a. a -> a); simply instantiate the a in the first type with ∀a. a -> a. Supposedly Haskell supports impredicative polymorphism to some extent, but it seems to have a problem with this particular example. – Coranto

Also, while forall b. (forall a. a -> a) -> b -> b and (forall a. a -> a) -> (forall b. b -> b) are not the same, they are equivalent (isomorphic) and should ideally be treated interchangeably by the type system. See the paper by SPJ that @Hydranth mentioned. – Coranto

Oops, I misunderstood. You're example makes sense, and my version (6.12.1) of ghci has no problems with it, however I receive a warning "-XImpredicativeTypes is deprecated: impredicative polymorphism will be simplified or removed in GHC 6.14". I suspect that may be relevant to your example. – Conchita

Interesting, I'm using GHC 7.2.2. Does it make any difference in 6.12.1 whether you use -XImpredicativeTypes, or does it work either way? – Coranto

The fact that this type checks in 6.x but not 7.x makes me suspect that it may be related to the same underlying issue that causes this oddity. – Coranto

Huh, it works either way but doesn't provide a warning unless I use -XImpredicativeTypes. – Conchita

SPJ confirms here that the ImpredicativeTypes implementation was mostly removed: haskell.org/pipermail/glasgow-haskell-users/2014-February/… – Saucy

Answer 3

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.

Winch

It does make sense to specialize forall a. a -> a to (forall a. a -> a) -> (forall a. a -> a). Your claim that you can concretize (2) to (Int -> Int) -> (String -> String) is the incorrect part of your counterargument. The result can be concretized to String -> String, but the argument cannot be concretized to Int -> Int in that way: the person implementing id at this other polymorphic type is the one that gets to choose how to concretize the argument, not the person calling the other id. Note that forall a. (a -> a) -> B is a very different type from (forall a. a -> a) -> B. – Oblivious