Practical applications of Rank 2 polymorphism?

Question

I'm covering polymorphism and I'm trying to see the practical uses of such a feature.

My basic understanding of Rank 2 is:

type MyType = ∀ a. a -> a

subFunction :: a -> a
subFunction el = el

mainFunction :: MyType -> Int
mainFunction func = func 3

I understand that this is allowing the user to use a polymorphic function (subFunction) inside mainFunction and strictly specify it's output (Int). This seems very similar to GADT's:

data Example a where
 ExampleInt :: Int -> Example Int
 ExampleBool :: Bool -> Example Bool

1) Given the above, is my understanding of Rank 2 polymorphism correct?

2) What are the general situations where Rank 2 polymorphism can be used, as opposed to GADT's, for example?

Answer 1

If you pass a polymorphic function as and argument to a Rank2-polymorphic function, you're essentially passing not just one function but a whole family of functions – for all possible types that fulfill the constraints.

Typically, those forall quantifiers come with a class constraint. For example, I might wish to do number arithmetic with two different types simultaneously (for comparing precision or whatever).

data FloatCompare = FloatCompare {
     singlePrecision :: Float
   , doublePrecision :: Double
   }

Now I might want to modify those numbers through some maths operation. Something like

modifyFloat :: (Num -> Num) -> FloatCompare -> FloatCompare

But Num is not a type, only a type class. I could of course pass a function that would modify any particular number type, but I couldn't use that to modify both a Float and a Double value, at least not without some ugly (and possibly lossy) converting back and forth.

Solution: Rank-2 polymorphism!

modifyFloat :: (∀ n . Num n => n -> n) -> FloatCompare -> FloatCompare
mofidyFloat f (FloatCompare single double)
    = FloatCompare (f single) (f double)

The best single example of how this is useful in practice are probably lenses. A lens is a “smart accessor function” to a field in some larger data structure. It allows you to access fields, update them, gather results... while at the same time composing in a very simple way. How it works: Rank2-polymorphism; every lens is polymorphic, with the different instantiations corresponding to the “getter” / “setter” aspects, respectively.

Answer 2

The go-to example of an application of rank-2 types is runST as Benjamin Hodgson mentioned in the comments. This is a rather good example and there are a variety of examples using the same trick. For example, branding to maintain abstract data type invariants across multiple types, avoiding confusion of differentials in ad, a region-based version of ST.

But I'd actually like to talk about how Haskell programmers are implicitly using rank-2 types all the time. Every type class whose methods have universally quantified types desugars to a dictionary with a field with a rank-2 type. In practice, this is virtually always a higher-kinded type class^* like Functor or Monad. I'll use a simplified version of Alternative as an example. The class declaration is:

class Alternative f where
    empty :: f a
    (<|>) :: f a -> f a -> f a

The dictionary representing this class would be:

data AlternativeDict f = AlternativeDict {
    empty :: forall a. f a,
    (<|>) :: forall a. f a -> f a -> f a }

Sometimes such an encoding is nice as it allows one to use different "instances" for the same type, perhaps only locally. For example, Maybe has two obvious instances of Alternative depending on whether Just a <|> Just b is Just a or Just b. Languages without type classes, such as Scala, do indeed use this encoding.

To connect to leftaroundabout's reference to lenses, you can view the hierarchy there as a hierarchy of type classes and the lens combinators as simply tools for explicitly building the relevant type class dictionaries. Of course, the reason it isn't actually a hierarchy of type classes is that we usually will have multiple "instances" for the same type. E.g. _head and _head . _tail are both "instances" of Traversal' s a.

^* A higher-kinded type class doesn't necessarily lead to this, and it can happen for a type class of kind *. For example:

-- Higher-kinded but doesn't require universal quantification.
class Sum c where
    sum :: c Int -> Int

-- Not higher-kinded but does require universal quantification.
class Length l where
    length :: [a] -> l