Understanding Haskell's RankNTypes
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 ?
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) 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 forall n. Num n => n -> n .
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 forall s are implicitly placed at the outer-most position (resulting in a rank-1 type).
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
上一篇: 有没有办法在GHC Haskell中定义一种存在量化的新类型？
下一篇: 了解Haskell的RankNTypes