What is the purpose of Rank2Types?

Solution 1:

It's hard to understand higher-rank polymorphism unless you study System F directly, because Haskell is designed to hide the details of that from you in the interest of simplicity.

But basically, the rough idea is that polymorphic types don't really have the a -> b form that they do in Haskell; in reality, they look like this, always with explicit quantifiers:

id :: ∀a.a → a
id = Λt.λx:t.x

If you don't know the "∀" symbol, it's read as "for all"; ∀x.dog(x) means "for all x, x is a dog." "Λ" is capital lambda, used for abstracting over type parameters; what the second line says is that id is a function that takes a type t, and then returns a function that's parametrized by that type.

You see, in System F, you can't just apply a function like that id to a value right away; first you need to apply the Λ-function to a type in order to get a λ-function that you apply to a value. So for example:

(Λt.λx:t.x) Int 5 = (λx:Int.x) 5
                  = 5

Standard Haskell (i.e., Haskell 98 and 2010) simplifies this for you by not having any of these type quantifiers, capital lambdas and type applications, but behind the scenes GHC puts them in when it analyzes the program for compilation. (This is all compile-time stuff, I believe, with no runtime overhead.)

But Haskell's automatic handling of this means that it assumes that "∀" never appears on the left-hand branch of a function ("→") type. Rank2Types and RankNTypes turn off those restrictions and allow you to override Haskell's default rules for where to insert forall.

Why would you want to do this? Because the full, unrestricted System F is hella powerful, and it can do a lot of cool stuff. For example, type hiding and modularity can be implemented using higher-rank types. Take for example a plain old function of the following rank-1 type (to set the scene):

f :: ∀r.∀a.((a → r) → a → r) → r

To use f, the caller first must choose what types to use for r and a, then supply an argument of the resulting type. So you could pick r = Int and a = String:

f Int String :: ((String → Int) → String → Int) → Int

But now compare that to the following higher-rank type:

f' :: ∀r.(∀a.(a → r) → a → r) → r

How does a function of this type work? Well, to use it, first you specify which type to use for r. Say we pick Int:

f' Int :: (∀a.(a → Int) → a → Int) → Int

But now the ∀a is inside the function arrow, so you can't pick what type to use for a; you must apply f' Int to a Λ-function of the appropriate type. This means that the implementation of f' gets to pick what type to use for a, not the caller of f'. Without higher-rank types, on the contrary, the caller always picks the types.

What is this useful for? Well, for many things actually, but one idea is that you can use this to model things like object-oriented programming, where "objects" bundle some hidden data together with some methods that work on the hidden data. So for example, an object with two methods—one that returns an Int and another that returns a String, could be implemented with this type:

myObject :: ∀r.(∀a.(a → Int, a -> String) → a → r) → r

How does this work? The object is implemented as a function that has some internal data of hidden type a. To actually use the object, its clients pass in a "callback" function that the object will call with the two methods. For example:

myObject String (Λa. λ(length, name):(a → Int, a → String). λobjData:a. name objData)

Here we are, basically, invoking the object's second method, the one whose type is a → String for an unknown a. Well, unknown to myObject's clients; but these clients do know, from the signature, that they will be able to apply either of the two functions to it, and get either an Int or a String.

For an actual Haskell example, below is the code that I wrote when I taught myself RankNTypes. This implements a type called ShowBox which bundles together a value of some hidden type together with its Show class instance. Note that in the example at the bottom, I make a list of ShowBox whose first element was made from a number, and the second from a string. Since the types are hidden by using the higher-rank types, this doesn't violate type checking.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ImpredicativeTypes #-}

type ShowBox = forall b. (forall a. Show a => a -> b) -> b

mkShowBox :: Show a => a -> ShowBox
mkShowBox x = \k -> k x

-- | This is the key function for using a 'ShowBox'.  You pass in
-- a function @k@ that will be applied to the contents of the 
-- ShowBox.  But you don't pick the type of @k@'s argument--the 
-- ShowBox does.  However, it's restricted to picking a type that
-- implements @Show@, so you know that whatever type it picks, you
-- can use the 'show' function.
runShowBox :: forall b. (forall a. Show a => a -> b) -> ShowBox -> b
-- Expanded type:
--
--     runShowBox 
--         :: forall b. (forall a. Show a => a -> b) 
--                   -> (forall b. (forall a. Show a => a -> b) -> b)
--                   -> b
--
runShowBox k box = box k


example :: [ShowBox] 
-- example :: [ShowBox] expands to this:
--
--     example :: [forall b. (forall a. Show a => a -> b) -> b]
--
-- Without the annotation the compiler infers the following, which
-- breaks in the definition of 'result' below:
--
--     example :: forall b. [(forall a. Show a => a -> b) -> b]
--
example = [mkShowBox 5, mkShowBox "foo"]

result :: [String]
result = map (runShowBox show) example

PS: for anybody reading this who's wondered how come ExistentialTypes in GHC uses forall, I believe the reason is because it's using this sort of technique behind the scenes.

Solution 2:

Do not functions in Haskell already support polymorphic arguments?

They do, but only of rank 1. This means that while you can write a function that takes different types of arguments without this extension, you can't write a function that uses its argument as different types in the same invocation.

For example the following function can't be typed without this extension because g is used with different argument types in the definition of f:

f g = g 1 + g "lala"

Note that it's perfectly possible to pass a polymorphic function as an argument to another function. So something like map id ["a","b","c"] is perfectly legal. But the function may only use it as monomorphic. In the example map uses id as if it had type String -> String. And of course you can also pass a simple monomorphic function of the given type instead of id. Without rank2types there is no way for a function to require that its argument must be a polymorphic function and thus also no way to use it as a polymorphic function.

Solution 3:

Luis Casillas's answer gives a lot of great info about what rank 2 types mean, but I'll just expand on one point he didn't cover. Requiring an argument to be polymorphic doesn't just allow it to be used with multiple types; it also restricts what that function can do with its argument(s) and how it can produce its result. That is, it gives the caller less flexibility. Why would you want to do that? I'll start with a simple example:

Suppose we have a data type

data Country = BigEnemy | MediumEnemy | PunyEnemy | TradePartner | Ally | BestAlly

and we want to write a function

f g = launchMissilesAt $ g [BigEnemy, MediumEnemy, PunyEnemy]

that takes a function that's supposed to choose one of the elements of the list it's given and return an IO action launching missiles at that target. We could give f a simple type:

f :: ([Country] -> Country) -> IO ()

The problem is that we could accidentally run

f (\_ -> BestAlly)

and then we'd be in big trouble! Giving f a rank 1 polymorphic type

f :: ([a] -> a) -> IO ()

doesn't help at all, because we choose the type a when we call f, and we just specialize it to Country and use our malicious \_ -> BestAlly again. The solution is to use a rank 2 type:

f :: (forall a . [a] -> a) -> IO ()

Now the function we pass in is required to be polymorphic, so \_ -> BestAlly won't type check! In fact, no function returning an element not in the list it is given will typecheck (although some functions that go into infinite loops or produce errors and therefore never return will do so).

The above is contrived, of course, but a variation on this technique is key to making the ST monad safe.