On 5/26/08, Andrew Coppin
This is probably the first real use I've ever seen of so-called rank-2 types, and I'm curios to know why people think they need to exist. [Obviously when somebody vastly more intelligent than me says something is necessary, they probably know something I don't...]
The usual example I've seen for "beauty in rank-2 types" is the ST monad. ST lets you define 'stateful' imperative algorithms with destructive update, but be able to call them safely from pure-functional code. This is made safe by a "phantom" type variable and the rank-2 type of runST:
runST :: forall a. (forall s. ST s a) -> a
The "s" in ST logically represents the "initial state" used by the imperative computation it represents; it tracks any allocations and updates that need to be made before the computation can run. By requiring that the passed in computation works for *any* initial state, you guarantee that it can't reference any external store or return data from within the store; for example, consider this:
newSTRef :: forall s a. a -> ST s (STRef s a)
mkZero :: forall s. ST s (STRef s Int) mkZero = newSTRef 0
Now consider trying to type "runST mkZero"; first we generate a new type variable "s1" for the "s" in mkZero, then use it to instantiate the result type, "a": runST :: (forall s. ST s (STRef s1 a)) -> STRef s1 a Now we need to unify s1 with s to match mkZero's type for the first argument. But we can't do that, because then "s" escapes its forall scope. So we can statically guarantee that no references escape from runST! --- Another example that I personally am attached to is Prompt: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/MonadPrompt (There's no Haddock documentation on that site, but the source code is well-commented and there's a module of examples). The function I want to talk about is "runPrompt"
prompt :: forall p a. p a -> Prompt p a runPrompt :: forall p r. (forall a. p a -> a) -> Prompt p r -> r
Lets instantiate p and r to simplify things; I'll use [] for p and Int for r.
test1 :: Prompt [] Int test1 = prompt [1,2,3]
test2 :: Prompt [] Int test2 = do x <- prompt ['A', 'B', 'C'] return (ord x) -- ord :: Char -> Int
Now, the type of runPrompt specialized for these examples is
runPrompt :: (forall a. [a] -> a) -> Prompt [] Int -> Int
Notice that we need to pass in a function that can take -any- list and return an element. One simple example is "head":
head :: forall a. [a] -> a head (x:xs) = x
So, putting it together: ghci> runPrompt head test1 1 ghci> runPrompt head test2 65 -- ascii code for 'A'. Now, this isn't that great on its own; wouldn't it be useful to be able to get some information about the type of result needed when writing your prompt-handler function? Then you could do something different in each case. That's a question for another topic, but to get you started, start looking around for information on GADTs. -- ryan