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?

Troytroyer

Real world example: runST :: (forall s. ST s a) -> a keeps two separate ST computations from having the same s. This prevents you from leaking STRefs outside the ST monad. – Kingwood

I'm not sure I understand why rank-2 functions seem similar to GADTs to you. Can you clarify what you mean by that? – Shaunshauna

@DanielWagner At least existential types can be expressed with GADTs (e.g data Ext where Ext :: a -> Ext). Probably also other constructs that could be expressed with Rank 2 Types? – Bucket

One can encode the equality between two types (as in the 'canonical' GADT - data (:~:) a b where Refl :: a :~: a) using rank 2 types - newtype (:~:) a b = Refl (forall p . p a -> p b) - and a similar such encoding is used in lens. – Tortoise

Answer 1

If you pass a polymorphic function as an 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 could not 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.

Roentgenogram

This is a great answer, the additional introduction to lenses is much appreciated! – Troytroyer

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

Tedda

Answer 3

If you are using modules in Haskell, you are already using Rank-2 types. Theoretically speaking, modules are records with rank-2 type properties.

For example, the Foo module below in Haskell ...

module Foo(id) where
id :: forall a. a -> a
id x = x

import qualified Foo
main = do
  putStrLn (Foo.id "hello")
  return ()

... can actually be thought as a record as follows:

type FooType = FooType {
  id :: forall a. a -> a
}
Foo :: FooType
Foo = Foo {
  id = \x -> x
}

P/S (unrelated this question): from a language design perspective, if you are going to support module system, then you might as well support higher-rank types (i.e. allow arbitrary quantification of type variables on any level) to reduce duplication of efforts (i.e. type checking a module should be almost the same as type checking a record with higher rank types).

Lavatory

Answer 4

The ability to treat something as a first-class construct means you can abstract it out. You can abstract 5 out of 5 * 5 * 5 using a (first-order) function f 5.

f :: Int -> Int
f x = x * x * x

Higher-order functions can abstract out multiplication f (*):

f :: (Int -> Int -> Int) -> Int
f (·) = (x · x) · x

This does not perfectly abstract the multiplication out because we are passing in a monomorphic multiplication function f ((*) :: Int -> Int -> Int) rather than the constrained polytype:

(*) :: forall a. Num a => a -> a -> a

To fully abstract the multiplication function, we need to be able to pass a polymorphic function as an argument: Without Rank-N types, we could not properly abstract out polymorphic functions! The type of the argument is copy-pasted from the type of (*).

f :: (forall a. Num a => a -> a -> a) -> Int 
f mul = mul @Int (mul @Int 5 5) 5

Passing a polymorphic function as an argument enables us to instantiate it at different types. run print abstracts out the polymorphic print function, used at print :: Int -> IO () and print :: Bool -> IO ().

run :: (forall a. Show a => a -> IO ()) -> IO ()
run pr = do
  pr @Int  10
  pr @Bool False

And you can abstract the sequencing as well, such that run print equals runOf (*>) print.

runOf :: (forall a b. IO a -> IO b -> IO b) 
      -> (forall a. Show a => a -> IO ())
      -> IO ()
runOf (·>) pr =
  sequ @() @()
    (pr @Int 10)
    (pr @Bool False)

This ability is important because polymorphic functions are one of the most common features in Haskell. To perform a dictionary translation of any type class with quantification in the methods, you need rank-2 types. You could say that Functor abstracts a over the polymorphic function fmap.

type  Functor :: (Type -> Type) -> Constraint
class Functor f where
  fmap :: forall a a'. (a -> a') -> (f a -> f a')

type DFunctor :: (Type -> Type) -> Type
data DFunctor f = DFunctor 
  { d_fmap :: forall a a'. (a -> a') -> (f a -> f a') }

As such you can replace a Functor f constraint with a polymorphic function argument.

ffmapNot :: (forall a a'. (a -> a') -> (f a -> f a'))
         -> (f (f Bool) -> f (f Bool))
ffmapNot fmap = fmap (fmap not)

This is the idea behind the lens library. To parameterise methods from type classes, and passing them as a compositional

type Traversal :: Type -> Type -> Type -> Type -> Type
type Traversal as bs a b = forall f. Applicative f => (a -> f b) -> (as -> f bs)

Now we can define toList = toListOf traverse (more accurately, toListof foldMap).

-- in actuality, `toListOf` has a more general type
toListOf :: forall as a. Traversal as as a a -> as -> [a]
toListOf trav as = trav' (:) as [] where
  trav' :: (a -> [a] -> [a]) -> (as -> [a] -> [a])
  trav' = coerce do trav @(Const (Endo [a]))

toListOf traverse
  :: Traversable t
  => t a -> [a]
toListOf (traverse . traverse)
  :: Traversable t1
  => Traversable t2
  => t1 (t2 a) -> [a]

Engagement