CODEWITHSUNDEEP
haskellghc
Ingo
Ingo

Reputation: 36339

What does forall on the right of a function arrow mean?

The topic of Section 7.12.5 of the GHC Users Guide is higher rank polymorphism. There are some example valid types, among others:

f4 :: Int -> (forall a.a->a)

Now I wonder what this type means. I think it is the same as:

f4' :: forall a. Int -> a -> a

If this is so, can we generally mentally move forall like the above (that appears right of the rightmost arrow) to the left assuming that no type variable with the same name occurs in the rest of the type (but this could be dealt with renaming, simply)?

For example, the following would still be correct, wouldn't it:

f5 :: Int -> (forall a. (forall b. b -> a) -> a)
f5' :: forall a. Int -> (forall b. b -> a) -> a

Would be thankful for an insightful answer.

Background: In this talk about lenses by SPJ, we have:

type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s

and then, when you compose them, you have such a lens type in the result. Therefore I just wanted to know whether my intuition is correct, that the forall in the result doesn't really matter - it just appears "accidentally" because of the type synonym. Otherwise, there must be some difference between the types for f4, f4'and f5, f5' above I would want to learn about.

Here is a ghci session:

Prelude> let f5 :: Int -> (forall a. (forall b. b -> a) -> a); f5 i f = f i
Prelude> :t f5
f5 :: Int -> (forall b. b -> a) -> a
Prelude>

Looks like GHC agrees with me, at least in this case .....

Upvotes: 4

Views: 297

Answers (1)

Satvik
Satvik

Reputation: 11208

f4 in your example can be universally quantified because Int -> (forall a. a -> a) and forall a. Int -> (a -> a) are essentially same.

But we can not apply you analogy for example in this Rank2 type (forall a. a -> a) -> (forall b. b -> b). This type is essentially same as forall b. (forall a. a -> a) -> (b -> b). But moving the first forall out (forall a b. (a -> a) -> (b -> b)) essentially changes the semantics of the type.

f :: (forall a. a -> a) -> (forall b. b -> b) -- Rank 2
g :: forall a b. (a -> a) -> (b -> b)         -- Rank 1

To see the difference, you can instantiate a in g to be Int and thus can pass a function of type Int -> Int to g. On the other hand the argument to f has to be universally quantified (specified by that forall before the function type) and should work for all types (Example of such a function is id).

Here is a good explanation of higher rank types.

Upvotes: 4

Related Questions