Understanding Haskell RankNTypes

Question

While working on GHC extensions, I met RankNTypes at Haskell , which gave an example:

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

This article suggests an alternative type for rankN :

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

The explanation for the difference is that "the last digit requires n from n to n for some Num n, the first signature requires a function from n to n for each Num n."

I can understand that the first type requires the signature to be in brackets or more general. I do not understand the explanation that the last signature just requires the function n -> n for "some Num n ". Can someone clarify and clarify? How do you “read” this former signature so that it sounds like it? Is the last signature the same as just Num n => (n -> n) -> (Int, Double) without having to forall ?

Answer 1

In the normal case ( forall n. Num n => (n -> n) -> (Int, Double) ) we first select a n and then provide a function. Thus, we could pass a function like Int -> Int , Double -> Double , Rational -> Rational , etc.

In the case of the 2nd rank ( (forall n. Num n => n -> n) -> (Int, Double) ) we must provide a function before we know n . This means that the function should work for any n ; none of the examples listed in the previous example will work.

We need this for the sample code, because the passed function f applies to two different types: a Int and a Double . Therefore, he must work for both of them.

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

What type of function works for any n ? This is for sure forall n. Num n => n -> n forall n. Num n => n -> n .

Answer 2

How do you “read” this former signature so that it sounds like this?

You can read

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

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

First rank

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

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

Is the last signature the same as just Num n => (n -> n) -> (Int, Double) without having to forall ?

Yes, by default, all forall implicitly placed in the outermost position (the result is a rank-1 type).

Answer 3

In the case of rankN f must be a polymorphic function that is valid for all number types n .

In rank1 case, f must be defined for only one number type.

Here are a few examples that illustrate 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) = (fi, fd) 

That is, we apply f both Int and Double. Without using RankNTypes, he will not enter a check:

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

None of the following signatures work for:

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