RankNTypes intuition

rank-n-types-intuition.md

A coworker and I were discussing RankNTypes and why the extension is used in lens. RankNTypes has confused me for a while, but making the connection to lens gave me a good intuition (strangely?). Here’s a recap in case it’s useful to anyone else:

If you have a normal higher-order function:

foo :: Num a => (a -> a) -> a
foo f = f 1

We can pass foo any function that fits the (a -> a) with a Num constraint:

foo id
1

foo abs
1

foo negate
-1

But what if we want to define foo such that foo itself can decide the type of a, since it knows it’s given a function that will work for any a as long as it is a Num. We’ll try:

foo' :: Num a => (a -> a) -> a
foo' f = f (1 :: Int)

<interactive>:23:13: error:
• Couldn't match expected type 'a' with actual type 'Int'
'a' is a rigid type variable bound by
the type signature for:
foo' :: forall a. Num a => (a -> a) -> a
at <interactive>:22:9
• In the first argument of 'f', namely '(1 :: Int)'
In the expression: f (1 :: Int)
In an equation for 'foo'': foo' f = f (1 :: Int)
• Relevant bindings include
f :: a -> a (bound at <interactive>:23:6)
foo' :: (a -> a) -> a (bound at <interactive>:23:1)

Womp womp, no can do. This makes sense too because the return type of the function is a. Changing it to Int would also give us a compiler error. But what if we instead make the function passed into the function we’re trying to define be Rank 2 polymorphic?

:set -XRank2Types

foo' :: (forall a. Num a => (a -> a)) -> Int
foo' f = f (1 :: Int)

Now the implementor of foo' gets the ability to specialize the concrete type to Int. Squint hard enough, and foo' is very similar to lens library’s view, set, etc:

type Setter s t a b = forall f. Settable f => (a -> f b) -> s -> f t
set :: Setter s t a b -> b -> s -> t
-- ... aka ...
set :: (forall f. Settable f => (a -> f b) -> s -> f t) -> b -> s -> t

The set function can choose what specialization it wants for f as long as it is Settable, so it uses the ASetter type synonym which uses Identity for f:

type ASetter s t a b = (a -> Identity b) -> s -> Identity t

In my coworker’s words, RankNTypes let us have “multiple specializations at different call sites”.