Consider this function:
tuple2Int :: (x -> Int) -> (a, b) -> (Int, Int) tuple2Int f (a, b) = (f a, f b)
…which wouldn’t work. Why? Because of
f a, the type checker deduces that
x is equivalent to
a); because of
f b, the type checker also deduces that
a~x~b, which is obviously false for most cases.
RankNTypes, we can instead write the type signature of the function as
tuple2Int' :: (forall x. x -> Int) -> (a, b) -> (Int, Int). This way, the compiler knows that it should use two seperate
b. It therefore deduces that
x2~b and because it is not enforced that
x1~x2, there is no problem at all!
What’s going on?
First, we need to learn the cruel and ugly fact that NO so-called “generic” function in Haskell is actually generic in essence. What does this mean? Let’s consider
length :: [a] -> Int. It looks pretty generic to me as I can use it on any type of list, you may say. This is true, but what happens under the hood is that the compiler specializes a version of the function with concrete type (i.e. no type variable like
a) everytime you use it. For example, when you do
length [1, 2, 3], a specialized version
length(Int) :: [Int] -> Int is magically created by the compiler to accomodate you; when you do
length "abcdefg", similarly a
length(Char) [Char] -> Int is created. Just remember this for now.
Just as we use
\x -> ... to define a lambda function with variable
x, we use
forall a. ... to define a type with type variable
a. Therefore, suppose that we can construct the type of a function by a data constructor
FunctionType a b, where
b are values that represent types, our
(forall x. x -> Int) in the last paragraph would be equivalent to
\x -> FunctionType x Int. You also need to remember this.
And then, a crash course in lambda calculus. Consider this lambda function:
\x y -> x + y + z. We call
y bound variables, because their appearance is bound by the
\x y part of the function. We call
z a free variable, because it is defined “elsewhere” and is thus not bound by the
\x y part. End of the crash course.
With the three things we just learned, we can touch on the problem. Firstly, we have a rule that no type variables in a type contruction can be free. For example, we can’t write a type-level function like
\x -> FunctionType x y, or formally
forall x. x -> y, because
y is free. This is a very strict rule and obviously we don’t want to be scolded by the compiler every now and then just because of it, so we have another catch-all rule: if a type variable is not explicitly bound, it is then treated as bound at the beginning of the expression. What does this mean? Suppose we have a type
a -> a (or
FunctionType a a with our syntax). Because you see no
forall in its type signature, technically
a is free. This is when the rule kicks in: because
a is not explicitly bound, we treat the whole type as
forall a. a -> a (or
\a -> FunctionType a a) and voila! The first rule is automatically satisfied. How nice.
Generic functions in Haskell are all defined this way.
id, for example, has type
forall a. a -> a. Our
tuple2Int, because it has
b that all appear to be free, has type
forall x a b. (x -> Int) -> (a, b) -> (Int, Int) by the second rule. This is where our problem arises: when we are using this function, the compiler needs to create a concrete version of it (in other words, it needs to assign types to
b). Furthremore, because
x is scoped on the whole type expression, it must takes the same value everywhere. An example:
foo = (\x -> x + (\y -> x + 3) 4) 5 bar = (\f -> f 2 + f 3 + f 4) (\x -> x + 2)
x is bound at the very beginning, it is scoped over the whole expression. Therefore, it must always takes the value
5. On the contrary, in
x is bound only inside the second pair of brackets, it can take different values of
4 elsewhere (i.e. inside the first pair of brackets).
tuple2Int. What type should the compiler assign to
x? It sees that
a can be applied to
x -> Int, so
x must be the same. Similar deduction goes for
x. Therefore, unless
b are the same type, we would have a type contradiction.
Now make sure that you understand the problem, and we’ll proceed to its solution.