The purpose of forall in RankNTypes

Question

In writing some Haskell code with the help of hlint, I followed the prompt to add a type signature to a function. It injected something sort of like this:

{-# LANGUAGE RankNTypes #-}

multipleOf :: forall a. Integral a => a -> a -> Bool
multipleOf divisor n = n `mod` divisor == 0

This language extension is new to me, but as I understand, this is identical with the simpler:

multipleOf :: Integral a => a -> a -> Bool
multipleOf divisor n = n `mod` divisor == 0

Every example of rank N types I've read about seem don't seem to add anything new over the polymorphism that was already available, and this forall syntax doesn't seem to add any value.

What am I missing? Is there a good example of what this forall syntax does beyond what's available without extensions?

Answer 1

You're missing that you can limit the scope of the quantified type variable:

modifyPair :: (Num b, Num c) => (forall a. Num a => a -> a) -> (b, c) -> (b, c)
modifyPair f (b, c) = (f b, f c)

Try writing that function without the RankNTypes extension. In particular, allowing the elements of the pair to be different types from each other.

This specific example isn't too useful, but the general idea holds. You can specify that an argument to a function must be polymorphic.

There's an additional trick you can perform with this tooling. The canonical example comes from ST. The goal of the ST library is to allow constrained use of mutable data. That is, you can implement an algorithm involving true mutation, and present an external interface that's pure. ST itself takes care of proving that the use is safe via clever type system tricks:

newtype ST s a    = ... -- details aren't important
newtype STRef s a = ... -- details still aren't important

-- a standard-ish interface to mutable data
newSTRef :: ST s (STRef s a)
readSTRef :: STRef s a -> ST s a
writeSTRef :: STRef s a -> a -> ST s ()

-- the magic using RankNTypes
runST :: (forall s. ST s a) -> a

That extra type variable, s, is worth paying attention to. It appears in both ST and STRef. Every function that manipulates an STRef makes sure that the s in the ST and STRef is the same type variable. So when you get to runST, you find that the type s has to be unrelated to the type a. s has its scope more confined than that of a. The end result of this is that you can't write something like runST newSTRef. The type checker will reject it because the type variable s would have to escape the context in which it's quantified.

So there really are some handy tricks you can pull when you can specify that a function's argument must be polymorphic.