For a beginner of haskell coming from popular imperative languages with “Generic” or “Template” construct in them, like C++, Java, it is not too hard to accept the parametric polymorphism at first glance. The type signature of id :: a -> a can quickly remind him of C++ template.
#include <iostream>
#include <string>
using namespace std;
template <typename T>
T id(const T &x)
{
return x;
}
int main()
{
cout << id(1) << endl;
cout << id(string("foo")) << endl;
return 0;
}
However, the thing would become complicated when he bumped to the type signature of runST
runST :: (forall s. ST s a) -> a
A few questions pop out. What the hell is that forall, and what are Rank2Types and RankNTypes documented in the GHC manual?
Higher Rank Polymorphism
The parametric polymorphism you usually see is actually Rank-1 Polymorphism. There is actually Rank-2 polymorphism … to Rank-N polymorphism. In not quite exact language, a Rank-1 polymorphic function is that it doesn’t depend on its input/output types. The type become parameters, and when you call the function, the types are “instantiated.” And Rank-2 polymorphic function is a function gets called with its parameters parameterized, or to be Rank-1 polymorphic. So on, Rank-N polymorphic function is a function gets called with its parameters to be Rank-(N-1) polymorphic.
Let’s look at a Rank-2 example. Suppose we have a list of Int and a list of Char, we want to write a function to check if the results of applying a function to both lists are equal. Use case would look like this.
check f l1 l2 = (f l1) == (f l2)
main = do
print $ check length [1,2,3,4] ['a','b','c','d']
print $ check ((+2) . length) [1,2] ['a']
We can see that we want parameter f of check to be a Rank-1 polymorphic function, so that we can apply it to both [Int] and [Char]. In such case, what would be the type signature of check? Let’s look at how we can declare it in haskell.
forall
Parametric polymorphism is implicit in haskell. When you write a -> a, actually it is forall a. a -> a. forall is the keyword to explicitly declare what is your type parameter, or type variable. A few examples from standard lib can be explicitly written like this.
length :: forall a. [a] -> Int
fst :: forall a b. (a,b) -> a
map :: forall a b. (a -> b) -> [a] -> [b]
Writing out explicitly, we declare the type signature of check as check :: (forall a. [a] -> Int) -> forall b. [b] -> forall c. [c] -> Bool. Notice that the effective range of forall greedily extends to the most right end, so the type signature above is equivalent to check :: (forall a. a -> [Int]) -> (forall b. [b] -> (forall c. [c] -> Bool)). But so many forall in the type signature, you would ask where should I put the forall to express a Rank-2 polymorphic function. Just as this link said, you can consider forall as a type level lambda /. This lambda / has some operational similarity with , instead of declare a variable binding, it binds type variables. A parallel in C++ would be binding T of template to the corresponding template.
With this in mind, basically we can write out the type variables and normal variables at the same time in / and . It would look like check = > /> 1 -> /> 2 -> Bool, where f is a function which is /-> -> Int.
Here is a working example:
{-# LANGUAGE RankNTypes #-}
module Main(main) where
import Prelude hiding (length)
length :: forall a. [a] -> Int
length (x:xs) = 1 + (length xs)
length [] = 0
check :: (forall a. [a] -> Int) -> forall b. [b] -> forall c. [c] -> Bool
check f l1 l2 = (f l1) == (f l2)
main = do
print $ check length [1] ['a','b']
You can play with Rank-N Type with N greater than 2. The spirit is the same. This is an example from here.
{-# LANGUAGE RankNTypes #-}
module Main (main) where
g1 :: a -> a
g1 x = x
g2 :: (forall a. a -> a) -> (Bool, Char)
g2 f = (f True, f 'a')
g3 :: ((forall a. a -> a) -> (Bool, Char)) -> (Char, Bool)
g3 f = (\x -> (snd x, fst x)) (f g1)
g4 :: (((forall a. a-> a) -> (Bool, Char)) -> (Char, Bool)) -> (Bool, Char)
g4 f = (\x -> (snd x, fst x)) (f g2)
main = do
putStrLn "Rank-2:"
putStrLn . show . fst $ (g2 g1)
putStrLn . show . snd $ (g2 g1)
putStrLn "Rank-3:"
putStrLn . show . fst . g3 $ g2
putStrLn . show . snd . g3 $ g2
putStrLn "Rank-4:"
putStrLn . show . fst . g4 $ g3
putStrLn . show . snd . g4 $ g3Possible Confusion
Possible Confusion
Due to the usage of forall keyword, it is very easy to confuse RankNTypes, Existential Types and Scoped Type Variables. You can go to check out an excellent discussion on stackoverflow. Also don’t miss out John Lato’s and ezyang’s explanations on Existenatial Types.
