Understanding Haskell's RankNTypes

Question

While working my way through GHC extensions, I came across RankNTypes at the School of Haskell, which had the following example:

main = print $ rankN (+1)

rankN :: (forall n. Num n => n -> n) -> (Int, Double)
rankN f = (f 1, f 1.0)

The article offered an alternative type for rankN:

rankN :: forall n. Num n => (n -> n) -> (Int, Double) 

The explanation of the difference is that

The latter signature requires a function from n to n for some Num n; the former signature requires a function from n to n for every Num n.

I can understand that the former type requires a signature to be what's in the parentheses or more general. I do not understand the explanation that the latter signature simply requires a function n -> n for "some Num n". Can someone elaborate and clarify? How do you "read" this former signature so that it sounds like what it means? Is the latter signature the same as simply Num n => (n -> n) -> (Int, Double) without the need for forall?

Answer 1

In the normal case (forall n. Num n => (n -> n) -> (Int, Double)), we choose an n first and then provide a function. So we could pass in a function of type Int -> Int, Double -> Double, Rational -> Rational and so on.

In the Rank 2 case ((forall n. Num n => n -> n) -> (Int, Double)) we have to provide the function before we know n. This means that the function has to work for any n; none of the examples I listed for the previous example would work.

We need this for the example code given because the function f that's passed in is applied to two different types: an Int and a Double. So it has to work for both of them.

The first case is normal because that's how type variables work by default. If you don't have a forall at all, your type signature is equivalent to having it at the very beginning. (This is called prenex form.) So Num n => (n -> n) -> (Int, Double) is implicitly the same as forall n. Num n => (n -> n) -> (Int, Double).

What's the type of a function that works for any n? It's exactly forall n. Num n => n -> n.

Answer 2

How do you "read" this former signature so that it sounds like what it means?

You can read

rankN :: (forall n. Num n => n -> n) -> (Int, Double)

as "rankN takes a parameter f :: Num n => n -> n" and returns (Int, Double), where f :: Num n => n -> n can be read as "for any numeric type n, f can take an n and return an n".

The rank one definition

rank1 :: forall n. Num n => (n -> n) -> (Int, Double)

would then be read as "For any numeric type n, rank1 takes an argument f :: n -> n and returns an (Int, Double)".

Is the latter signature the same as simply Num n => (n -> n) -> (Int, Double) without the need for forall?

Yes, by default all foralls are implicitly placed at the outer-most position (resulting in a rank-1 type).

Answer 3

In the rankN case f has to be a polymorphic function which is valid for all numeric types n.

In the rank1 case f only has to be defined for a single numeric type.

Here is some code which illustrates this:

{-# LANGUAGE RankNTypes #-}

rankN :: (forall n. Num n => n -> n) -> (Int, Double)
rankN = undefined

rank1 :: forall n. Num n => (n -> n) -> (Int, Double)
rank1 = undefined

foo :: Int -> Int  -- monomorphic
foo n = n + 1

test1 = rank1 foo -- OK

test2 = rankN foo -- does not type check

test3 = rankN (+1) -- OK since (+1) is polymorphic

Update

In response to @helpwithhaskell's question in the comments...

Consider this function:

bar :: (forall n. Num n => n -> n) -> (Int, Double) -> (Int, Double)
bar f (i,d) = (f i, f d)

That is, we apply f to both an Int and a Double. Without using RankNTypes it won't type check:

-- doesn't work
bar' :: ??? -> (Int, Double) -> (Int, Double)
bar' f (i,d) = (f i, f d)

None of the following signatures work for ???:

Num n => (n -> n)
Int -> Int
Double -> Double